SSL for_examples.pvs

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