| products/sources/formale Sprachen/PVS/exact_real_arith/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: bisection_nat_sqrt.pvs Sprache: PVSOriginal 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.1 Sekunden (vorverarbeitet) ¤ |
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 |
