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

new example: minimum excludant

parent dd2efcbf
(* {1 Minimum excludant, aka mex}
Given a finite set of integers, find the smallest nonnegative integer
that does not belong to this set.
*)
module MexArray
use import int.Int
use import map.Map
use import array.Array
use import ref.Refint
use import pigeon.Pigeonhole
predicate mem (x: int) (a: array int) =
exists i. 0 <= i < length a && a[i] = x
let mex (a: array int) : int
ensures { 0 <= result <= length a }
ensures { not (mem result a) }
ensures { forall x. 0 <= x < result -> mem x a }
= let n = length a in
let used = make n false in
let ghost idx = ref (fun i -> i) in
for i = 0 to n - 1 do
invariant { forall x. 0 <= x < n -> used[x] ->
mem x a && 0 <= !idx x < n && a[!idx x] = x }
invariant { forall j. 0 <= j < i -> 0 <= a[j] < n ->
used[a[j]] && 0 <= !idx a[j] < n && a[!idx a[j]] = a[j] }
let x = a[i] in
if 0 <= x && x < n then begin used[x] <- true; idx := set !idx x i end
done;
let r = ref 0 in
let ghost posn = ref (-1) in
while !r < n && used[!r] do
invariant { 0 <= !r <= n }
invariant { forall j. 0 <= j < !r -> used[j] && 0 <= !idx j < n }
invariant { if !posn >= 0 then 0 <= !posn < n && a[!posn] = n
else forall j. 0 <= j < !r -> a[j] <> n }
variant { n - !r }
if a[!r] = n then posn := !r;
incr r
done;
if !r = n && !posn >= 0 then pigeonhole (n+1) n (set !idx n !posn);
!r
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="4">
<prover id="1" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../mex.mlw" proved="true">
<theory name="MexArray" proved="true">
<goal name="VC mex" expl="VC for mex" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC mex.0" expl="array creation size" proved="true">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC mex.1" expl="loop invariant init" proved="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC mex.2" expl="loop invariant init" proved="true">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC mex.3" expl="index in array bounds" proved="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC mex.4" expl="index in array bounds" proved="true">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC mex.5" expl="loop invariant preservation" proved="true">
<proof prover="2"><result status="valid" time="0.07" steps="204"/></proof>
</goal>
<goal name="VC mex.6" expl="loop invariant preservation" proved="true">
<proof prover="2"><result status="valid" time="0.01" steps="41"/></proof>
</goal>
<goal name="VC mex.7" expl="loop invariant preservation" proved="true">
<proof prover="2"><result status="valid" time="0.00" steps="27"/></proof>
</goal>
<goal name="VC mex.8" expl="loop invariant preservation" proved="true">
<proof prover="2"><result status="valid" time="0.01" steps="35"/></proof>
</goal>
<goal name="VC mex.9" expl="loop invariant init" proved="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC mex.10" expl="loop invariant init" proved="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC mex.11" expl="loop invariant init" proved="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC mex.12" expl="index in array bounds" proved="true">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC mex.13" expl="index in array bounds" proved="true">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC mex.14" expl="loop variant decrease" proved="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC mex.15" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC mex.16" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC mex.17" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC mex.18" expl="loop variant decrease" proved="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC mex.19" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC mex.20" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC mex.21" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC mex.22" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC mex.23" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC mex.24" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC mex.25" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.03" steps="85"/></proof>
</goal>
<goal name="VC mex.26" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC mex.27" expl="out of loop bounds" proved="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
</transf>
</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