Commit 5aa12d33 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Fix some documentation.

parent 1827453a
......@@ -26,7 +26,7 @@ module GmpModel
type memory = array int
val m: memory
(** invariant: each cell contains an integer in [0..beta[ *)
(** invariant: each cell contains an integer in [\[0..beta\[] *)
type pointer = int
type size = int
......@@ -38,11 +38,11 @@ module GmpModel
p1 + s1 <= p2 \/ p2 + s2 <= p1
function i (m: memory) (p: pointer) (s: size) : int
(** the GMP integer in m[p..p+s[ *)
(** the GMP integer in [m\[p..p+s\[] *)
predicate modifies (m1 m2: memory) (p: pointer) (s: size) =
forall q: pointer. (q < p \/ p + s <= q) -> m2[q] = m1[q]
(** nothing modified apart from [p..p+s[ *)
(** nothing modified apart from [\[p..p+s\[] *)
axiom frame:
forall m1 m2: memory, p: pointer, s: size.
......@@ -53,7 +53,7 @@ module GmpModel
(p1: pointer) (s1: size) (p2: pointer) (s2: size) =
forall q: pointer. ( (q < p1 \/ p1 + s1 <= q)
/\ (q < p2 \/ p2 + s2 <= q)) -> m2[q] = m1[q]
(** nothing modified apart from [p1..p1+s1[ and [p2..p2+s2[ *)
(** nothing modified apart from [\[p1..p1+s1\[] and [\[p2..p2+s2\[] *)
axiom frame2:
forall m1 m2: memory, p1 p2: pointer, s1 s2: size.
......
......@@ -6,8 +6,8 @@
Verification of the following 2-lines C program solving the N-queens problem:
{h <pre>
t(a,b,c){int d=0,e=a&~b&~c,f=1;if(a)for(f=0;d=(e-=d)&-e;f+=t(a-d,(b+d)*2,(
c+d)/2));return f;}main(q){scanf("%d",&q);printf("%d\n",t(~(~0<<q),0,0));}
t(a,b,c){int d=0,e=a&amp;~b&amp;~c,f=1;if(a)for(f=0;d=(e-=d)&amp;-e;f+=t(a-d,(b+d)*2,(
c+d)/2));return f;}main(q){scanf("%d",&amp;q);printf("%d\n",t(~(~0&lt;&lt;q),0,0));}
</pre>}
*)
......@@ -46,7 +46,7 @@ theory Solution
type solution = map int int
(** solutions [t] and [u] have the same prefix [[0..i[] *)
(** solutions [t] and [u] have the same prefix [\[0..i\[] *)
predicate eq_prefix (t u: map int 'a) (i: int) =
forall k: int. 0 <= k < i -> t[k] = u[k]
......@@ -71,7 +71,7 @@ theory Solution
type solutions = map int solution
(** [s[a..b[] is sorted for [lt_sol] *)
(** [s\[a..b\[] is sorted for [lt_sol] *)
predicate sorted (s: solutions) (a b: int) =
forall i j: int. a <= i < j < b -> lt_sol s[i] s[j]
......
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