Skip to content

GitLab

why3
why3
Commit 715be130 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files
Options

new example mex.MexArrayInPlace

parent 22f12ce4
Hide whitespace changes
Inline Side-by-side
Showing with 232 additions and 2 deletions
examples/mex.mlw
View file @ 715be130
(* {1 Minimum excludant, aka mex}
(** {1 Minimum excludant, aka mex}
Author: Jean-Christophe Filliâtre (CNRS)
Given a finite set of integers, find the smallest nonnegative integer
that does not belong to this set.
In the following, the set is given as an array A.
If N is the size of this array, it is clear that we have 0 <= mex <= N
for we cannot have the N+1 first natural numbers in the N cells of
array A (pigeon hole principle).
*)
(**
A simple algorithm is thus to mark values that belong to [0..N[ in
some external Boolean array of length N, ignoring any value that is
negative or greater or equal than N. Then a second loop scans the
marks until we find some unused value. If don't find any, then it means
that A contains exactly the integers 0,...,N-1 and the answer is N.
The very last step in this reasoning requires to invoke the pigeon hole
principle (imported from the standard library).
Time O(N) and space O(N).
*)
module MexArray
use import int.Int
......@@ -22,7 +41,7 @@ module MexArray
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
let ghost idx = ref (fun i -> i) in (* the position of each marked value *)
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 }
......@@ -42,8 +61,74 @@ module MexArray
if a[!r] = n then posn := !r;
incr r
done;
(* we cannot have !r=n (all values marked) and !posn>=0 at the same time *)
if !r = n && !posn >= 0 then pigeonhole (n+1) n (set !idx n !posn);
!r
end
(**
In this second implementation, we assume we are free to mutate array A.
The idea is then to scan the array from left to right, while
swapping elements to put any value in 0..N-1 at its place in the
array. When we are done, a second loop looks for the mex, advancing
as long as a[i]=i holds.
Since we perform only swaps, it is obvious that the mex of the final
array is equal to the mex of the original array.
Time O(N) and space O(1). The argument for a linear time complexity is as
follows: whenever we do not advance, we swap the element to its place,
which is further and did not contain that element; so we can do this only
N times.
Surprinsingly, proving that N is the answer whenever array A contains a
permutation of 0..N-1 is now easy (no need for a pigeon hole
principle or any kind of proof by induction).
*)
module MexArrayInPlace
use import int.Int
use import int.NumOf
use import array.Array
use import array.ArraySwap
use import ref.Refint
predicate mem (x: int) (a: array int) =
exists i. 0 <= i < length a && a[i] = x
function placed (a: array int) : int -> bool =
fun i -> a[i] = i
let mex (a: array int) : int
ensures { 0 <= result <= length a }
ensures { not (mem result (old a)) }
ensures { forall x. 0 <= x < result -> mem x (old a) }
= let n = length a in
let i = ref 0 in
while !i < n do
invariant { 0 <= !i <= n }
invariant { forall x. mem x a <-> mem x (old a) }
invariant { forall j. 0 <= j < !i -> 0 <= a[j] < n -> a[a[j]] = a[j] }
variant { n - !i, n - numof (placed a) 0 n }
let x = a[!i] in
if x < 0 || x >= n then
incr i
else if x < !i then begin
swap a !i x; incr i
end else if a[x] = x then
incr i
else
swap a !i x
done;
assert { forall j. 0 <= j < n -> let x = (old a)[j] in
0 <= x < n -> a[x] = x };
for i = 0 to n - 1 do
invariant { forall j. 0 <= j < i -> a[j] = j }
if a[i] <> i then return i
done;
n
end
examples/mex/why3session.xml
View file @ 715be130
......@@ -2,6 +2,7 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Z3" version="4.4.0" timelimit="1" steplimit="0" memlimit="1000"/>
<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">
......@@ -95,5 +96,149 @@
</transf>
</goal>
</theory>
<theory name="MexArrayInPlace" proved="true">
<goal name="VC mex" expl="VC for mex" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC mex.0" expl="loop invariant init" proved="true">
<proof prover="1"><result status="valid" time="0.03"/></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">
<transf name="split_all_full" proved="true" >
<goal name="VC mex.2.0" expl="loop invariant init" proved="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
</transf>
</goal>
<goal name="VC mex.3" expl="index in array bounds" proved="true">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC mex.4" expl="loop variant decrease" proved="true">
<proof prover="1"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC mex.5" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC mex.6" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC mex.7" expl="loop invariant preservation" proved="true">
<transf name="split_all_full" proved="true" >
<goal name="VC mex.7.0" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.04"/></proof>
</goal>
</transf>
</goal>
<goal name="VC mex.8" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC mex.9" expl="loop variant decrease" proved="true">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC mex.10" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC mex.11" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.22"/></proof>
</goal>
<goal name="VC mex.12" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.03"/></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.02"/></proof>
</goal>
<goal name="VC mex.15" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC mex.16" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.03"/></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="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC mex.19" expl="loop variant decrease" proved="true">
<proof prover="1"><result status="valid" time="0.30"/></proof>
</goal>
<goal name="VC mex.20" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC mex.21" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.24"/></proof>
</goal>
<goal name="VC mex.22" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.09"/></proof>
</goal>
<goal name="VC mex.23" expl="VC for mex" proved="true">
<proof prover="0"><result status="valid" time="0.32"/></proof>
</goal>
<goal name="VC mex.24" expl="loop invariant init" proved="true">
<proof prover="1"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="VC mex.25" expl="index in array bounds" proved="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC mex.26" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC mex.27" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC mex.28" expl="postcondition" proved="true">
<transf name="assert" proved="true" arg1="(mem x a)">
<goal name="VC mex.28.0" proved="true">
<transf name="assert" proved="true" arg1="(a[x] = x)">
<goal name="VC mex.28.0.0" proved="true">
<proof prover="1"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC mex.28.0.1" proved="true">
<proof prover="1"><result status="valid" time="0.03"/></proof>
</goal>
</transf>
</goal>
<goal name="VC mex.28.1" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
</goal>
<goal name="VC mex.29" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC mex.30" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC mex.31" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC mex.32" expl="postcondition" proved="true">
<transf name="assert" proved="true" arg1="(mem x a)">
<goal name="VC mex.32.0" proved="true">
<transf name="assert" proved="true" arg1="(a[x] = x)">
<goal name="VC mex.32.0.0" proved="true">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC mex.32.0.1" proved="true">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
</goal>
<goal name="VC mex.32.1" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
</goal>
<goal name="VC mex.33" expl="out of loop bounds" proved="true">
<proof prover="1"><result status="valid" time="0.02"/></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