skew heaps: application to heapsort

examples/skew_heaps.mlw

@@ -2,17 +2,14 @@
 module SkewHeaps
 
   use import bintree.Tree
-  use import bintree.Size
+  use export bintree.Size
+  use export bintree.Occ
 
   type elt
 
   predicate le elt elt
   clone relations.TotalPreOrder with type t = elt, predicate rel = le
 
-  predicate eq (x y: elt) = le x y && le y x
-
-  clone import bintree.Occ with type elt = elt, predicate eq = eq
-
   (* [e] is no greater than the root of [t], if any *)
   predicate le_root (e: elt) (t: tree elt) = match t with
     | Empty      -> true
@@ -25,21 +22,44 @@ module SkewHeaps
     | Node l x r -> le_root x l && heap l && le_root x r && heap r
   end
 
+  function minimum (tree elt) : elt
+  axiom minimum_def: forall l x r. minimum (Node l x r) = x
+
   predicate is_minimum (x: elt) (t: tree elt) =
     mem x t && forall e. mem e t -> le x e
 
   (* the root is the smallest element *)
-  let rec lemma root_is_min (l: tree elt) (x: elt) (r: tree elt) : unit
-     requires { heap (Node l x r) } variant { size (Node l x r) }
-     ensures  { is_minimum x (Node l x r) }
+  let rec lemma root_is_min (t: tree elt) : unit
+     requires { heap t && 0 < size t }
+     ensures  { is_minimum (minimum t) t }
+     variant  { size t }
+  = match t with
+    | Empty -> absurd
+    | Node l _ r ->
+        if l <> Empty then root_is_min l;
+        if r <> Empty then root_is_min r
+    end
+
+  let empty () : tree elt
+    ensures { heap result }
+    ensures { size result = 0 }
+    ensures { forall e. not (mem e result) }
+  =
+    Empty
+
+  let is_empty (t: tree elt) : bool
+    ensures { result <-> size t = 0 }
+  =
+    t = Empty
+
+  let size (t: tree elt) : int
+    ensures { result = size t }
   =
-    match l with Empty -> () | Node ll lx lr -> root_is_min ll lx lr end;
-    match r with Empty -> () | Node rl rx rr -> root_is_min rl rx rr end;
-    ()
+    size t
 
   let get_min (t: tree elt) : elt
-    requires { heap t && t <> Empty }
-    ensures  { is_minimum result t }
+    requires { heap t && 0 < size t }
+    ensures  { result = minimum t }
   =
     match t with
       | Empty      -> absurd
@@ -50,6 +70,7 @@ module SkewHeaps
     requires { heap t1 && heap t2 }
     ensures  { heap result }
     ensures  { forall e. occ e result = occ e t1 + occ e t2 }
+    ensures  { size result = size t1 + size t2 }
     variant  { size t1 + size t2 }
   =
     match t1, t2 with
@@ -66,15 +87,17 @@ module SkewHeaps
     requires { heap t }
     ensures  { heap result }
     ensures  { occ x result = occ x t + 1 }
-    ensures  { forall e. not (eq e x) -> occ e result = occ e t }
+    ensures  { forall e. e <> x -> occ e result = occ e t }
+    ensures  { size result = size t + 1 }
   =
     merge (Node Empty x Empty) t
 
-  let remove_minimum (t: tree elt) : tree elt
-    requires { heap t && t <> Empty }
+  let remove_min (t: tree elt) : tree elt
+    requires { heap t && 0 < size t }
     ensures  { heap result }
-    ensures  { forall e. if is_minimum e t then occ e result = occ e t - 1
-                                           else occ e result = occ e t }
+    ensures  { occ (minimum t) result = occ (minimum t) t - 1 }
+    ensures  { forall e. e <> minimum t -> occ e result = occ e t }
+    ensures  { size result = size t - 1 }
   =
     match t with
       | Empty      -> absurd
@@ -82,3 +105,42 @@ module SkewHeaps
     end
 
 end
+
+(* application *)
+
+module HeapSort
+
+  use import SkewHeaps
+  use import int.Int
+  use import ref.Ref
+  use import array.Array
+  use import array.ArrayPermut
+  clone export array.Sorted with type elt = elt, predicate le = le
+  use import map.Occ as M
+  use import bintree.Occ as H
+
+  let heapsort (a: array elt) : unit
+    ensures { sorted a }
+    ensures { permut_all (old a) a }
+  =
+    let n = length a in
+    let t = ref (empty ()) in
+    for i = 0 to n - 1 do
+      invariant { heap !t && size !t = i }
+      invariant { forall e.
+                  M.occ e a.elts i n + H.occ e !t = M.occ e a.elts 0 n }
+      t := add a[i] !t;
+      assert { M.occ a[i] a.elts i n = 1 + M.occ a[i] a.elts (i+1) n }
+    done;
+    'I:
+    for i = 0 to n - 1 do
+      invariant { sorted_sub a 0 i }
+      invariant { heap !t && size !t = n - i }
+      invariant { forall j. 0 <= j < i -> forall e. mem e !t -> le a[j] e }
+      invariant { forall e.
+                  M.occ e a.elts 0 i + H.occ e !t = M.occ e (at a.elts 'I) 0 n }
+      a[i] <- get_min !t;
+      t := remove_min !t
+    done
+
+end

theories/bintree.why

@@ -19,6 +19,8 @@ theory Size "number of nodes"
 
   lemma size_nonneg: forall t: tree 'a. 0 <= size t
 
+  lemma size_empty: forall t: tree 'a. 0 = size t <-> t = Empty
+
 end
 
 theory Occ "occurrences in a binary tree"
@@ -26,19 +28,15 @@ theory Occ "occurrences in a binary tree"
   use export Tree
   use export int.Int
 
-  type elt
-
-  predicate eq elt elt
-
-  function occ (x: elt) (t: tree elt) : int = match t with
+  function occ (x: 'a) (t: tree 'a) : int = match t with
     | Empty      -> 0
-    | Node l y r -> (if eq y x then 1 else 0) + occ x l + occ x r
+    | Node l y r -> (if y = x then 1 else 0) + occ x l + occ x r
   end
 
   lemma occ_nonneg:
-    forall x: elt, t: tree elt. 0 <= occ x t
+    forall x: 'a, t: tree 'a. 0 <= occ x t
 
-  predicate mem (x: elt) (t: tree elt) =
+  predicate mem (x: 'a) (t: tree 'a) =
     0 < occ x t
 
 end

theories/bintree/why3session.xml

@@ -8,7 +8,7 @@
  <file
   name="../bintree.why"
   verified="true"
-  expanded="false">
+  expanded="true">
   <theory
    name="Tree"
    locfile="../bintree.why"
@@ -21,7 +21,7 @@
    locfile="../bintree.why"
    loclnum="10" loccnumb="7" loccnume="11"
    verified="true"
-   expanded="false">
+   expanded="true">
    <label
     name="number of nodes"/>
    <goal
@@ -30,12 +30,12 @@
     loclnum="20" loccnumb="8" loccnume="19"
     sum="cb8c289d9686ccc4e3509e0890619661"
     proved="true"
-    expanded="false"
+    expanded="true"
     shape="ainfix &lt;=c0asizeV0F">
     <transf
      name="induction_ty_lex"
      proved="true"
-     expanded="false">
+     expanded="true">
      <goal
       name="size_nonneg.1"
       locfile="../bintree.why"
@@ -43,7 +43,7 @@
       expl="1."
       sum="12d53d1b4d232aed7f7f83d7cb5e3f42"
       proved="true"
-      expanded="false"
+      expanded="true"
       shape="Cainfix &lt;=c0asizeV0aEmptyainfix &lt;=c0asizeV0Iainfix &lt;=c0asizeV1Iainfix &lt;=c0asizeV3aNodeVVVV0F">
       <proof
        prover="0"
@@ -56,35 +56,67 @@
      </goal>
     </transf>
    </goal>
+   <goal
+    name="size_empty"
+    locfile="../bintree.why"
+    loclnum="22" loccnumb="8" loccnume="18"
+    sum="b31540d42a20b62d3b95f5df6a1117e7"
+    proved="true"
+    expanded="true"
+    shape="ainfix =V0aEmptyqainfix =c0asizeV0F">
+    <transf
+     name="induction_ty_lex"
+     proved="true"
+     expanded="true">
+     <goal
+      name="size_empty.1"
+      locfile="../bintree.why"
+      loclnum="22" loccnumb="8" loccnume="18"
+      expl="1."
+      sum="c50dc79fc1bbfb85ca3062b724b8de5e"
+      proved="true"
+      expanded="false"
+      shape="Cainfix =V0aEmptyqainfix =c0asizeV0aEmptyainfix =V0aEmptyqainfix =c0asizeV0Iainfix =V1aEmptyqainfix =c0asizeV1Iainfix =V3aEmptyqainfix =c0asizeV3aNodeVVVV0F">
+      <proof
+       prover="0"
+       timelimit="6"
+       memlimit="1000"
+       obsolete="false"
+       archived="false">
+       <result status="valid" time="0.01"/>
+      </proof>
+     </goal>
+    </transf>
+   </goal>
   </theory>
   <theory
    name="Occ"
    locfile="../bintree.why"
-   loclnum="24" loccnumb="7" loccnume="10"
+   loclnum="26" loccnumb="7" loccnume="10"
    verified="true"
-   expanded="false">
+   expanded="true">
    <label
     name="occurrences in a binary tree"/>
    <goal
     name="occ_nonneg"
     locfile="../bintree.why"
-    loclnum="38" loccnumb="8" loccnume="18"
-    sum="f2106ad0f6afef73c8d8659379f4e159"
+    loclnum="36" loccnumb="8" loccnume="18"
+    sum="717594c52723f5c7e9666ab1ab6810b6"
     proved="true"
-    expanded="false"
+    expanded="true"
     shape="ainfix &lt;=c0aoccV0V1F">
     <transf
      name="induction_ty_lex"
      proved="true"
-     expanded="false">
+     expanded="true">
      <goal
       name="occ_nonneg.1"
       locfile="../bintree.why"
-      loclnum="38" loccnumb="8" loccnume="18"
+      loclnum="36" loccnumb="8" loccnume="18"
       expl="1."
-      sum="6ad4875c535741780c16685271aaf9e3"
+      sum="63d90ff251110ddb7e30c27b8bb421b1"
       proved="true"
-      expanded="false"
+      expanded="true"
       shape="Cainfix &lt;=c0aoccV0V1aEmptyainfix &lt;=c0aoccV0V1Iainfix &lt;=c0aoccV0V2Iainfix &lt;=c0aoccV0V4aNodeVVVV1F">
       <proof
        prover="0"
@@ -101,7 +133,7 @@
   <theory
    name="Inorder"
    locfile="../bintree.why"
-   loclnum="46" loccnumb="7" loccnume="14"
+   loclnum="44" loccnumb="7" loccnume="14"
    verified="true"
    expanded="false">
    <label
@@ -110,7 +142,7 @@
   <theory
    name="Preorder"
    locfile="../bintree.why"
-   loclnum="58" loccnumb="7" loccnume="15"
+   loclnum="56" loccnumb="7" loccnume="15"
    verified="true"
    expanded="false">
    <label
@@ -119,29 +151,29 @@
   <theory
    name="InorderLength"
    locfile="../bintree.why"
-   loclnum="70" loccnumb="7" loccnume="20"
+   loclnum="68" loccnumb="7" loccnume="20"
    verified="true"
-   expanded="false">
+   expanded="true">
    <goal
     name="inorder_length"
     locfile="../bintree.why"
-    loclnum="76" loccnumb="8" loccnume="22"
-    sum="35f8a02ac76b338b12bc12823565d6c2"
+    loclnum="74" loccnumb="8" loccnume="22"
+    sum="e81c509b7e9a14f0ce5eba170b717974"
     proved="true"
-    expanded="false"
+    expanded="true"
     shape="ainfix =alengthainorderV0asizeV0F">
     <transf
      name="induction_ty_lex"
      proved="true"
-     expanded="false">
+     expanded="true">
      <goal
       name="inorder_length.1"
       locfile="../bintree.why"
-      loclnum="76" loccnumb="8" loccnume="22"
+      loclnum="74" loccnumb="8" loccnume="22"
       expl="1."
-      sum="a14cd8e33cdb1250c6764bf6b3d4c8b8"
+      sum="76c4ea67fd68f44ff3811c278c699051"
       proved="true"
-      expanded="false"
+      expanded="true"
       shape="Cainfix =alengthainorderV0asizeV0aEmptyainfix =alengthainorderV0asizeV0Iainfix =alengthainorderV1asizeV1Iainfix =alengthainorderV3asizeV3aNodeVVVV0F">
       <proof
        prover="0"
@@ -158,7 +190,7 @@
   <theory
    name="Zipper"
    locfile="../bintree.why"
-   loclnum="80" loccnumb="7" loccnume="13"
+   loclnum="78" loccnumb="7" loccnume="13"
    verified="true"
    expanded="false">
    <label