new example: Hillel challenge

parent 8b02eb33
(** {1 Hillel challenge}
See https://www.hillelwayne.com/post/theorem-prover-showdown/
*)
module Leftpad
use import int.Int
use import int.MinMax
use import array.Array
type char (* whatever it is *)
type string = array char
let leftpad (pad: char) (n: int) (s: string) : string
ensures { length result = max n (length s) }
ensures { forall i. 0 <= i < length result - length s -> result[i] = pad }
ensures { forall i. 0 <= i < length s ->
result[length result - 1 - i] = s[length s - 1 - i] }
= let len = max n (length s) in
let res = Array.make len pad in
Array.blit s 0 res (len - length s) (length s);
res
end
module Unique
use import int.Int
use import ref.Refint
clone hashtbl.Hashtbl with type key = int
use import array.Array
predicate mem (x: int) (a: array int) (i: int) =
exists j. 0 <= j < i /\ a[j] = x
predicate hmem (x: int) (h: Hashtbl.t unit) =
Hashtbl.contents h x <> Hashtbl.List.Nil
let unique (a: array int) : array int
ensures { forall x. mem x result (length result) <-> mem x a (length a) }
ensures { forall i j. 0 <= i < j < length result -> result[i] <> result[j] }
= let n = length a in
let h = Hashtbl.create n in
let res = Array.make n 0 in
let len = ref 0 in
for i = 0 to n - 1 do
invariant { 0 <= !len <= i }
invariant { forall x. mem x a i <-> hmem x h }
invariant { forall x. mem x a i <-> mem x res !len }
invariant { forall i j. 0 <= i < j < !len -> res[i]<>res[j] }
if not (Hashtbl.mem h a[i]) then begin
Hashtbl.add h a[i] ();
res[!len] <- a[i];
incr len
end
done;
Array.sub res 0 !len
end
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="5">
<prover id="0" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="1" name="Z3" version="4.4.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../hillel_challenge.mlw" proved="true">
<theory name="Leftpad" proved="true">
<goal name="VC leftpad" expl="VC for leftpad" proved="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
</theory>
<theory name="Unique" proved="true">
<goal name="VC unique" expl="VC for unique" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC unique.0" expl="array creation size" proved="true">
<proof prover="0"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC unique.1" expl="loop invariant init" proved="true">
<proof prover="0"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC unique.2" expl="loop invariant init" proved="true">
<proof prover="0"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC unique.3" expl="loop invariant init" proved="true">
<proof prover="0"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC unique.4" expl="loop invariant init" proved="true">
<proof prover="0"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC unique.5" expl="index in array bounds" proved="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC unique.6" expl="index in array bounds" proved="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC unique.7" expl="index in array bounds" proved="true">
<proof prover="0"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC unique.8" expl="index in array bounds" proved="true">
<proof prover="0"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC unique.9" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC unique.10" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.59"/></proof>
</goal>
<goal name="VC unique.11" expl="loop invariant preservation" proved="true">
<transf name="case" proved="true" arg1="(x=o)">
<goal name="VC unique.11.0" expl="true case (loop invariant preservation)" proved="true">
<proof prover="2"><result status="valid" time="0.01" steps="88"/></proof>
</goal>
<goal name="VC unique.11.1" expl="false case (loop invariant preservation)" proved="true">
<transf name="assert" proved="true" arg1="(mem x a (i+1) &lt;-&gt; mem x a i)">
<goal name="VC unique.11.1.0" proved="true">
<proof prover="0"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC unique.11.1.1" expl="false case (loop invariant preservation)" proved="true">
<proof prover="2"><result status="valid" time="0.02" steps="105"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="VC unique.12" expl="loop invariant preservation" proved="true">
<transf name="case" proved="true" arg1="(j &lt; len-1)">
<goal name="VC unique.12.0" expl="true case (loop invariant preservation)" proved="true">
<proof prover="2"><result status="valid" time="0.01" steps="44"/></proof>
</goal>
<goal name="VC unique.12.1" expl="false case (loop invariant preservation)" proved="true">
<transf name="assert" proved="true" arg1="(not (mem o a i1))">
<goal name="VC unique.12.1.0" proved="true">
<proof prover="0"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC unique.12.1.1" expl="false case (loop invariant preservation)" proved="true">
<proof prover="2"><result status="valid" time="0.01" steps="50"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="VC unique.13" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC unique.14" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC unique.15" expl="loop invariant preservation" proved="true">
<transf name="case" proved="true" arg1="(x = o)">
<goal name="VC unique.15.0" expl="true case (loop invariant preservation)" proved="true">
<proof prover="2"><result status="valid" time="0.02" steps="54"/></proof>
</goal>
<goal name="VC unique.15.1" expl="false case (loop invariant preservation)" proved="true">
<transf name="assert" proved="true" arg1="(mem x a (i+1) &lt;-&gt; mem x a i)">
<goal name="VC unique.15.1.0" proved="true">
<proof prover="0"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC unique.15.1.1" expl="false case (loop invariant preservation)" proved="true">
<proof prover="2"><result status="valid" time="0.02" steps="25"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="VC unique.16" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC unique.17" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC unique.18" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC unique.19" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC unique.20" expl="out of loop bounds" proved="true">
<proof prover="0"><result status="valid" time="0.04"/></proof>
</goal>
</transf>
</goal>
</theory>
</file>
</why3session>
......@@ -240,7 +240,7 @@ module RandomAccessListWithSeq
if mod i 2 = 0 then x0 else x1
end
let rec tail (l: ral 'a) : ral 'a
let rec tail (l: ral 'a) : ral 'a
requires { 0 < length (elements l) }
variant { l }
ensures { elements result == (elements l)[1..] }
......
......@@ -176,10 +176,10 @@
<goal name="VC fupdate.6" expl="assertion" proved="true">
<transf name="split_goal_right" proved="true" >
<goal name="VC fupdate.6.0" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.16" steps="235"/></proof>
<proof prover="3"><result status="valid" time="0.30" steps="235"/></proof>
</goal>
<goal name="VC fupdate.6.1" expl="VC for fupdate" proved="true">
<proof prover="3"><result status="valid" time="0.92" steps="1299"/></proof>
<proof prover="3"><result status="valid" time="1.00" steps="1299"/></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