Merge branch '863-forward-propagation-strategy-accept-optionnal-arguments' into ...
[why3.git] / examples / verifythis_2018_mind_the_gap_2.mlw
blob4c3ca13b07dcf29929da2ce721cc6de88ee7e453
1 (**
3 {1 VerifyThis @ ETAPS 2018 competition
4    Challenge 1: Mind the gap}
6 Author: Raphaël Rieu-Helft (LRI, Université Paris Sud)
7 *)
9 module GapBuffer
11   use int.Int
12   use seq.Seq
13   use map.Map
14   use array.Array
16   type char
17   val constant dummy_char : char
19   type buffer =  {
20     mutable data : array char;
21     mutable l : int;
22     mutable r : int
23   } invariant { 0 <= l <= r <= data.length }
24   by { data = make 1 dummy_char; l = 0; r = 0 }
26   function len_contents (b:buffer) : int
27     = b.data.length - b.r + b.l
29   function contents (b:buffer) : int -> char
30     = fun i -> if 0 <= i < b.l then b.data.elts i
31                else if b.l <= i <= len_contents b
32                     then b.data.elts (i+b.r-b.l)
33                     else dummy_char
35   function cursor_pos (b:buffer) : int = b.l
37   predicate same_contents (b1 b2:buffer)
38   = len_contents b1 = len_contents b2
39       /\ forall i. 0 <= i < len_contents b1 ->
40                    contents b1 i = contents b2 i
42   val b: buffer
44   let left ()
45     ensures { if old b.l = 0
46               then b = old b
47               else cursor_pos b = cursor_pos (old b) - 1 }
48     ensures { same_contents b (old b) }
49   = if b.l <> 0
50     then begin
51       b.l <- b.l - 1;
52       b.r <- b.r - 1;
53       b.data[b.r] <- b.data[b.l]
54     end
56   let right ()
57     ensures { if old b.r = old b.data.length
58               then b = old b
59               else cursor_pos b = cursor_pos (old b) + 1 }
60     ensures { same_contents b (old b) }
61   = if b.r <> b.data.length
62     then begin
63       b.data[b.l] <- b.data[b.r];
64       b.l <- b.l + 1;
65       b.r <- b.r + 1
66     end
68   let constant k = 42
70   let grow ()
71     ensures { b.l = old b.l }
72     ensures { b.r = old b.r + k }
73     ensures { same_contents b (old b) }
74   = let ndata = Array.make (b.data.length + k) dummy_char in
75     Array.blit b.data 0 ndata 0 b.l;
76     Array.blit b.data b.r ndata (b.r + k) (b.data.length - b.r);
77     b.r <- b.r + k;
78     b.data <- ndata
81   predicate contents_inserted (newb oldb: buffer) (x:char) (pos:int)
82   = len_contents newb = len_contents oldb + 1
83     /\ 0 <= pos <= len_contents oldb
84     /\ (forall i. 0 <= i < pos -> contents newb i = contents oldb i)
85     /\ contents newb pos = x
86     /\ (forall i. pos < i < len_contents newb ->
87                   contents newb i = contents oldb (i-1))
89   let insert (x:char)
90     ensures  { cursor_pos b = old cursor_pos b + 1 }
91     ensures  { contents_inserted b (old b) x (old b.l) }
92   =
93     if b.l = b.r then grow ();
94     b.data[b.l] <- x;
95     b.l <- b.l + 1
98   predicate contents_deleted (newb oldb: buffer) (pos:int)
99   = len_contents newb = len_contents oldb - 1
100     /\ 0 <= pos < len_contents oldb
101     /\ (forall i. 0 <= i < pos -> contents newb i = contents oldb i)
102     /\ (forall i. pos <= i < len_contents newb ->
103                   contents newb i = contents oldb (i+1))
104   let delete ()
105     ensures { if cursor_pos (old b) = 0
106               then b = old b
107               else cursor_pos b = old cursor_pos b - 1
108                    /\ contents_deleted b (old b) (old b.l - 1) }
109   = if b.l <> 0
110     then b.l <- b.l - 1
111     else ()