muller example: simplified invariants

parent 715be130
...@@ -18,13 +18,13 @@ module Muller ...@@ -18,13 +18,13 @@ module Muller
let compact (a: array int) = let compact (a: array int) =
let count = ref 0 in let count = ref 0 in
for i = 0 to length a - 1 do for i = 0 to length a - 1 do
invariant { 0 <= !count = numof a 0 i <= i} invariant { !count = numof a 0 i }
if a[i] <> 0 then incr count if a[i] <> 0 then incr count
done; done;
let u = make !count 0 in let u = make !count 0 in
count := 0; count := 0;
for i = 0 to length a - 1 do for i = 0 to length a - 1 do
invariant { 0 <= !count = numof a 0 i <= i } invariant { !count = numof a 0 i }
if a[i] <> 0 then begin u[!count] <- a[i]; incr count end if a[i] <> 0 then begin u[!count] <- a[i]; incr count end
done done
......
...@@ -6,7 +6,7 @@ ...@@ -6,7 +6,7 @@
<file name="../muller.mlw" proved="true"> <file name="../muller.mlw" proved="true">
<theory name="Muller" proved="true"> <theory name="Muller" proved="true">
<goal name="VC compact" expl="VC for compact" proved="true"> <goal name="VC compact" expl="VC for compact" proved="true">
<proof prover="1"><result status="valid" time="0.27" steps="743"/></proof> <proof prover="1"><result status="valid" time="0.14" steps="429"/></proof>
</goal> </goal>
</theory> </theory>
</file> </file>
......
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