new example in progress: ropes

examples/in_progress/ropes.mlw

-module M
+
+module Rope
 
   use import int.Int
 
-  (* use import string.String *)
+  (* immutable strings *)
+(**
   namespace import S
+
+    use HighOrd as HO
     type char
-    type string
-    function length string : int
-    function get string int : char
-    function app string string : string
-    function sub string int int : string
-    function create int : string
+    constant dummy_char: char
+    type string = { length: int; chars: HO.func int char }
+
+    val get (s: string) (i:int) : char
+      requires { 0 <= i < s.length }
+      ensures  { result = s.chars i }
+
+    function app (s1 s2: string) : string =
+      { length = s1.length + s2.length;
+        chars = \ i: int.
+          if i < s1.length then s1.chars i else s2.chars (i - s1.length) }
+    function sub (s: string) (ofs: int) (len: int) : string =
+      { length = len; chars = \ i: int. s.chars (i - ofs) }
+    constant empty : string = { length = 0; chars = \ i: int. dummy_char }
+    predicate (==) (s1 s2: string) =
+      s1.length = s2.length /\
+      forall i:int. 0 <= i < s1.length -> s1.chars i = s2.chars i
+
   end
+**)
+  namespace import S
+
+    type char
+    constant dummy_char: char
+
+    type string
+
+    function length string: int
+    axiom length_nonnegative: forall s: string. length s >= 0
+
+    function ([]) string int: char
+
+    constant empty: string
+    axiom empty_def: length empty = 0
+
+    predicate (==) (s1 s2: string) =
+      length s1 = length s2 /\
+      forall i:int. 0 <= i < length s1 -> s1[i] = s2[i]
+
+    function app string string: string
+    axiom app_def1:
+      forall s1 s2: string. length (app s1 s2) = length s1 + length s2
+    axiom app_def2:
+      forall s1 s2: string, i: int.
+      0 <= i < length s1 -> (app s1 s2)[i] = s1[i]
+    axiom app_def3:
+      forall s1 s2: string, i: int.
+      length s1 <= i < length s1 + length s2 ->
+      (app s1 s2)[i] = s2[i - length s1]
+
+    function sub string int int: string
+    axiom sub_def1:
+      forall s: string, ofs len: int.
+      0 <= len -> 0 <= ofs < length s -> ofs + len <= length s ->
+      length (sub s ofs len) = len
+    axiom sub_def2:
+      forall s: string, ofs len: int.
+      0 <= len -> 0 <= ofs < length s -> ofs + len <= length s ->
+      forall i: int. 0 <= i < len -> (sub s ofs len)[i] = s[ofs + i]
+
+ end
+
 
   type rope =
-    | Str string int  (len: int)
-    | App rope   rope (len: int)
+    | Emp
+    | Str string int  int  (* Str s ofs len is s[ofs..ofs+len[ *)
+    | App rope   rope int  (* concatenation and total length   *)
+
+  function length (r: rope) : int = match r with
+    | Emp         -> 0
+    | Str _ _ len -> len
+    | App _ _ len -> len
+  end
 
   predicate inv (r: rope) = match r with
+    | Emp ->
+        true
     | Str s ofs len ->
-        len = 0 \/ 0 <= ofs < S.length s /\ ofs + len <= S.length s
-    | App l r _ ->
-        0 < len l /\ inv l /\ 0 < len r /\ inv r
+        0 < len /\ 0 <= ofs < S.length s /\ ofs + len <= S.length s
+    | App l r len ->
+        0 < length l /\ inv l /\ 0 < length r /\ inv r /\
+        len = length l + length r
   end
 
-  function model (r: rope) : string = match r with
+  function string (r: rope) : string = match r with
+    | Emp           -> S.empty
     | Str s ofs len -> S.sub s ofs len
-    | App l r _     -> S.app (model l) (model r)
+    | App l r _     -> S.app (string l) (string r)
   end
 
-  predicate eq (s1 s2: string) =
-    S.length s1 = S.length s2 /\
-    forall i:int. 0 <= i < S.length s1 -> S.get s1 i = S.get s2 i
+  lemma rope_length_is_string_length:
+    forall r: rope. inv r -> S.length (string r) = length r
 
   let empty ()
-    ensures { len result = 0 /\ inv result /\ eq (model result) (S.create 0) }
-  = Str (S.create 0) 0 0
+    ensures { length result = 0 /\ inv result /\ string result == S.empty }
+  = Emp
 
-  let length r ensures { result = len r } = len r
+  let is_empty (r: rope) : bool
+    requires { inv r }
+    ensures  { result <-> length r = 0 }
+  = r = Emp
 
-(**
-  let rec get (r: rope) i
-    requires { inv r /\ 0 <= i < len r }
-    ensures { result = S.get (model r) i }
+  let of_string (s: string) : rope
+    requires { 0 <= S.length s }
+    ensures  { string result == s }
+    ensures  { inv result }
+  = if S.length s = 0 then Emp else Str s 0 (S.length s)
+
+  let rec get (r: rope) (i: int) : char
+    requires { inv r /\ 0 <= i < length r }
+    ensures  { result = (string r)[i] }
+    variant  { r }
   = match r with
-    | Str s ofs len ->
-        S.get s (ofs + i)
-    | App l r   _   ->
-        let n = length l in
-        if i < n then get l i else get r (i - n)
+    | Emp ->
+        absurd
+    | Str s ofs _ ->
+       s[ofs + i]
+    | App left right _   ->
+        let n = length left in
+        if i < n then get left i else get right (i - n)
     end
-**)
+
+  let rec concat (r1 r2: rope) : rope
+    requires { inv r1 /\ inv r2 }
+    ensures  { inv result }
+    ensures  { string result = S.app (string r1) (string r2) }
+  = absurd (* TODO *)
+
+  let rec sub (r: rope) (ofs len: int) : rope
+    requires { inv r }
+    requires { 0 <= len /\ 0 <= ofs < length r /\ ofs + len <= length r }
+    ensures  { inv result }
+    ensures  { string result = S.sub (string r) ofs len }
+  = absurd (* TODO *)
 
 end

examples/in_progress/ropes/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"/>
+ <prover
+  id="1"
+  name="CVC4"
+  version="1.3"/>
+ <file
+  name="../ropes.mlw"
+  verified="true"
+  expanded="true">
+  <theory
+   name="Rope"
+   locfile="../ropes.mlw"
+   loclnum="2" loccnumb="7" loccnume="11"
+   verified="true"
+   expanded="true">
+   <goal
+    name="rope_length_is_string_length"
+    locfile="../ropes.mlw"
+    loclnum="102" loccnumb="8" loccnume="36"
+    sum="c6f0e9a4526fd86fc2c651a3aa144de9"
+    proved="true"
+    expanded="false"
+    shape="ainfix =alengthastringV0alengthV0IainvV0F">
+    <transf
+     name="induction_ty_lex"
+     proved="true"
+     expanded="false">
+     <goal
+      name="rope_length_is_string_length.1"
+      locfile="../ropes.mlw"
+      loclnum="102" loccnumb="8" loccnume="36"
+      expl="1."
+      sum="b6bf4eb630e8ae656734e891c2a69a5e"
+      proved="true"
+      expanded="false"
+      shape="Cainfix =alengthastringV0alengthV0IainvV0aEmpainfix =alengthastringV0alengthV0IainvV0aStrVVVainfix =alengthastringV0alengthV0IainvV0Iainfix =alengthastringV4alengthV4IainvV4Iainfix =alengthastringV5alengthV5IainvV5aAppVVVV0F">
+      <proof
+       prover="0"
+       timelimit="10"
+       memlimit="1000"
+       obsolete="false"
+       archived="false">
+       <result status="valid" time="0.03"/>
+      </proof>
+     </goal>
+    </transf>
+   </goal>
+   <goal
+    name="WP_parameter empty"
+    locfile="../ropes.mlw"
+    loclnum="105" loccnumb="6" loccnume="11"
+    expl="VC for empty"
+    sum="b3b8030e65ca587fb31305a23fc6ab60"
+    proved="true"
+    expanded="false"
+    shape="ainfix ==astringV0aemptyAainvV0LaEmp">
+    <label
+     name="expl:VC for empty"/>
+    <proof
+     prover="0"
+     timelimit="10"
+     memlimit="1000"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.02"/>
+    </proof>
+   </goal>
+   <goal
+    name="WP_parameter is_empty"
+    locfile="../ropes.mlw"
+    loclnum="109" loccnumb="6" loccnume="14"
+    expl="VC for is_empty"
+    sum="8c4e0b30b4cbb3005c093d850107a848"
+    proved="true"
+    expanded="false"
+    shape="ainfix =Cc0aEmpV1aStrwwVV2aAppwwVV0c0qainfix =V0aEmpIainvV0F">
+    <label
+     name="expl:VC for is_empty"/>
+    <proof
+     prover="1"
+     timelimit="10"
+     memlimit="1000"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.02"/>
+    </proof>
+   </goal>
+   <goal
+    name="WP_parameter of_string"
+    locfile="../ropes.mlw"
+    loclnum="114" loccnumb="6" loccnume="15"
+    expl="VC for of_string"
+    sum="f8a4505f5a32f2c1fe7e4dc8ef6cb8ac"
+    proved="true"
+    expanded="false"
+    shape="ainviaStrV0c0alengthV0aEmpainfix =alengthV0c0Aainfix ==astringiaStrV0c0alengthV0aEmpainfix =alengthV0c0V0Iainfix &lt;=c0alengthV0F">
+    <label
+     name="expl:VC for of_string"/>
+    <proof
+     prover="0"
+     timelimit="10"
+     memlimit="1000"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.04"/>
+    </proof>
+   </goal>
+   <goal
+    name="WP_parameter get"
+    locfile="../ropes.mlw"
+    loclnum="120" loccnumb="10" loccnume="13"
+    expl="VC for get"
+    sum="a80563ebb39638bdf9c3747ac80b243f"
+    proved="true"
+    expanded="true"
+    shape="CfaEmpainfix =amixfix []V2ainfix +V3V1amixfix []astringV0V1aStrVVwiainfix =amixfix []astringV5V7amixfix []astringV0V1Aainfix &lt;V7Cc0aEmpV8aStrwwVV9aAppwwVV5Aainfix &lt;=c0V7AainvV5ACfaEmpfaStrwwwainfix =V11V5Oainfix =V10V5aAppVVwV0Lainfix -V1V6ainfix =amixfix []astringV4V1amixfix []astringV0V1Aainfix &lt;V1Cc0aEmpV12aStrwwVV13aAppwwVV4Aainfix &lt;=c0V1AainvV4ACfaEmpfaStrwwwainfix =V15V4Oainfix =V14V4aAppVVwV0ainfix &lt;V1V6LCc0aEmpV16aStrwwVV17aAppwwVV4aAppVVwV0Iainfix &lt;V1Cc0aEmpV18aStrwwVV19aAppwwVV0Aainfix &lt;=c0V1AainvV0F">
+    <label
+     name="expl:VC for get"/>
+    <transf
+     name="split_goal_wp"
+     proved="true"
+     expanded="true">
+     <goal
+      name="WP_parameter get.1"
+      locfile="../ropes.mlw"
+      loclnum="120" loccnumb="10" loccnume="13"
+      expl="1. unreachable point"
+      sum="89aad05b35e2b576108ba50a784a2a17"
+      proved="true"
+      expanded="false"
+      shape="unreachable pointCfaEmptaStrVVwtaAppVVwV0Iainfix &lt;V1Cc0aEmpV6aStrwwVV7aAppwwVV0Aainfix &lt;=c0V1AainvV0F">
+      <label
+       name="expl:VC for get"/>
+      <proof
+       prover="0"
+       timelimit="10"
+       memlimit="1000"
+       obsolete="false"
+       archived="false">
+       <result status="valid" time="0.01"/>
+      </proof>
+     </goal>
+     <goal
+      name="WP_parameter get.2"
+      locfile="../ropes.mlw"
+      loclnum="120" loccnumb="10" loccnume="13"
+      expl="2. postcondition"
+      sum="9ec250bc36ca76c0f194e25de8c2966e"
+      proved="true"
+      expanded="false"
+      shape="postconditionCtaEmpainfix =amixfix []V2ainfix +V3V1amixfix []astringV0V1aStrVVwtaAppVVwV0Iainfix &lt;V1Cc0aEmpV6aStrwwVV7aAppwwVV0Aainfix &lt;=c0V1AainvV0F">
+      <label
+       name="expl:VC for get"/>
+      <proof
+       prover="0"
+       timelimit="10"
+       memlimit="1000"
+       obsolete="false"
+       archived="false">
+       <result status="valid" time="0.03"/>
+      </proof>
+     </goal>
+     <goal
+      name="WP_parameter get.3"
+      locfile="../ropes.mlw"
+      loclnum="120" loccnumb="10" loccnume="13"
+      expl="3. variant decrease"
+      sum="b67bf33eb3cc79bb3e5ef8368b68d517"
+      proved="true"
+      expanded="false"
+      shape="variant decreaseCtaEmptaStrVVwCfaEmpfaStrwwwainfix =V8V4Oainfix =V7V4aAppVVwV0Iainfix &lt;V1V6LCc0aEmpV9aStrwwVV10aAppwwVV4aAppVVwV0Iainfix &lt;V1Cc0aEmpV11aStrwwVV12aAppwwVV0Aainfix &lt;=c0V1AainvV0F">
+      <label
+       name="expl:VC for get"/>
+      <proof
+       prover="0"
+       timelimit="10"
+       memlimit="1000"
+       obsolete="false"
+       archived="false">
+       <result status="valid" time="0.02"/>
+      </proof>
+     </goal>
+     <goal
+      name="WP_parameter get.4"
+      locfile="../ropes.mlw"
+      loclnum="120" loccnumb="10" loccnume="13"
+      expl="4. precondition"
+      sum="63a96e9f5c7a491a06a0f48d16e350e1"
+      proved="true"
+      expanded="false"
+      shape="preconditionCtaEmptaStrVVwainfix &lt;V1Cc0aEmpV7aStrwwVV8aAppwwVV4Aainfix &lt;=c0V1AainvV4Iainfix &lt;V1V6LCc0aEmpV9aStrwwVV10aAppwwVV4aAppVVwV0Iainfix &lt;V1Cc0aEmpV11aStrwwVV12aAppwwVV0Aainfix &lt;=c0V1AainvV0F">
+      <label
+       name="expl:VC for get"/>
+      <proof
+       prover="0"
+       timelimit="10"
+       memlimit="1000"
+       obsolete="false"
+       archived="false">
+       <result status="valid" time="0.03"/>
+      </proof>
+     </goal>
+     <goal
+      name="WP_parameter get.5"
+      locfile="../ropes.mlw"
+      loclnum="120" loccnumb="10" loccnume="13"
+      expl="5. postcondition"
+      sum="4ce40f215e6b5c85767a8fad17492c14"
+      proved="true"
+      expanded="true"
+      shape="postconditionCtaEmptaStrVVwainfix =amixfix []astringV4V1amixfix []astringV0V1Iainfix &lt;V1Cc0aEmpV7aStrwwVV8aAppwwVV4Aainfix &lt;=c0V1AainvV4Iainfix &lt;V1V6LCc0aEmpV9aStrwwVV10aAppwwVV4aAppVVwV0Iainfix &lt;V1Cc0aEmpV11aStrwwVV12aAppwwVV0Aainfix &lt;=c0V1AainvV0F">
+      <label
+       name="expl:VC for get"/>
+      <proof
+       prover="0"
+       timelimit="10"
+       memlimit="1000"
+       obsolete="false"
+       archived="false">
+       <result status="valid" time="0.03"/>
+      </proof>
+     </goal>
+     <goal
+      name="WP_parameter get.6"
+      locfile="../ropes.mlw"
+      loclnum="120" loccnumb="10" loccnume="13"
+      expl="6. variant decrease"
+      sum="7f73ae5b0544744a8bb87d6c5184a80d"
+      proved="true"
+      expanded="false"
+      shape="variant decreaseCtaEmptaStrVVwCfaEmpfaStrwwwainfix =V9V5Oainfix =V8V5aAppVVwV0Lainfix -V1V6INainfix &lt;V1V6LCc0aEmpV10aStrwwVV11aAppwwVV4aAppVVwV0Iainfix &lt;V1Cc0aEmpV12aStrwwVV13aAppwwVV0Aainfix &lt;=c0V1AainvV0F">
+      <label
+       name="expl:VC for get"/>
+      <proof
+       prover="0"
+       timelimit="10"
+       memlimit="1000"
+       obsolete="false"
+       archived="false">
+       <result status="valid" time="0.03"/>
+      </proof>
+     </goal>
+     <goal
+      name="WP_parameter get.7"
+      locfile="../ropes.mlw"
+      loclnum="120" loccnumb="10" loccnume="13"
+      expl="7. precondition"
+      sum="5dbfcae409f9bc13b582f741b9cf8fad"
+      proved="true"
+      expanded="false"
+      shape="preconditionCtaEmptaStrVVwainfix &lt;V7Cc0aEmpV8aStrwwVV9aAppwwVV5Aainfix &lt;=c0V7AainvV5Lainfix -V1V6INainfix &lt;V1V6LCc0aEmpV10aStrwwVV11aAppwwVV4aAppVVwV0Iainfix &lt;V1Cc0aEmpV12aStrwwVV13aAppwwVV0Aainfix &lt;=c0V1AainvV0F">
+      <label
+       name="expl:VC for get"/>
+      <proof
+       prover="0"
+       timelimit="10"
+       memlimit="1000"
+       obsolete="false"
+       archived="false">
+       <result status="valid" time="0.02"/>
+      </proof>
+     </goal>
+     <goal
+      name="WP_parameter get.8"
+      locfile="../ropes.mlw"
+      loclnum="120" loccnumb="10" loccnume="13"
+      expl="8. postcondition"
+      sum="e3a44ec65e45648a5f560a9635f7d47c"
+      proved="true"
+      expanded="true"
+      shape="postconditionCtaEmptaStrVVwainfix =amixfix []astringV5V7amixfix []astringV0V1Iainfix &lt;V7Cc0aEmpV8aStrwwVV9aAppwwVV5Aainfix &lt;=c0V7AainvV5Lainfix -V1V6INainfix &lt;V1V6LCc0aEmpV10aStrwwVV11aAppwwVV4aAppVVwV0Iainfix &lt;V1Cc0aEmpV12aStrwwVV13aAppwwVV0Aainfix &lt;=c0V1AainvV0F">
+      <label
+       name="expl:VC for get"/>
+      <proof
+       prover="0"
+       timelimit="10"
+       memlimit="1000"
+       obsolete="false"
+       archived="false">
+       <result status="valid" time="0.04"/>
+      </proof>
+     </goal>
+    </transf>
+   </goal>
+  </theory>
+ </file>
+</why3session>