new example: simple priority queue (only safety, so far)

57af1c42 · Jean-Christophe Filliâtre · cb38a2bd · 57af1c42 · 57af1c42
Commit 57af1c42 authored Mar 23, 2013 by Jean-Christophe Filliâtre
--- a/examples/simple_priority_queue.mlw
+++ b/examples/simple_priority_queue.mlw
+
+(* Simple priority queue implementation
+   (inspired by Tinelli's lecture http://www.divms.uiowa.edu/~tinelli/181/) *)
+
+module SimplePrioriyQueue
+
+  use import int.Int
+  use import ref.Ref
+  use import array.Array
+
+  type elt
+  function priority elt : int
+
+  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 *)
+  }
+  invariant { 0 <= self.size <= self.elems.length }
+  invariant { self.size = 0 \/ 0 <= self.h < self.size }
+
+  let create (n: int) (dummy: elt) : t
+    requires { 0 <= n }
+    ensures  {result. size = 0 }
+  = { elems = Array.make n dummy; size = 0; h = 0; }
+
+  predicate is_empty (q: t) = q.size = 0
+
+  predicate is_full (q: t) = q.size = length q.elems
+
+  let add (q: t) (x: elt) : unit
+    requires { not (is_full q) }
+    writes   { q.elems.elts, q.h, q.size }
+  = 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
+
+  let highest (q: t) : elt
+    requires { not (is_empty q) }
+  = q.elems[q.h]
+
+  let remove (q: t) : elt
+    requires { not (is_empty q) }
+  = q.size <- q.size - 1;
+    let r = q.elems[q.h] in
+    q.elems[q.h] <- q.elems[q.size];
+    if q.size > 0 then begin
+      let m = ref (priority q.elems[0]) in
+      q.h <- 0;
+      for i = 1 to q.size - 1 do
+        invariant { 0 <= q.h < q.size }
+        let p = priority q.elems[i] in
+        if p > !m then begin q.h <- i; m := p end
+      done
+    end;
+    r
+
+end
+
--- a/examples/simple_priority_queue/why3session.xml
+++ b/examples/simple_priority_queue/why3session.xml
+<?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="b2d372c21a7fb7e381ff0f6d8c508632"
+    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="4a9f046d480d7daacf1561e3aa59c185"
+    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="96427a3aa7dd3b9c59e6af1d2cfeaa81"
+    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>