more program examples

parent e6a5ae99
......@@ -3,22 +3,28 @@ module M
use import int.Int
use import module stdlib.Ref
logic sqr (x:int) : int = x * x
logic sqr (x:int) : int = x * x
let isqrt (x:int) =
{ x >= 0 }
let count = ref 0 in
let sum = ref 1 in
while !sum <= x do
invariant { count >= 0 and
x >= sqr count and
sum = sqr (count+1) }
variant { x - sum }
count := !count + 1;
sum := !sum + 2 * !count + 1
done;
!count
{ result >= 0 and sqr result <= x and x < sqr (result + 1) }
let isqrt (x:int) =
{ x >= 0 }
let count = ref 0 in
let sum = ref 1 in
while !sum <= x do
invariant { count >= 0 and x >= sqr count and sum = sqr (count+1) }
variant { x - sum }
count := !count + 1;
sum := !sum + 2 * !count + 1
done;
!count
{ result >= 0 and sqr result <= x and x < sqr (result + 1) }
let main () =
{ }
let r = isqrt 17 in
assert { r < 4 -> false };
assert { r > 4 -> false };
r
{ result = 4 }
end
......
module M
use import int.Int
use import int.ComputerDivision
use import int.Power
let rec fast_exp x n variant { n } =
{ 0 <= n }
if n = 0 then
1
else begin
let r = fast_exp x (div n 2) in
if mod n 2 = 0 then r * r else r * r * x
end
{ result = power x n }
use import module stdlib.Ref
let fast_exp_imperative x n =
{ 0 <= n }
let r = ref 1 in
let p = ref x in
let e = ref n in
while !e > 0 do
invariant { r * power x e = power x n }
variant { e }
if mod !e 2 = 1 then r := !r * !p;
p := !p * !p;
e := div !e 2
done;
!r
{ result = power x n }
end
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. examples/programs/power"
End:
*)
module M
(* VSTTE'10 competition http://www.macs.hw.ac.uk/vstte10/Competition.html
Problem 2: inverting an injection *)
use import int.Int
use import module stdlib.Ref
use array.ArrayLength as A
type array 'a = A.t int 'a
module M
logic (#) (a : array 'a) (i : int) : 'a = A.get a i
use import int.Int
use import module stdlib.Array
logic injective (a : array int) (n : int) =
forall i j : int. 0 <= i < n -> 0 <= j < n -> i <> j -> a#i <> a#j
logic injective (a : t int int) (n : int) =
forall i j : int. 0 <= i < n -> 0 <= j < n -> i <> j -> a[i] <> a[j]
logic surjective (a : array int) (n : int) =
forall i : int [i]. 0 <= i < n -> exists j : int. (0 <= j < n and a#j = i)
logic surjective (a : t int int) (n : int) =
forall i : int [i]. 0 <= i < n -> exists j : int. (0 <= j < n and a[j] = i)
logic range (a : array int) (n : int) =
forall i : int. 0 <= i < n -> 0 <= a#i < n
logic range (a : t int int) (n : int) =
forall i : int. 0 <= i < n -> 0 <= a[i] < n
lemma Injective_surjective :
forall a : array int, n : int.
forall a : t int int, n : int.
injective a n -> range a n -> surjective a n
let array_get (a : ref (array 'a)) i =
{ 0 <= i < A.length a } A.get !a i { result = A.get a i }
let array_set (a : ref (array 'a)) i v =
{ 0 <= i < A.length a } a := A.set !a i v { a = A.set (old a) i v }
let inverting (a : ref (array int)) (b : ref (array int)) n =
{ n >= 0 and A.length a = n and A.length b = n and
injective a n and range a n }
for i = 0 to n-1 do
invariant
{ A.length b = n and forall j : int. 0 <= j < i -> b#(a#j) = j }
array_set b (array_get a i) i
done
{ injective b n }
let inverting (a : array int) (b : array int) n =
{ n >= 0 and length a = n and length b = n and
injective a n and range a n }
for i = 0 to n-1 do
invariant
{ length b = n and forall j : int. 0 <= j < i -> b[a[j]] = j }
b[a[i] <- i]
done
{ injective b n }
end
......
module M
(* VSTTE'10 competition http://www.macs.hw.ac.uk/vstte10/Competition.html
Problem 1: max and sum of an array *)
module M
use import int.Int
use import module stdlib.Ref
use array.ArrayLength as A
type array 'a = A.t int 'a
logic (#) (a : array 'a) (i : int) : 'a = A.get a i
use import module stdlib.Array
let max_sum a n =
{ n >= 0 and forall i:int. 0 <= i < n -> a#i >= 0 }
let max_sum a n =
{ n >= 0 and length a = n and forall i:int. 0 <= i < n -> a[i] >= 0 }
let sum = ref 0 in
let max = ref 0 in
for i = 0 to n-1 do
invariant { sum <= i * max and forall j:int. 0 <= j < i -> a#j <= max }
if !max < a#i then max := a#i;
sum := !sum + a#i
invariant { sum <= i * max and forall j:int. 0 <= j < i -> a[j] <= max }
if !max < a[i] then max := a[i];
sum := !sum + a[i]
done;
(!sum, !max)
{ let (sum, max) = result in sum <= n * max }
......
module M
(* VSTTE'10 competition http://www.macs.hw.ac.uk/vstte10/Competition.html
Problem 3: searching a linked list *)
module M
use import int.Int
use import module stdlib.Ref
use export list.List
......
......@@ -96,15 +96,17 @@ theory Power
use import Int
(*
logic power (x n : int) : int =
if n = 0 then 1 else x * power x (n-1)
*)
logic power int int : int
(* FIXME: should we give a partial definition? *)
axiom Power_def : forall x n : int. power x n =
if n <= 0 then 1 else x * power x (n-1)
axiom Power_0 : forall x : int. power x 0 = 1
axiom Power_s : forall x n : int. 0 < n -> power x n = x * power x (n-1)
lemma Power_sum : forall x n m : int. 0 <= n -> 0 <= m ->
power x (n + m) = power x n * power x m
lemma Power_mult : forall x n m : int. 0 <= n -> 0 <= m ->
power x (n * m) = power (power x n) m
end
......@@ -206,6 +208,6 @@ end
(*
Local Variables:
compile-command: "../bin/why.opt int.why"
compile-command: "make -C .. theories/int.gui"
End:
*)
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