gallery: simple verification exercises

examples/zeros.mlw

 
+(** Setting all the elements of an array to zero *)
+
 module SetZeros
 
   use import int.Int
@@ -18,3 +20,72 @@ module SetZeros
     assert { a0[12] = 0 }
 
 end
+
+(** Checking that an array contains only zeros *)
+
+module AllZeros
+
+  use import int.Int
+  use import array.Array
+  use import ref.Refint
+
+  predicate all_zeros (a: array int) (hi: int) =
+    forall i: int. 0 <= i < hi -> a[i] = 0
+
+  (** with a for loop (a bit naive, since it always scans the whole array) *)
+
+  let all_zeros1 (a: array int) : bool
+    ensures { result <-> all_zeros a a.length }
+  =
+    let res = ref True in
+    for i = 0 to length a - 1 do
+      invariant { !res <-> all_zeros a i }
+      if a[i] <> 0 then res := False
+    done;
+    !res
+
+  (** with a while loop, stopping as early as possible *)
+
+  let all_zeros2 (a: array int) : bool
+    ensures { result <-> all_zeros a a.length }
+  =
+    let res = ref True in
+    let i = ref 0 in
+    while !res && !i < length a do
+      invariant { 0 <= !i <= a.length }
+      invariant { !res <-> all_zeros a !i }
+      variant   { a.length - !i }
+      res := (a[!i] = 0);
+      incr i
+    done;
+    !res
+
+  (** no need for a Boolean variable, actually *)
+
+  let all_zeros3 (a: array int) : bool
+    ensures { result <-> all_zeros a a.length }
+  =
+    let i = ref 0 in
+    while !i < length a && a[!i] = 0 do
+      invariant { 0 <= !i <= a.length }
+      invariant { all_zeros a !i }
+      variant   { a.length - !i }
+      incr i
+    done;
+    !i = length a
+
+  (** with a recursive function *)
+
+  let all_zeros4 (a: array int) : bool
+    ensures { result <-> all_zeros a a.length }
+  =
+    let rec check_from (i: int) : bool
+      requires { 0 <= i <= a.length }
+      requires { all_zeros a i }
+      variant  { a.length - i }
+      ensures  { result <-> all_zeros a a.length }
+    = i = length a || a[i] = 0 && check_from (i+1)
+    in
+    check_from 0
+
+end

examples/zeros/why3session.xml

@@ -5,44 +5,59 @@
 <prover id="0" name="CVC3" version="2.4.1" timelimit="10" memlimit="0"/>
 <prover id="1" name="Alt-Ergo" version="0.95.1" timelimit="10" memlimit="1000"/>
 <prover id="2" name="Z3" version="2.19" timelimit="10" memlimit="0"/>
+<prover id="3" name="Alt-Ergo" version="0.99.1" timelimit="6" memlimit="1000"/>
 <file name="../zeros.mlw" expanded="true">
-<theory name="SetZeros" sum="60a48f611ed3b9df1a065d4e414c9408" expanded="true">
- <goal name="WP_parameter set_zeros" expl="VC for set_zeros" expanded="true">
- <transf name="split_goal_wp" expanded="true">
-  <goal name="WP_parameter set_zeros.1" expl="1. postcondition" expanded="true">
+<theory name="SetZeros" sum="60a48f611ed3b9df1a065d4e414c9408">
+ <goal name="WP_parameter set_zeros" expl="VC for set_zeros">
+ <transf name="split_goal_wp">
+  <goal name="WP_parameter set_zeros.1" expl="1. postcondition">
   <proof prover="1" memlimit="0"><result status="valid" time="0.00"/></proof>
   </goal>
-  <goal name="WP_parameter set_zeros.2" expl="2. loop invariant init" expanded="true">
+  <goal name="WP_parameter set_zeros.2" expl="2. loop invariant init">
   <proof prover="1" memlimit="0"><result status="valid" time="0.01"/></proof>
   </goal>
   <goal name="WP_parameter set_zeros.3" expl="3. type invariant">
   <proof prover="1" timelimit="5"><result status="valid" time="0.01"/></proof>
   </goal>
-  <goal name="WP_parameter set_zeros.4" expl="4. index in array bounds" expanded="true">
+  <goal name="WP_parameter set_zeros.4" expl="4. index in array bounds">
   <proof prover="1" timelimit="5"><result status="valid" time="0.01"/></proof>
   </goal>
-  <goal name="WP_parameter set_zeros.5" expl="5. loop invariant preservation" expanded="true">
+  <goal name="WP_parameter set_zeros.5" expl="5. loop invariant preservation">
   <proof prover="0"><result status="valid" time="0.00"/></proof>
   <proof prover="2"><result status="valid" time="0.02"/></proof>
   </goal>
   <goal name="WP_parameter set_zeros.6" expl="6. type invariant">
   <proof prover="1" timelimit="5"><result status="valid" time="0.01"/></proof>
   </goal>
-  <goal name="WP_parameter set_zeros.7" expl="7. postcondition" expanded="true">
+  <goal name="WP_parameter set_zeros.7" expl="7. postcondition">
   <proof prover="1" memlimit="0"><result status="valid" time="0.01"/></proof>
   </goal>
  </transf>
  </goal>
- <goal name="WP_parameter harness" expl="VC for harness" expanded="true">
- <transf name="split_goal_wp" expanded="true">
-  <goal name="WP_parameter harness.1" expl="1. array creation size" expanded="true">
+ <goal name="WP_parameter harness" expl="VC for harness">
+ <transf name="split_goal_wp">
+  <goal name="WP_parameter harness.1" expl="1. array creation size">
   <proof prover="1" memlimit="0"><result status="valid" time="0.00"/></proof>
   </goal>
-  <goal name="WP_parameter harness.2" expl="2. assertion" expanded="true">
+  <goal name="WP_parameter harness.2" expl="2. assertion">
   <proof prover="1" memlimit="0"><result status="valid" time="0.00"/></proof>
   </goal>
  </transf>
  </goal>
 </theory>
+<theory name="AllZeros" sum="791471af260f297a97e7cb2b0aadbc4e" expanded="true">
+ <goal name="WP_parameter all_zeros1" expl="VC for all_zeros1" expanded="true">
+ <proof prover="3"><result status="valid" time="0.02" steps="104"/></proof>
+ </goal>
+ <goal name="WP_parameter all_zeros2" expl="VC for all_zeros2" expanded="true">
+ <proof prover="3"><result status="valid" time="0.00" steps="72"/></proof>
+ </goal>
+ <goal name="WP_parameter all_zeros3" expl="VC for all_zeros3" expanded="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="42"/></proof>
+ </goal>
+ <goal name="WP_parameter all_zeros4" expl="VC for all_zeros4" expanded="true">
+ <proof prover="3"><result status="valid" time="0.02" steps="52"/></proof>
+ </goal>
+</theory>
 </file>
 </why3session>