Merge branch 'master' of git+ssh://scm.gforge.inria.fr//gitroot/why3/why3

examples/in_progress/schorr_waite.mlw

+
+(** Schorr-Waite algorithm
+
+    The Schorr-Waite algorithm is the first mountain that any
+    formalism for pointer aliasing should climb.
+                                      -- Richard Bornat, 2000
+
+*)
+
+
+module SchorrWaite
+
+  use import bool.Bool
+  use import map.Map
+  use import ref.Ref
+
+  (** a small component-as-array memory model *)
+
+  type loc
+  constant null: loc
+
+  val m: ref (map loc bool)
+  val c: ref (map loc bool)
+  val left: ref (map loc loc)
+  val right: ref (map loc loc)
+
+  val get_left (p: loc) : loc
+    requires { p <> null }
+    ensures  { result = !left[p] }
+
+  val get_right (p: loc) : loc
+    requires { p <> null }
+    ensures  { result = !right[p] }
+
+  val set_left (p: loc) (v: loc) : unit
+    requires { p <> null }
+    writes   { left }
+    ensures  { !left = set (old !left) p v }
+
+  val set_right (p: loc) (v: loc) : unit
+    requires { p <> null }
+    writes   { right }
+    ensures  { !right = set (old !right) p v }
+
+  val set_m (p: loc) (v: bool) : unit
+    requires { p <> null }
+    writes   { m }
+    ensures  { !m = set (old !m) p v }
+
+  val set_c (p: loc) (v: bool) : unit
+    requires { p <> null }
+    writes   { c }
+    ensures  { !c = set (old !c) p v }
+
+  let rec schorr_waite (root: loc) : unit
+    requires { true }
+    ensures  { true }
+  =
+    let t = ref root in
+    let p = ref null in
+    while !p <> null || !t <> null && not !m[!t] do
+      if !t = null || !m[!t] then begin
+        if !c[!p] then begin (* pop *)
+          let q = !t in
+          t := !p;
+          p := !right[!p];
+          set_right !t q;
+        end else begin (* swing *)
+          let q = !t in
+          t := get_right !p;
+          set_right !p (get_left !p);
+          set_left !p q;
+          set_c !p true;
+        end
+      end else begin (* push *)
+        let q = !p in
+        p := !t;
+        t := get_left !t;
+        set_left !p q;
+        set_m !p true;
+        set_c !p false
+      end
+    done
+
+
+end

examples/in_progress/schorr_waite/why3session.xml

+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
+"http://why3.lri.fr/why3session.dtd">
+<why3session shape_version="4">
+<prover id="0" name="Alt-Ergo" version="0.95.2" timelimit="6" memlimit="1000"/>
+<file name="../schorr_waite.mlw" expanded="true">
+<theory name="SchorrWaite" sum="314f8aff34aee757724062323b08572c" expanded="true">
+ <goal name="WP_parameter schorr_waite" expl="VC for schorr_waite" expanded="true">
+ <proof prover="0"><result status="valid" time="0.01" steps="30"/></proof>
+ </goal>
+</theory>
+</file>
+</why3session>