Commit 3082132d authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

zeros: yet another program

parent 6ebd407c
......@@ -88,4 +88,25 @@ module AllZeros
in
check_from 0
(** divide-and-conqueer *)
predicate zero_interval (a: array int) (lo hi: int) =
forall i: int. lo <= i < hi -> a[i] = 0
use import int.ComputerDivision
let all_zeros5 (a: array int) : bool
ensures { result <-> all_zeros a a.length }
=
let rec check_between (lo hi: int) : bool
requires { 0 <= lo <= hi <= a.length }
variant { hi - lo }
ensures { result <-> zero_interval a lo hi }
=
hi <= lo ||
let mid = lo + div (hi - lo) 2 in
a[mid] = 0 && check_between lo mid && check_between (mid+1) hi
in
check_between 0 (Array.length a)
end
......@@ -45,7 +45,7 @@
</transf>
</goal>
</theory>
<theory name="AllZeros" sum="1d320632b50748c7da056f42e9fe27a9" expanded="true">
<theory name="AllZeros" sum="4d522333682d37ebf90b16bbe3ff5d1b" 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>
......@@ -58,6 +58,9 @@
<goal name="WP_parameter all_zeros4" expl="VC for all_zeros4" expanded="true">
<proof prover="3"><result status="valid" time="0.02" steps="50"/></proof>
</goal>
<goal name="WP_parameter all_zeros5" expl="VC for all_zeros5" expanded="true">
<proof prover="3" timelimit="61"><result status="valid" time="0.88" steps="292"/></proof>
</goal>
</theory>
</file>
</why3session>
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