programs: examples

parent 68b57f64
......@@ -11,19 +11,42 @@
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 [get (set m a1 b) a2].
forall m : table 'a 'b. forall a1 a2 : 'a. forall b : 'b.
a1 = a2 -> get (set m a1 b) a2 = Some b
axiom Select_neq :
forall m : table 'a 'b. forall a1 a2 : 'a.
forall b : 'b [get (set m a1 b) a2].
forall m : table 'a 'b. forall a1 a2 : 'a. forall b : 'b.
a1 <> a2 -> get (set m a1 b) a2 = get m a2
logic inv (t : table int int) =
forall x y : int. get 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 }
exception Not_found
parameter find :
x:int ->
{}
int reads table raises Not_found
{ get !table x = Some result } | Not_found -> { get !table x = None }
let rec fibo n =
{ 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) }
and memo_fibo 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) }
(*
Local Variables:
......
......@@ -12,15 +12,38 @@
type int3 = (int,int,int)
logic r (d:int3) (n:int) =
logic pr1 (d:int3) (n:int) =
let (a,b,c) = d in
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
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
clone int.NumOfParam as R with type param = int3, logic pr = r
clone int.NumOfParam as P2 with type param = int3, logic pr = pr2
logic solution(m : int) : int = R.num_of (0,0,10) 0 (power 10 m)
logic solution(a b m : int) : int = P2.num_of (a,b,10) 0 (power 10 m)
lemma Base00: forall a b : int. 0 <= a -> sum_digits a + b = 0 -> r (a,b,10) 0
lemma Base00:
forall a b : int. 0 <= a -> sum_digits a + b = 0 -> pr2 (a,b,10) 0
lemma Empty:
forall a b x y : int. P2.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:
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))
}
......@@ -41,11 +64,10 @@ let rec f m a b =
(* only n = 0 is possible *)
if sd a + b = 0 then 1 else 0
end else begin
absurd;
let sum = ref 0 in
let c = ref 0 in
while !c <= 9 do (* n = 10n' + c *)
invariant { 0 <= !c <= 10 and !sum = R.num_of (a,b,!c) 0 (power 10 m) }
invariant { 0 <= !c <= 10 and !sum = P2.num_of (a,b,!c) 0 (power 10 m) }
variant { 10 - !c }
let x = 137 * !c + a in
let a' = div x 10 in
......@@ -55,7 +77,7 @@ let rec f m a b =
done;
!sum
end
{ result = solution m }
{ result = solution a b m }
(*
......
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