examples/verifythis_2018_mind_the_gap_1.mlw

   1 (**
   2
   3 {1 VerifyThis @ ETAPS 2018 competition
   4    Challenge 1: Mind the gap}
   5
   6 Author: Martin Clochard (LRI, Université Paris Sud)
   7 *)
   8
   9 use int.Int
  10 use import seq.Seq as S
  11 use array.Array
  12
  13 type char
  14 val constant any_char : char
  15
  16 (* gap buffer model: content (buffer content) + l (location in buffer). *)
  17 type gap_buffer = {
  18   mutable a : array char;
  19   mutable l : int;
  20   mutable r : int;
  21   mutable ghost content : seq char;
  22 } invariant { 0 <= l <= r <= a.length }
  23 invariant { a.length = content.S.length + r - l }
  24 invariant { forall i. 0 <= i < l -> S.get content i = a.elts i }
  25 invariant { forall i. l <= i < content.S.length ->
  26                         S.get content i = a.elts (i+r-l) }
  27 by { a = make 0 any_char; l = 0; r = 0; content = empty }
  28
  29 let left (g:gap_buffer) : unit
  30   ensures  { g.l = old (if g.l = 0 then g.l else g.l - 1) }
  31   ensures  { g.content = old g.content }
  32 = if g.l <> 0 then begin
  33     g.l <- g.l - 1;
  34     g.r <- g.r - 1;
  35     g.a[g.r]<- g.a[g.l]
  36   end
  37
  38 let right (g:gap_buffer) : unit
  39   ensures { g.l = old (if g.l = g.content.S.length then g.l else g.l + 1) }
  40   ensures { g.content = old g.content }
  41 = if g.r <> g.a.length then begin
  42     g.a[g.l] <- g.a[g.r];
  43     g.l <- g.l + 1;
  44     g.r <- g.r + 1
  45   end
  46
  47 let delete (g:gap_buffer) : unit
  48   ensures { if old g.l = 0 then g = old g else
  49     g.l = old g.l - 1 /\
  50     g.content = old (g.content[.. g.l - 1] ++ g.content[g.l ..]) }
  51 = if g.l <> 0 then begin
  52     ghost (g.content <- g.content[.. g.l - 1] ++ g.content[g.l ..]);
  53     g.l <- g.l - 1;
  54   end
  55
  56 (* Send back the capacity increment without modifying buffer.
  57    Implemented by a constant (K) in the problem statement.
  58    This version is more general and account for the standard doubling pattern
  59    as well. *)
  60 val growth (g:gap_buffer) : int ensures { result > 0 }
  61
  62 (* Since it is an internal primitive, it is fine to refer to r as well. *)
  63 let grow (g:gap_buffer) : unit
  64   ensures { g.l = old g.l /\ g.content = old g.content }
  65   ensures { g.l < g.r }
  66 = let k = growth g in
  67   let b = Array.make (g.a.length + k) any_char in
  68   Array.blit g.a 0 b 0 g.l;
  69   Array.blit g.a g.r b (g.r + k) (g.a.length - g.r);
  70   g.r <- g.r + k;
  71   g.a <- b
  72
  73 let insert (g:gap_buffer) (x:char) : unit
  74   ensures { g.l = old g.l + 1 }
  75   ensures { g.content = old (g.content[.. g.l] ++ cons x g.content[g.l ..]) }
  76 = if g.l = g.r then grow g;
  77   ghost (g.content <- g.content[.. g.l] ++ cons x g.content[g.l ..]);
  78   g.a[g.l] <- x;
  79   g.l <- g.l + 1
  80
  81