new example: skew heaps

various stuff added to in_progress

examples/in_progress/dyck.mlw

+
+theory Dyck
+
+  use export list.List
+  use export list.Append
+
+  type paren = L | R
+
+  type word = list paren
+
+  (* D -> eps | L D R D *)
+  inductive dyck word =
+  | Dyck_nil:
+      dyck Nil
+  | Dyck_ind:
+      forall w1 w2. dyck w1 -> dyck w2 -> dyck (Cons L (w1 ++ Cons R w2))
+
+  lemma dyck_concat:
+    forall w1 w2. dyck w1 -> dyck w2 -> dyck (w1 ++ w2)
+
+  (* the first letter, if any, must be L *)
+  lemma dyck_word_first:
+    forall w: word. dyck w ->
+    match w with Nil -> true | Cons c _ -> c = L end
+
+  lemma dyck_decomp:
+    forall w1 w2: word. dyck (w1 ++ w2) -> dyck w1 -> dyck w2
+
+end
+
+module Check
+
+  use import Dyck
+  use import list.Length
+
+  exception Failure
+
+  let rec is_dyck_rec (w: word) : word
+    ensures { exists p: word. dyck p && w = p ++ result &&
+              match result with Cons L _ -> false | _ -> true end }
+    raises  { Failure -> forall p s: word. w = p ++ s -> not (dyck p) }
+    variant { length w }
+  =
+    match w with
+    | Cons L w ->
+       match is_dyck_rec w with
+       | Cons R w -> is_dyck_rec w
+       | _        -> raise Failure
+       end
+    | _ ->
+       w
+    end
+
+  let is_dyck (w: word) : bool
+    ensures { result <-> dyck w }
+  =
+    try is_dyck_rec w = Nil with Failure -> false end
+
+end
+

examples/in_progress/dyck_language.mlw

@@ -38,6 +38,7 @@ module Check
   use import int.Int
   use import Dyck
 
+  (* open n w = L^n w *)
   function open (n: int) (w: word) : word
   axiom open0: forall w: word. open 0 w = w
   axiom openS: forall w: word, n: int. 0 < n ->

examples/in_progress/warshall_algorithm.mlw

+
+(** Warshall algorithm
+
+    Computes the transitive closure of a graph implemented as a Boolean
+    matrix. *)
+
+module WarshallAlgorithm
+
+  use import int.Int
+  use import matrix.Matrix
+
+  (* path m i j k =
+     there is a path from i to j, using only vertices smaller than k *)
+  inductive path (matrix bool) int int int =
+  | Path_empty:
+      forall m: matrix bool, i j k: int.
+      get m (i,j) -> path m i j k
+  | Path_cons:
+      forall m: matrix bool, i x j k: int.
+      0 <= x < k -> path m i x k -> path m x j k -> path m i j k
+
+  lemma weakening:
+    forall m i j k1 k2. 0 <= k2 <= k1 ->
+    path m i j k1 -> path m i j k2
+
+  let transitive_closure (m: matrix bool) : matrix bool
+    requires { m.rows = m.columns }
+    ensures  { let n = m.rows in
+               forall x y: int. 0 <= x < n -> 0 <= y < n ->
+               get result (x,y) <-> path m x y n }
+  =
+    let t = copy m in
+    let n = m.rows in
+    for k = 0 to n - 1 do
+      invariant { forall x y. 0 <= x < n -> 0 <= y < n ->
+                  get t (x,y) <-> path m x y k }
+      for i = 0 to n - 1 do
+        invariant { forall x y. 0 <= x < n -> 0 <= y < n ->
+                    get t (x,y) <->
+                    (path m x y k || x < i && path m x y (k+1)) }
+        for j = 0 to n - 1 do
+          invariant { forall x y. 0 <= x < n -> 0 <= y < n ->
+                      get t (x,y) <->
+                      (path m x y k || x < i && path m x y (k+1)
+                                    || x = i && y < j && path m x y (k+1)) }
+          set t (i,j) (get t (i,j) || get t (i,k) && get t (k,j))
+        done
+      done
+    done;
+    t
+
+end

examples/skew_heaps.mlw

+
+module SkewHeaps
+
+  use import bintree.Tree
+  use import bintree.Size
+
+  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
+    | Node _ x _ -> le e x
+  end
+
+  (* [t] is a heap *)
+  predicate heap (t: tree elt) = match t with
+    | Empty      -> true
+    | Node l x r -> le_root x l && heap l && le_root x r && heap r
+  end
+
+  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) }
+  =
+    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;
+    ()
+
+  let get_min (t: tree elt) : elt
+    requires { heap t && t <> Empty }
+    ensures  { is_minimum result t }
+  =
+    match t with
+      | Empty      -> absurd
+      | Node _ x _ -> x
+    end
+
+  let rec merge (t1 t2: tree elt) : tree elt
+    requires { heap t1 && heap t2 }
+    ensures  { heap result }
+    ensures  { forall e. occ e result = occ e t1 + occ e t2 }
+    variant  { size t1 + size t2 }
+  =
+    match t1, t2 with
+    | Empty, _ -> t2
+    | _, Empty -> t1
+    | Node l1 x1 r1, Node l2 x2 r2 ->
+       if le x1 x2 then
+         Node (merge r1 t2) x1 l1
+       else
+         Node (merge r2 t1) x2 l2
+    end
+
+  let add (x: elt) (t: tree elt) : tree elt
+    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 }
+  =
+    merge (Node Empty x Empty) t
+
+  let remove_minimum (t: tree elt) : tree elt
+    requires { heap t && t <> Empty }
+    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 }
+  =
+    match t with
+      | Empty      -> absurd
+      | Node l _ r -> merge l r
+    end
+
+end

theories/bintree.why

@@ -21,6 +21,28 @@ theory Size "number of nodes"
 
 end
 
+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
+    | Empty      -> 0
+    | Node l y r -> (if eq 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
+
+  predicate mem (x: elt) (t: tree elt) =
+    0 < occ x t
+
+end
+
 theory Inorder "inorder traversal"
 
   use export Tree

theories/bintree/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="4">
+ <prover
+  id="0"
+  name="Alt-Ergo"
+  version="0.95.2"/>
+ <file
+  name="../bintree.why"
+  verified="true"
+  expanded="false">
+  <theory
+   name="Tree"
+   locfile="../bintree.why"
+   loclnum="4" loccnumb="7" loccnume="11"
+   verified="true"
+   expanded="false">
+  </theory>
+  <theory
+   name="Size"
+   locfile="../bintree.why"
+   loclnum="10" loccnumb="7" loccnume="11"
+   verified="true"
+   expanded="false">
+   <label
+    name="number of nodes"/>
+   <goal
+    name="size_nonneg"
+    locfile="../bintree.why"
+    loclnum="20" loccnumb="8" loccnume="19"
+    sum="cb8c289d9686ccc4e3509e0890619661"
+    proved="true"
+    expanded="false"
+    shape="ainfix &lt;=c0asizeV0F">
+    <transf
+     name="induction_ty_lex"
+     proved="true"
+     expanded="false">
+     <goal
+      name="size_nonneg.1"
+      locfile="../bintree.why"
+      loclnum="20" loccnumb="8" loccnume="19"
+      expl="1."
+      sum="12d53d1b4d232aed7f7f83d7cb5e3f42"
+      proved="true"
+      expanded="false"
+      shape="Cainfix &lt;=c0asizeV0aEmptyainfix &lt;=c0asizeV0Iainfix &lt;=c0asizeV1Iainfix &lt;=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"
+   verified="true"
+   expanded="false">
+   <label
+    name="occurrences in a binary tree"/>
+   <goal
+    name="occ_nonneg"
+    locfile="../bintree.why"
+    loclnum="38" loccnumb="8" loccnume="18"
+    sum="f2106ad0f6afef73c8d8659379f4e159"
+    proved="true"
+    expanded="false"
+    shape="ainfix &lt;=c0aoccV0V1F">
+    <transf
+     name="induction_ty_lex"
+     proved="true"
+     expanded="false">
+     <goal
+      name="occ_nonneg.1"
+      locfile="../bintree.why"
+      loclnum="38" loccnumb="8" loccnume="18"
+      expl="1."
+      sum="6ad4875c535741780c16685271aaf9e3"
+      proved="true"
+      expanded="false"
+      shape="Cainfix &lt;=c0aoccV0V1aEmptyainfix &lt;=c0aoccV0V1Iainfix &lt;=c0aoccV0V2Iainfix &lt;=c0aoccV0V4aNodeVVVV1F">
+      <proof
+       prover="0"
+       timelimit="6"
+       memlimit="1000"
+       obsolete="false"
+       archived="false">
+       <result status="valid" time="0.01"/>
+      </proof>
+     </goal>
+    </transf>
+   </goal>
+  </theory>
+  <theory
+   name="Inorder"
+   locfile="../bintree.why"
+   loclnum="46" loccnumb="7" loccnume="14"
+   verified="true"
+   expanded="false">
+   <label
+    name="inorder traversal"/>
+  </theory>
+  <theory
+   name="Preorder"
+   locfile="../bintree.why"
+   loclnum="58" loccnumb="7" loccnume="15"
+   verified="true"
+   expanded="false">
+   <label
+    name="preorder traversal"/>
+  </theory>
+  <theory
+   name="InorderLength"
+   locfile="../bintree.why"
+   loclnum="70" loccnumb="7" loccnume="20"
+   verified="true"
+   expanded="false">
+   <goal
+    name="inorder_length"
+    locfile="../bintree.why"
+    loclnum="76" loccnumb="8" loccnume="22"
+    sum="35f8a02ac76b338b12bc12823565d6c2"
+    proved="true"
+    expanded="false"
+    shape="ainfix =alengthainorderV0asizeV0F">
+    <transf
+     name="induction_ty_lex"
+     proved="true"
+     expanded="false">
+     <goal
+      name="inorder_length.1"
+      locfile="../bintree.why"
+      loclnum="76" loccnumb="8" loccnume="22"
+      expl="1."
+      sum="a14cd8e33cdb1250c6764bf6b3d4c8b8"
+      proved="true"
+      expanded="false"
+      shape="Cainfix =alengthainorderV0asizeV0aEmptyainfix =alengthainorderV0asizeV0Iainfix =alengthainorderV1asizeV1Iainfix =alengthainorderV3asizeV3aNodeVVVV0F">
+      <proof
+       prover="0"
+       timelimit="6"
+       memlimit="1000"
+       obsolete="false"
+       archived="false">
+       <result status="valid" time="0.01"/>
+      </proof>
+     </goal>
+    </transf>
+   </goal>
+  </theory>
+  <theory
+   name="Zipper"
+   locfile="../bintree.why"
+   loclnum="80" loccnumb="7" loccnume="13"
+   verified="true"
+   expanded="false">
+   <label
+    name="Huet&apos;s zipper"/>
+  </theory>
+ </file>
+</why3session>