Anforderungen  |   Konzepte  |   Entwurf  |   Entwicklung  |   Qualitätssicherung  |   Lebenszyklus  |   Steuerung
 
 
 
 


Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Test.java   Sprache: PVS

Original von: PVS©

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%  From any sequence one can extract           %
%  an increasing or a decreasing sub-sequence  %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

monotone_subsequence : THEORY

  BEGIN

  IMPORTING sequence_props

  u, s : VAR sequence[real]

  i, j, n : VAR nat
  


  %---------------------------------------------------
  %  If all the suffixes of v have a minimal element
  %  then v contains an increasing sub-sequence
  %---------------------------------------------------

  has_minimum(u, n) : bool =
 EXISTS i : n <= i AND FORALL j : n <= j IMPLIES u(i) <= u(j)

  minimum_prefix : LEMMA
 EXISTS i : FORALL j : j <= n IMPLIES u(i) <= u(j)

  minimum_suffix : LEMMA
 has_minimum(u, n) IMPLIES has_minimum(u, 0)


  v : VAR { u | FORALL n : has_minimum(u, n) }


  %--- a minimum of the elements n, n+1, ....  ---%

  mini(v, n) : nat =
 epsilon! i : n <= i AND FORALL j : n <= j IMPLIES v(i) <= v(j)

  min_prop : LEMMA
 n <= mini(v, n) AND FORALL j : n <= j IMPLIES v(mini(v, n)) <= v(j)

  min_prop1 : COROLLARY  n <= mini(v, n)

  min_prop2 : COROLLARY  n <= i IMPLIES v(mini(v, n)) <= v(i)


  %--- subsequence ---%

  h(v)(i) : RECURSIVE nat =
 IF i = 0
 THEN mini(v, 0)
 ELSE mini(v, h(v)(i - 1) + 1)
 ENDIF
     MEASURE i

  hseq(v) : sequence[real] = LAMBDA i : v(h(v)(i))

  h_increasing : LEMMA strict_increasing?(h(v))

  hseq_extraction : LEMMA subseq(hseq(v), v)

  hseq_increasing : LEMMA increasing?(hseq(v))


    

  %------------------------------------------------------
  %  If a sequence has no minimal element it contains a 
  %  (strictly) decreasing sub-sequence
  %------------------------------------------------------

  w : VAR { u | not has_minimum(u, 0) }

  no_minimum : LEMMA not has_minimum(w, n)

  pick(w, n) : nat = epsilon! i : n <= i AND w(i) < w(n)

  pick_prop : LEMMA  n <= pick(w, n) AND w(pick(w, n)) < w(n)

  pick_prop1 : COROLLARY  n < pick(w, n)

  pick_prop2 : COROLLARY  w(pick(w, n)) < w(n)


  %--- subsequence ---%

  g(w)(i) : RECURSIVE nat =
 IF i = 0
 THEN pick(w, 0)
 ELSE pick(w, g(w)(i - 1))
 ENDIF
     MEASURE i

  gseq(w) : sequence[real] = LAMBDA i : w(g(w)(i))

  g_increasing : LEMMA strict_increasing?(g(w))

  gseq_extraction : LEMMA subseq(gseq(w), w)

  gseq_decreasing : LEMMA strict_decreasing(gseq(w))


  %------------------------
  %  Suffix starting at n
  %------------------------

  suffix(u, n) : sequence[real] = LAMBDA i : u(n+i)

  suffix_subseq : LEMMA subseq(suffix(u, n), u)

  suffix_hasmin : LEMMA
 has_minimum(suffix(u, n), 0) IFF has_minimum(u, n)


  %----------------
  %  Main theorem
  %----------------

  monotone_subsequence : THEOREM
 EXISTS s : subseq(s, u) AND (increasing?(s) OR decreasing(s))
 

  END monotone_subsequence

¤ Dauer der Verarbeitung: 0.25 Sekunden  (vorverarbeitet)  ¤





Download des
Quellennavigators
Download des
sprechenden Kalenders

in der Quellcodebibliothek suchen




Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.


Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff



                                                                                                                                                                                                                                                                                                                                                                                                     


Neuigkeiten

     Aktuelles
     Motto des Tages

Software

     Produkte
     Quellcodebibliothek

Aktivitäten

     Artikel über Sicherheit
     Anleitung zur Aktivierung von SSL

Muße

     Gedichte
     Musik
     Bilder

Jenseits des Üblichen ....
    

Besucherstatistik

Besucherstatistik