programs: examples

parent 41659db7
(* Fibonacci function with memoisation *)
{
logic fib (n:int) : int =
if n <= 1 then 1 else fib (n-1) + fib (n-2)
type option 'a = None | Some 'a
type table 'a 'b
logic get (table 'a 'b) 'a : option 'b
logic set (table 'a 'b) 'a 'b : table 'a 'b
axiom Select_eq :
forall m : table 'a 'b. forall a1 a2 : 'a. forall b : 'b.
a1 = a2 -> get (set m a1 b) a2 = Some b
use array.Array as A
axiom Select_neq :
forall m : table 'a 'b. forall a1 a2 : 'a. forall b : 'b.
a1 <> a2 -> get (set m a1 b) a2 = get m a2
type table 'a 'b = A.t 'a (option 'b)
logic inv (t : table int int) =
forall x y : int. get t x = Some y -> y = fib x
forall x y : int. A.select t x = Some y -> y = fib x
}
parameter table : ref (table int int)
parameter add :
x:int -> y:int -> {} unit writes table { !table = set (old !table) x y }
x:int -> y:int ->
{} unit writes table { !table = A.store (old !table) x (Some y) }
exception Not_found
......@@ -33,20 +27,22 @@ parameter find :
x:int ->
{}
int reads table raises Not_found
{ get !table x = Some result } | Not_found -> { get !table x = None }
{ A.select !table x = Some result }
| Not_found -> { A.select !table x = None }
let rec fibo n =
{ 0 <= n and inv(!table) }
{ 0 <= n and inv !table }
if n <= 1 then
1
else memo_fibo (n-1) + memo_fibo (n-2)
{ result = fib n and inv(!table) }
else
memo_fibo (n-1) + memo_fibo (n-2)
{ result = fib n and inv !table }
and memo_fibo n =
{ 0 <= n and inv(!table) }
try find n
{ 0 <= n and inv !table }
try find n
with Not_found -> let fn = fibo n in add n fn; fn end
{ result = fib n and inv(!table) }
{ result = fib n and inv !table }
(*
Local Variables:
......
......@@ -10,40 +10,39 @@
logic sum_digits (n:int) : int =
if n = 0 then 0 else sum_digits (div n 10) + mod n 10
(* the number of n st 0 <= n mod 10 < c and sd(n) = sd(137n+a)+b *)
type int3 = (int,int,int)
logic pr1 (d:int3) (n:int) =
logic p (d:int3) (n:int) =
let (a,b,c) = d in
mod n 10 = c and sum_digits n = sum_digits (137 * n + a) + b
0 <= mod n 10 < c and sum_digits n = sum_digits (137 * n + a) + b
clone int.NumOfParam as P1 with type param = int3, logic pr = pr1
clone int.NumOfParam as P with type param = int3, logic pr = p
logic pr2 (d:int3) (n:int) =
let (a,b,c) = d in
0 <= mod n 10 < c and sum_digits n = sum_digits (137 * n + a) + b
logic solution(a b m : int) : int = P.num_of (a,b,10) 0 (power 10 m)
clone int.NumOfParam as P2 with type param = int3, logic pr = pr2
(* short cut for the number of n st n mod 10 = c and ... *)
logic solution(a b m : int) : int = P2.num_of (a,b,10) 0 (power 10 m)
logic num_of_modc (d:int3) (x y:int) : int =
let (a,b,c) = d in
P.num_of (a,b,c+1) x y - P.num_of (a,b,c) x y
(* helper lemmas *)
lemma Base00:
forall a b : int. 0 <= a -> sum_digits a + b = 0 -> pr2 (a,b,10) 0
lemma Base:
forall a b : int. 0 <= a -> sum_digits a + b = 0 -> p (a,b,10) 0
lemma Empty:
forall a b x y : int. P2.num_of (a,b,0) x y = 0
forall a b x y : int. P.num_of (a,b,0) x y = 0
lemma Induc1:
forall a b c : int. 0 <= a -> 0 <= c < 10 ->
forall x y : int.
P2.num_of (a,b,c+1) x y = P2.num_of (a,b,c) x y + P1.num_of (a,b,c) x y
lemma Induc2:
lemma Induc:
forall a b c : int. 0 <= a -> 0 <= c < 10 ->
let x = 137 * c + a in
let a' = div x 10 in
let b' = mod x 10 + b - c in
forall m : int. m > 0 ->
P1.num_of (a,b,c) 0 (power 10 m) = P2.num_of (a', b', 10) 0 (power 10 (m-1))
solution a' b' (m-1) = num_of_modc (a,b,c) 0 (power 10 m)
}
......@@ -67,12 +66,12 @@ let rec f m a b =
let sum = ref 0 in
let c = ref 0 in
while !c <= 9 do (* n = 10n' + c *)
invariant { 0 <= !c <= 10 and !sum = P2.num_of (a,b,!c) 0 (power 10 m) }
invariant { 0 <= !c <= 10 and !sum = P.num_of (a,b,!c) 0 (power 10 m) }
variant { 10 - !c }
let x = 137 * !c + a in
let a' = div x 10 in
let c' = mod x 10 in
sum := !sum + f (m-1) a' (c' + b - !c);
let q = div x 10 in
let r = mod x 10 in
sum := !sum + f (m-1) q (r + b - !c);
c := !c + 1
done;
!sum
......
......@@ -127,6 +127,10 @@ theory NumOfParam
forall p : param, a b c : int.
a <= b <= c -> num_of p a c = num_of p a b + num_of p b c
axiom Empty :
forall p : param, a b : int.
(forall n : int. a <= n < b -> not pr p n) -> num_of p a b = 0
end
theory NumOf
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment