new example: array_most_frequent

(a simple programming exercise, with a simple proof)
parent 9004bddb
use int.Int
use ref.Refint
use array.Array
use array.NumOfEq
(** A simple programming exercise: find out the most frequent value in an array
Using an external table (e.g. a hash table), we can easily do it
in linear time and space.
However, if the array is sorted, we can do it in linear time and
constant space. *)
let most_frequent (a: array int) : int
requires { length a > 0 }
requires { forall i j. 0 <= i <= j < length a -> a[i] <= a[j] }
ensures { numof a result 0 (length a) > 0 }
ensures { forall x. numof a x 0 (length a) <= numof a result 0 (length a) }
= let ref r = a[0] in
let ref c = 1 in
let ref m = 1 in
for i = 1 to length a - 1 do
invariant { c = numof a a[i-1] 0 i }
invariant { m = numof a r 0 i }
invariant { forall x. numof a x 0 i <= m }
if a[i] = a[i-1] then begin
incr c;
if c > m then begin m <- c; r <- a[i] end
end else
c <- 1
done;
r
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="6">
<prover id="0" name="Z3" version="4.6.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="2.2.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="2" name="CVC4" version="1.6" timelimit="1" steplimit="0" memlimit="1000"/>
<file proved="true">
<path name=".."/>
<path name="array_most_frequent.mlw"/>
<theory name="Top" proved="true">
<goal name="VC most_frequent" expl="VC for most_frequent" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC most_frequent.0" expl="index in array bounds" proved="true">
<proof prover="2"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC most_frequent.1" expl="loop invariant init" proved="true">
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC most_frequent.2" expl="loop invariant init" proved="true">
<proof prover="2"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC most_frequent.3" expl="loop invariant init" proved="true">
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC most_frequent.4" expl="index in array bounds" proved="true">
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC most_frequent.5" expl="index in array bounds" proved="true">
<proof prover="2"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC most_frequent.6" expl="index in array bounds" proved="true">
<proof prover="2"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC most_frequent.7" expl="loop invariant preservation" proved="true">
<proof prover="2"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="VC most_frequent.8" expl="loop invariant preservation" proved="true">
<proof prover="2"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC most_frequent.9" expl="loop invariant preservation" proved="true">
<proof prover="2"><result status="valid" time="0.17"/></proof>
</goal>
<goal name="VC most_frequent.10" expl="loop invariant preservation" proved="true">
<proof prover="2"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="VC most_frequent.11" expl="loop invariant preservation" proved="true">
<proof prover="2"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC most_frequent.12" expl="loop invariant preservation" proved="true">
<proof prover="2"><result status="valid" time="0.29"/></proof>
</goal>
<goal name="VC most_frequent.13" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC most_frequent.14" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.46" steps="834"/></proof>
</goal>
<goal name="VC most_frequent.15" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.09"/></proof>
</goal>
<goal name="VC most_frequent.16" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.26" steps="1059"/></proof>
</goal>
<goal name="VC most_frequent.17" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC most_frequent.18" expl="out of loop bounds" proved="true">
<proof prover="2"><result status="valid" time="0.03"/></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