Commit d78b08e0 authored by Jean-Christophe's avatar Jean-Christophe
Browse files

vstte'10 competition : problem 2 almost completed (one VC not proved, but which should be)

parent 9453ec6f
next_digit_sum
vstte10_max_sum
vstte10_inverting
(* VSTTE'10 competition
Problem 2: inverting an injection *)
{
use array.ArrayLength as A
type array 'a = A.t int 'a
logic (#) (a : array 'a) (i : int) : 'a = A.get a i
logic injective (a : array 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. 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
lemma Injective_surjective :
forall a : array 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 b 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 }
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. examples/programs/vstte10_inverting.gui"
End:
*)
(* VSTTE'10 competition *)
(* VSTTE'10 competition
Problem 1: max and sum of an array *)
{
use array.ArrayLength as A
use import int.MinMax
type array 'a = A.t int 'a
......
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