VerifyThis 2018: mind the gap

solution to VerifyThis 2018 challenge 1

Authors: Martin Clochard

Tools: Why3

References: VerifyThis @ ETAPS 2018

see also the index (by topic, by tool, by reference, by year)

VerifyThis @ ETAPS 2018 competition Challenge 1: Mind the gap

Author: Martin Clochard (LRI, Université Paris Sud)

```use int.Int
use import seq.Seq as S
use array.Array

type char
val constant any_char : char

(* gap buffer model: content (buffer content) + l (location in buffer). *)
type gap_buffer = {
mutable a : array char;
mutable l : int;
mutable r : int;
mutable ghost content : seq char;
} invariant { 0 <= l <= r <= a.length }
invariant { a.length = content.S.length + r - l }
invariant { forall i. 0 <= i < l -> S.get content i = a.elts i }
invariant { forall i. l <= i < content.S.length ->
S.get content i = a.elts (i+r-l) }
by { a = make 0 any_char; l = 0; r = 0; content = empty }

let left (g:gap_buffer) : unit
ensures  { g.l = old (if g.l = 0 then g.l else g.l - 1) }
ensures  { g.content = old g.content }
= if g.l <> 0 then begin
g.l <- g.l - 1;
g.r <- g.r - 1;
g.a[g.r]<- g.a[g.l]
end

let right (g:gap_buffer) : unit
ensures { g.l = old (if g.l = g.content.S.length then g.l else g.l + 1) }
ensures { g.content = old g.content }
= if g.r <> g.a.length then begin
g.a[g.l] <- g.a[g.r];
g.l <- g.l + 1;
g.r <- g.r + 1
end

let delete (g:gap_buffer) : unit
ensures { if old g.l = 0 then g = old g else
g.l = old g.l - 1 /\
g.content = old (g.content[.. g.l - 1] ++ g.content[g.l ..]) }
= if g.l <> 0 then begin
ghost (g.content <- g.content[.. g.l - 1] ++ g.content[g.l ..]);
g.l <- g.l - 1;
end

(* Send back the capacity increment without modifying buffer.
Implemented by a constant (K) in the problem statement.
This version is more general and account for the standard doubling pattern
as well. *)
val growth (g:gap_buffer) : int ensures { result > 0 }

(* Since it is an internal primitive, it is fine to refer to r as well. *)
let grow (g:gap_buffer) : unit
ensures { g.l = old g.l /\ g.content = old g.content }
ensures { g.l < g.r }
= let k = growth g in
let b = Array.make (g.a.length + k) any_char in
Array.blit g.a 0 b 0 g.l;
Array.blit g.a g.r b (g.r + k) (g.a.length - g.r);
g.r <- g.r + k;
g.a <- b

let insert (g:gap_buffer) (x:char) : unit
ensures { g.l = old g.l + 1 }
ensures { g.content = old (g.content[.. g.l] ++ cons x g.content[g.l ..]) }
= if g.l = g.r then grow g;
ghost (g.content <- g.content[.. g.l] ++ cons x g.content[g.l ..]);
g.a[g.l] <- x;
g.l <- g.l + 1

```