programs: ropes

examples/programs/ropes.mlw

 
 {
-  type char
-
-  use array.ArrayLength as S
-
-  type string = S.t char
-
-  logic empty_string : string
+  use string.String as S
+  type string = S.t
 
   type rope =
     | Str string (*ofs:*) int (len: int)
     | App rope rope (len: int)
 
+  logic inv (r: rope) = match r with
+    | Str s ofs len -> 0 <= ofs < S.length s and ofs + len <= S.length s
+    | App l r len   -> 0 < len l and 0 < len r
+    end
+
+  logic model (r: rope) : string = match r with
+    | Str s ofs len -> S.sub s ofs len
+    | App l r _     -> S.app (model l) (model r)
+    end
+
 }
 
-let empty () = Str empty_string 0 0
+let empty () = Str (S.create 0) 0 0
 
 let length r = len r
 

theories/string.why

+
+theory String
+
+  use import int.Int
+
+  type char
+
+  type t
+
+  logic get t int : char
+  logic set t int char : t
+  
+  axiom Get_set_eq : 
+    forall s : t. forall i j : int. 
+    forall c : char [get (set s i c) j].
+    i = j -> get (set s i c) j = c
+
+  axiom Get_set_neq : 
+    forall s : t. forall i j : int. 
+    forall c : char [get (set s i c) j].
+    i <> j -> get (set s i c) j = get s j
+
+  logic length t : int
+
+  logic create int : t
+
+  axiom Create_length : 
+    forall n : int. length (create n) = n
+
+  axiom Length_set : 
+    forall s : t. forall i : int. forall c : char.
+    length (set s i c) = length s
+
+  logic sub t int int : t
+
+  logic app t t : t
+
+end