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

simple_priority_queue: proof in progress

parent a005a14e
......@@ -7,22 +7,38 @@ module SimplePrioriyQueue
use import int.Int
use import ref.Ref
use import array.Array
use import bag.Bag
type elt
function priority elt : int
clone import array.NumOfEq with type elt = elt
type t = {
elems: array elt;
mutable size : int; (* size elements, stored in elems[0..size[ *)
mutable h : int; (* index of the highest prioiry element, if any *)
mutable h : int; (* index of the highest priority element, if any *)
ghost mutable bag: bag elt;
}
invariant { 0 <= self.size <= self.elems.length }
invariant { self.size = 0 \/ 0 <= self.h < self.size }
invariant { forall e: elt.
numof self.elems e 0 self.size = nb_occ e self.bag }
invariant { self.size > 0 -> forall e: elt. mem e self.bag ->
priority e <= priority self.elems[self.h] }
lemma numof_occ:
forall a: array elt, e: elt, l u: int.
numof a e l u > 0 <-> exists i: int. l <= i < u /\ a[i] = e
lemma numof_add:
forall a: array elt, e: elt, l u: int. l <= u ->
e = a[u] -> numof a e l (u+1) = 1 + numof a e l u
let create (n: int) (dummy: elt) : t
requires { 0 <= n }
ensures {result. size = 0 }
= { elems = Array.make n dummy; size = 0; h = 0; }
= { elems = Array.make n dummy; size = 0; h = 0; bag = empty_bag }
predicate is_empty (q: t) = q.size = 0
......@@ -30,20 +46,28 @@ module SimplePrioriyQueue
let add (q: t) (x: elt) : unit
requires { not (is_full q) }
writes { q.elems.elts, q.h, q.size }
writes { q.elems.elts, q.h, q.size, q.bag }
ensures { q.bag = add x (old q.bag) }
= q.elems[q.size] <- x;
if q.size = 0 then
q.h <- 0
else if priority x > priority q.elems[q.h] then
q.h <- q.size;
q.size <- q.size + 1
q.size <- q.size + 1;
q.bag <- add x q.bag
let highest (q: t) : elt
requires { not (is_empty q) }
ensures { mem result q.bag }
ensures { forall e: elt. mem e q.bag -> priority e <= priority result }
= q.elems[q.h]
let remove (q: t) : elt
requires { not (is_empty q) }
writes { q.elems.elts, q.h, q.size, q.bag }
ensures { old q.bag = add result q.bag }
ensures { mem result q.bag }
ensures { forall e: elt. mem e q.bag -> priority e <= priority result }
= q.size <- q.size - 1;
let r = q.elems[q.h] in
q.elems[q.h] <- q.elems[q.size];
......@@ -52,10 +76,13 @@ module SimplePrioriyQueue
q.h <- 0;
for i = 1 to q.size - 1 do
invariant { 0 <= q.h < q.size }
invariant { forall j: int. 0 <= j < i ->
priority q.elems[j] <= priority q.elems[q.h] }
let p = priority q.elems[i] in
if p > !m then begin q.h <- i; m := p end
done
end;
q.bag <- diff q.bag (singleton r);
r
end
......
This diff is collapsed.
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v2//EN" "http://why3.lri.fr/why3session.dtd">
<why3session shape_version="2">
<prover
id="0"
name="Alt-Ergo"
version="0.95.1"/>
<file
name="../simple_priority_queue.mlw"
verified="true"
expanded="true">
<theory
name="SimplePrioriyQueue"
locfile="../simple_priority_queue.mlw"
loclnum="5" loccnumb="7" loccnume="25"
verified="true"
expanded="true">
<goal
name="WP_parameter create"
locfile="../simple_priority_queue.mlw"
loclnum="22" loccnumb="6" loccnume="12"
expl="VC for create"
sum="6f03cecc7cfa9fbcc000cbcc4d582191"
proved="true"
expanded="true"
shape="ainfix =c0c0Aainfix &lt;c0c0Aainfix &lt;=c0c0Oainfix =c0c0Aainfix &lt;=c0V0Aainfix &lt;=c0c0Iainfix &lt;=c0V0Aainfix &gt;=V0c0Iainfix &lt;=c0V0F">
<label
name="expl:VC for create"/>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.04"/>
</proof>
</goal>
<goal
name="WP_parameter add"
locfile="../simple_priority_queue.mlw"
loclnum="31" loccnumb="6" loccnume="9"
expl="VC for add"
sum="42cbe0c4a7dc4264796928a1a4dc19da"
proved="true"
expanded="true"
shape="iainfix =V3c0ainfix &lt;=c0V0Aainfix &lt;V6V7Aainfix &lt;=c0V6Oainfix =V7c0Aainfix &lt;=V7V0Aainfix &lt;=c0V7Iainfix =V7ainfix +V3c1FIainfix =V6c0Fiainfix &gt;apriorityV1apriorityagetV5V2ainfix &lt;V8V9Aainfix &lt;=c0V8Oainfix =V9c0Aainfix &lt;=V9V0Aainfix &lt;=c0V9Iainfix =V9ainfix +V3c1FIainfix =V8V3Fainfix &lt;V2V10Aainfix &lt;=c0V2Oainfix =V10c0Aainfix &lt;=V10V0Aainfix &lt;=c0V10Iainfix =V10ainfix +V3c1FAainfix &lt;V2V0Aainfix &lt;=c0V2Aainfix &lt;=c0V0Iainfix =V5asetV4V3V1Aainfix &lt;=c0V0FAainfix &lt;V3V0Aainfix &lt;=c0V3Iainfix =V3V0NAainfix &lt;=c0V0Aainfix &lt;V2V3Aainfix &lt;=c0V2Oainfix =V3c0Aainfix &lt;=V3V0Aainfix &lt;=c0V3FF">
<label
name="expl:VC for add"/>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal
name="WP_parameter highest"
locfile="../simple_priority_queue.mlw"
loclnum="41" loccnumb="6" loccnume="13"
expl="VC for highest"
sum="5743111db96ddfdab0d06640c815d6c1"
proved="true"
expanded="true"
shape="ainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix =V2c0NAainfix &lt;=c0V0Aainfix &lt;V1V2Aainfix &lt;=c0V1Oainfix =V2c0Aainfix &lt;=V2V0Aainfix &lt;=c0V2FF">
<label
name="expl:VC for highest"/>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal
name="WP_parameter remove"
locfile="../simple_priority_queue.mlw"
loclnum="45" loccnumb="6" loccnume="12"
expl="VC for remove"
sum="4d296d95201068942df6ee3dd58e3f8b"
proved="true"
expanded="true"
shape="iainfix &gt;V4c0ainfix &lt;V8V4Aainfix &lt;=c0V8Oainfix =V4c0Aainfix &lt;=V4V0Aainfix &lt;=c0V4Iainfix &lt;V8V4Aainfix &lt;=c0V8Aiainfix &gt;apriorityV10V7ainfix &lt;V11V4Aainfix &lt;=c0V11Iainfix =V12apriorityV10FIainfix =V11V9Fainfix &lt;V8V4Aainfix &lt;=c0V8LagetV5V9Aainfix &lt;V9V0Aainfix &lt;=c0V9Iainfix &lt;V8V4Aainfix &lt;=c0V8Iainfix &lt;=V9ainfix -V4c1Aainfix &lt;=c1V9FFAainfix &lt;V6V4Aainfix &lt;=c0V6Iainfix &lt;=c1ainfix -V4c1Aainfix &lt;V6V4Aainfix &lt;=c0V6Oainfix =V4c0Aainfix &lt;=V4V0Aainfix &lt;=c0V4Iainfix &gt;c1ainfix -V4c1Iainfix =V6c0FAainfix &lt;c0V0Aainfix &lt;=c0c0Aainfix &lt;=c0V0ainfix &lt;=c0V0Aainfix &lt;V1V4Aainfix &lt;=c0V1Oainfix =V4c0Aainfix &lt;=V4V0Aainfix &lt;=c0V4Iainfix =V5asetV3V1agetV3V4Aainfix &lt;=c0V0FAainfix &lt;V1V0Aainfix &lt;=c0V1Aainfix &lt;V4V0Aainfix &lt;=c0V4Aainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix =V4ainfix -V2c1FIainfix =V2c0NAainfix &lt;=c0V0Aainfix &lt;V1V2Aainfix &lt;=c0V1Oainfix =V2c0Aainfix &lt;=V2V0Aainfix &lt;=c0V2FF">
<label
name="expl:VC for remove"/>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
</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