playing with ghost code

parent 03bb57a2
......@@ -11,24 +11,23 @@ module M
predicate inv (a : array int) =
a[0] = 0 /\ length a = 11 /\ forall k:int. 1 <= k <= 10 -> 0 < a[k]
val loop1 : ref int
val loop2 : ref int
val ghost loop1 : ref int
val ghost loop2 : ref int
let insertion_sort () =
{ inv a /\
(* ghost *) !loop1 = 0 /\ !loop2 = 0 }
{ inv a /\ !loop1 = 0 /\ !loop2 = 0 }
let i = ref 2 in
while !i <= 10 do
invariant { 2 <= !i <= 11 /\ inv a /\
(* ghost *) !loop1 = !i - 2 /\ 2 * !loop2 <= (!i-2) * (!i-1) }
!loop1 = !i - 2 /\ 2 * !loop2 <= (!i-2) * (!i-1) }
variant { 10 - !i }
(* ghost *) incr loop1;
ghost incr loop1;
let j = ref !i in
while a[!j] < a[!j - 1] do
invariant { 1 <= !j <= !i /\ inv a /\
(* ghost *) 2 * !loop2 <= (!i-2) * (!i-1) + 2*(!i - !j) }
2 * !loop2 <= (!i-2) * (!i-1) + 2*(!i - !j) }
variant { !j }
(* ghost *) incr loop2;
ghost incr loop2;
let temp = a[!j] in
a[!j] <- a[!j - 1];
a[!j - 1] <- temp;
......@@ -122,7 +121,7 @@ module InsertionSortExample
let path_init_l2 () =
{ separation !fp /\ inv !mem }
(* ghost *) l4 := 0; l7 := 0;
l4 := 0; l7 := 0;
r3 := 2;
str r3 (!fp - 16)
{ inv_l2 !mem !fp !l4 }
......
......@@ -97,11 +97,12 @@ module NQueensSets
use import module ref.Refint
use import Solution
val col: ref solution (* solution under construction *)
val k : ref int (* current row in the current solution *)
val ghost col: ref solution (* solution under construction *)
val ghost k : ref int (* current row in the current solution *)
val sol: ref solutions (* all solutions *)
val s : ref int (* next slot for a solution = number of solutions *)
val ghost sol: ref solutions (* all solutions *)
val ghost s : ref int (* next slot for a solution
= current number of solutions *)
let rec t3 (a b c : set int) variant { cardinal a } =
{ 0 <= !k /\ !k + cardinal a = n /\ !s >= 0 /\
......@@ -131,16 +132,16 @@ module NQueensSets
eq_prefix (at !sol 'L) !sol (at !s 'L) }
variant { cardinal !e }
let d = min_elt !e in
(* ghost *) col := !col[!k <- d];
(* ghost *) incr k;
ghost col := !col[!k <- d];
ghost incr k;
f += t3 (remove d a) (succ (add d b)) (pred (add d c));
(* ghost *) decr k;
ghost decr k;
e := remove d !e
done;
!f
end else begin
(* ghost *) sol := !sol[!s <- !col];
(* ghost *) incr s;
ghost sol := !sol[!s <- !col];
ghost incr s;
1
end
{ result = !s - old !s >= 0 /\ !k = old !k /\
......@@ -270,16 +271,16 @@ module NQueensBits
eq_prefix (at !sol 'L) !sol (at !s 'L) }
variant { cardinal (bits !e) }
let d = !e & (- !e) in
(* ghost *) col := !col[!k <- min_elt d];
(* ghost *) incr k;
ghost col := !col[!k <- min_elt d];
ghost incr k;
f += t (a - d) ((b+d) * 2) ((c+d)/2);
(* ghost *) decr k;
ghost decr k;
e -= d
done;
!f
end else begin
(* ghost *) sol := !sol[!s <- !col];
(* ghost *) incr s;
ghost sol := !sol[!s <- !col];
ghost incr s;
1
end
{ result = !s - old !s >= 0 /\ !k = old !k /\
......
module TestGhost
use import ref.Ref
val x: ref int
let test1 () =
{}
ghost x := 0;
()
{ !x = 0 }
end
module Johannes
type a = {| mutable f1 : int |}
......
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