Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: csequence_merge_split.pvs Sprache: PVS

Original von: PVS^©

bisection_nat_sqrt: THEORY

BEGIN

  IMPORTING appendix

  n,m,x: VAR nat
  pn:    VAR posnat

  fs_lt?(n,m):bool = sq(m+1) <= n
  fs_eq?(n,m):bool = sq(m) <= n AND n < sq(m+1)
  fs_gt?(n,m):bool = n < sq(m)

  fs_lt?(n)(m):bool = fs_lt?(n,m)
  fs_le?(n)(m):bool = fs_lt?(n,m) OR fs_eq?(n,m)
  fs_eq?(n)(m):bool = fs_eq?(n,m)
  fs_gt?(n)(m):bool = fs_gt?(n,m)
  fs_ge?(n)(m):bool = fs_eq?(n,m) OR fs_gt?(n,m)

  fs_lt_def: LEMMA fs_lt?(n,m) => (NOT fs_eq?(n,m) AND NOT fs_gt?(n,m))
  fs_eq_def: LEMMA fs_eq?(n,m) => (NOT fs_lt?(n,m) AND NOT fs_gt?(n,m))
  fs_gt_def: LEMMA fs_gt?(n,m) => (NOT fs_lt?(n,m) AND NOT fs_eq?(n,m))

  fs_trichotomy: LEMMA fs_lt?(n,m) OR fs_eq?(n,m) OR fs_gt?(n,m)

  fs_le_ge: LEMMA fs_le?(x)(m) AND fs_ge?(x)(n) AND m /= n => m < n

  bisection_sqrt_aux(x:nat,m:(fs_le?(x)),n:(fs_ge?(x))): RECURSIVE nat
    = IF m = n THEN m ELSE LET t = floor((n+m)/2) IN
          IF    fs_lt?(x,t) THEN bisection_sqrt_aux(x,t+1,n)
          ELSIF fs_eq?(x,t) THEN t
                            ELSE bisection_sqrt_aux(x,m,t) ENDIF ENDIF
      MEASURE (LAMBDA (x:nat,m:(fs_le?(x)),n:(fs_ge?(x))): (n-m)+1)

  bisection_sqrt_aux_prop: LEMMA fs_le?(x)(m) AND fs_ge?(x)(n) =>
                                 fs_eq?(x,bisection_sqrt_aux(x,m,n))

  bisection_sqrt(n):nat = bisection_sqrt_aux(n,0,n)

  bisection_sqrt_def: LEMMA bisection_sqrt(n) = floor(sqrt(n))

END bisection_nat_sqrt

¤ Dauer der Verarbeitung: 0.22 Sekunden (vorverarbeitet) ¤

Bilder Diashow
Bilder sprechenden Kalenders
Eigene Datei ansehen

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.