more return types with names in the gallery

parent 96b8a02e
......@@ -35,9 +35,9 @@ module Division
use import int.Int
use import ref.Ref
let division (x: int) (y: int)
let division (x: int) (y: int) : (q: int, r: int)
requires { 0 <= x /\ 0 < y }
returns { q, r -> 0 <= r < y /\ x = q * y + r }
ensures { 0 <= r < y /\ x = q * y + r }
= let q = ref 0 in
let r = ref x in
while !r >= y do
......
......@@ -15,13 +15,13 @@ module TwoEqualElements
exists i: int. 0 <= i < u /\ a[i] = v /\
exists j: int. 0 <= j < u /\ j <> i /\ a[j] = v
let two_equal_elements (a: array int) (n: int)
let two_equal_elements (a: array int) (n: int) : (v1:int, v2:int)
requires { length a = n+2 /\ n >= 2 }
requires { forall i: int. 0 <= i < length a -> 0 <= a[i] < n }
requires {
exists v1: int. appear_twice a v1 (n+2) /\
exists v2: int. appear_twice a v2 (n+2) /\ v2 <> v1 }
returns { v1, v2 ->
ensures {
appear_twice a v1 (n+2) /\ appear_twice a v2 (n+2) /\ v1 <> v2 }
= let deja_vu = make n False in
let v1 = ref (-1) in
......
......@@ -36,12 +36,10 @@ module TortoiseAndHareAlgorithm
(* First, we prove the existence of mu and lambda, with a ghost program.
Starting with x0, we repeatedly apply f, storing the elements in
a sequence, until we find a repetition. *)
let ghost periodicity () : (int, int)
returns { mu, lambda ->
0 <= mu < m /\ 1 <= lambda <= m /\ mu + lambda <= m /\
x (mu + lambda) = x mu /\
forall i j. 0 <= i < j < mu + lambda -> x i <> x j
}
let ghost periodicity () : (mu:int, lambda:int)
ensures { 0 <= mu < m /\ 1 <= lambda <= m /\ mu + lambda <= m /\
x (mu + lambda) = x mu }
ensures { forall i j. 0 <= i < j < mu + lambda -> x i <> x j }
= let s = ref (singleton x0) in
let cur = ref x0 in
for k = 1 to m do
......@@ -75,9 +73,9 @@ module TortoiseAndHareAlgorithm
ensures { x (n + k * lambda) = x n } =
if k > 0 then begin
plus_lambdas n (k - 1); plus_lambda (n + (k - 1) * lambda) end in
let decomp (i: int) : (int, int)
let decomp (i: int) : (qi:int, mi:int)
requires { i >= mu }
returns { qi,mi -> i = mu + qi * lambda + mi && qi >= 0 &&
ensures { i = mu + qi * lambda + mi && qi >= 0 &&
0 <= mi < lambda && x i = x (mu + mi) } =
let qi = div (i - mu) lambda in
let mi = mod (i - mu) lambda in
......@@ -96,12 +94,10 @@ module TortoiseAndHareAlgorithm
(* Finally, we implement the tortoise and hare algorithm that computes
the values of mu and lambda in linear time and constant space *)
let tortoise_and_hare () : (int, int)
returns { mu, lambda ->
0 <= mu < m /\ 1 <= lambda <= m /\ mu + lambda <= m /\
x (mu + lambda) = x mu /\
forall i j. 0 <= i < j < mu + lambda -> x i <> x j
}
let tortoise_and_hare () : (mu:int, lambda:int)
ensures { 0 <= mu < m /\ 1 <= lambda <= m /\ mu + lambda <= m /\
x (mu + lambda) = x mu }
ensures { forall i j. 0 <= i < j < mu + lambda -> x i <> x j }
= let mu, lambda = periodicity () in
equality mu lambda;
(* the first loop implements the tortoise and hare,
......
......@@ -28,34 +28,37 @@
<goal name="VC periodicity.3" expl="loop invariant init" proved="true">
<proof prover="2"><result status="valid" time="0.01" steps="16"/></proof>
</goal>
<goal name="VC periodicity.4" expl="VC for periodicity" proved="true">
<goal name="VC periodicity.4" expl="postcondition" proved="true">
<proof prover="6"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC periodicity.5" expl="postcondition" proved="true">
<proof prover="6"><result status="valid" time="0.19"/></proof>
</goal>
<goal name="VC periodicity.5" expl="loop invariant preservation" proved="true">
<goal name="VC periodicity.6" expl="loop invariant preservation" proved="true">
<proof prover="6"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="VC periodicity.6" expl="precondition" proved="true">
<goal name="VC periodicity.7" expl="precondition" proved="true">
<proof prover="6"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC periodicity.7" expl="precondition" proved="true">
<goal name="VC periodicity.8" expl="precondition" proved="true">
<proof prover="6"><result status="valid" time="0.19"/></proof>
</goal>
<goal name="VC periodicity.8" expl="loop invariant preservation" proved="true">
<goal name="VC periodicity.9" expl="loop invariant preservation" proved="true">
<proof prover="6"><result status="valid" time="1.24"/></proof>
</goal>
<goal name="VC periodicity.9" expl="loop invariant preservation" proved="true">
<goal name="VC periodicity.10" expl="loop invariant preservation" proved="true">
<proof prover="2"><result status="valid" time="0.92" steps="823"/></proof>
</goal>
<goal name="VC periodicity.10" expl="loop invariant preservation" proved="true">
<goal name="VC periodicity.11" expl="loop invariant preservation" proved="true">
<proof prover="6"><result status="valid" time="0.16"/></proof>
</goal>
<goal name="VC periodicity.11" expl="VC for periodicity" proved="true">
<goal name="VC periodicity.12" expl="out of loop bounds" proved="true">
<proof prover="6"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC periodicity.12" expl="unreachable point" proved="true">
<goal name="VC periodicity.13" expl="unreachable point" proved="true">
<proof prover="6"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC periodicity.13" expl="unreachable point" proved="true">
<goal name="VC periodicity.14" expl="unreachable point" proved="true">
<proof prover="6"><result status="valid" time="0.06"/></proof>
</goal>
</transf>
......@@ -365,7 +368,10 @@
</transf>
</goal>
<goal name="VC tortoise_and_hare.27" expl="postcondition" proved="true">
<proof prover="5"><result status="valid" time="0.24"/></proof>
<proof prover="6"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC tortoise_and_hare.28" expl="postcondition" proved="true">
<proof prover="5"><result status="valid" time="0.03"/></proof>
</goal>
</transf>
</goal>
......
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