|
for_examples : THEORY
BEGIN
IMPORTING for_iterate,
ints@factorial
%% a = 1;
%% for (i=1; i <= n; i++) {
%% a = a*x;
%% }
expit(x:real,n:nat): real =
for[real](1,n,1,LAMBDA(i:subrange(1,n),a:real):a*x)
expit_test : LEMMA
expit(2,10) = 1024
%% Proved using for_induction.
%% Invariant is LAMBDA(i:upto(n),a:nat): a = x^i
expit_sound : LEMMA
FORALL(x:real,n:nat): expit(x,n) = x^n
%% a = 1;
%% for (i=n; i >= 1; i--) {
%% a = a*i;
%% }
factit(n:nat) : nat =
for_down[nat](n,1,1,LAMBDA(i:subrange(1,n),a:nat):a*i)
factit_test : LEMMA
factit(10) = 3628800
%% Proved using for_down_induction.
%% Invariant is LAMBDA(i:upto(n),a:nat): a = factorial(n)/factorial(n-i)
factit_sound : LEMMA
FORALL(n:nat): factit(n) = factorial(n)
%% a = nth(l,0);
%% for (i=1;i<=length(l)-1;i++) {
%% a = max(a,nth(l,i))
%% }
maxit(l:(cons?[real])) : real =
iterate_left(0,length(l)-1,LAMBDA(i:below(length(l))):nth(l,i),max)
maxit_test : LEMMA
maxit((:2,3,4,1,2:)) = 4
%% Proved using iterate_left_induction.
%% Invariant is LAMBDA(n:below(length(l)),a:real):FORALL(k:upto(n)) : nth(l,k) <= a
maxit_sound : LEMMA
FORALL (l:(cons?[real]),i:below(length(l))) :
nth(l,i) <= maxit(l)
%% a = nth(l,0);
%% for (i=1;i<=length(l)-1;i++) {
%% a = min(nth(l,i),a)
%% }
minit(l:(cons?[real])) : real =
iterate_right(0,length(l)-1,LAMBDA(i:below(length(l))):nth(l,i),min)
minit_test : LEMMA
minit((:2,3,4,1,2:)) = 1
%% Proved using iterate_right_induction.
%% Invariant is LAMBDA(n:below(length(l)),a:real): LET ll = length(l)-1 IN
%% FORALL(k:subrange(ll-n,ll)) :a <= nth(l,k)
minit_sound : LEMMA
FORALL (l:(cons?[real]),i:below(length(l))) :
minit(l) <= nth(l,i)
END for_examples
¤ Dauer der Verarbeitung: 0.24 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.
|
