examples/verifythis_2018_mind_the_gap_2.mlw

   1 (**
   2
   3 {1 VerifyThis @ ETAPS 2018 competition
   4    Challenge 1: Mind the gap}
   5
   6 Author: Raphaël Rieu-Helft (LRI, Université Paris Sud)
   7 *)
   8
   9 module GapBuffer
  10
  11   use int.Int
  12   use seq.Seq
  13   use map.Map
  14   use array.Array
  15
  16   type char
  17   val constant dummy_char : char
  18
  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 }
  25
  26   function len_contents (b:buffer) : int
  27     = b.data.length - b.r + b.l
  28
  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
  34
  35   function cursor_pos (b:buffer) : int = b.l
  36
  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
  41
  42   val b: buffer
  43
  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
  55
  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
  67
  68   let constant k = 42
  69
  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
  79
  80
  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))
  88
  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
  96
  97
  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 ()
 112
 113
 114 end