Quelle bisection_nat_sqrt.pvs Sprache: 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

quality93%

¤ Dauer der Verarbeitung: 0.9 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.