## VerifyThis 2018: mind the gap (alt)

solution to VerifyThis 2018 challenge 1

Authors: Raphaël Rieu-Helft

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: Raphaël Rieu-Helft (LRI, Université Paris Sud)

```module GapBuffer

use int.Int
use seq.Seq
use map.Map
use array.Array

type char
val constant dummy_char : char

type buffer =  {
mutable data : array char;
mutable l : int;
mutable r : int
} invariant { 0 <= l <= r <= data.length }
by { data = make 1 dummy_char; l = 0; r = 0 }

function len_contents (b:buffer) : int
= b.data.length - b.r + b.l

function contents (b:buffer) : int -> char
= fun i -> if 0 <= i < b.l then b.data.elts i
else if b.l <= i <= len_contents b
then b.data.elts (i+b.r-b.l)
else dummy_char

function cursor_pos (b:buffer) : int = b.l

predicate same_contents (b1 b2:buffer)
= len_contents b1 = len_contents b2
/\ forall i. 0 <= i < len_contents b1 ->
contents b1 i = contents b2 i

val b: buffer

let left ()
ensures { if old b.l = 0
then b = old b
else cursor_pos b = cursor_pos (old b) - 1 }
ensures { same_contents b (old b) }
= if b.l <> 0
then begin
b.l <- b.l - 1;
b.r <- b.r - 1;
b.data[b.r] <- b.data[b.l]
end

let right ()
ensures { if old b.r = old b.data.length
then b = old b
else cursor_pos b = cursor_pos (old b) + 1 }
ensures { same_contents b (old b) }
= if b.r <> b.data.length
then begin
b.data[b.l] <- b.data[b.r];
b.l <- b.l + 1;
b.r <- b.r + 1
end

let constant k = 42

let grow ()
ensures { b.l = old b.l }
ensures { b.r = old b.r + k }
ensures { same_contents b (old b) }
= let ndata = Array.make (b.data.length + k) dummy_char in
Array.blit b.data 0 ndata 0 b.l;
Array.blit b.data b.r ndata (b.r + k) (b.data.length - b.r);
b.r <- b.r + k;
b.data <- ndata

predicate contents_inserted (newb oldb: buffer) (x:char) (pos:int)
= len_contents newb = len_contents oldb + 1
/\ 0 <= pos <= len_contents oldb
/\ (forall i. 0 <= i < pos -> contents newb i = contents oldb i)
/\ contents newb pos = x
/\ (forall i. pos < i < len_contents newb ->
contents newb i = contents oldb (i-1))

let insert (x:char)
ensures  { cursor_pos b = old cursor_pos b + 1 }
ensures  { contents_inserted b (old b) x (old b.l) }
=
if b.l = b.r then grow ();
b.data[b.l] <- x;
b.l <- b.l + 1

predicate contents_deleted (newb oldb: buffer) (pos:int)
= len_contents newb = len_contents oldb - 1
/\ 0 <= pos < len_contents oldb
/\ (forall i. 0 <= i < pos -> contents newb i = contents oldb i)
/\ (forall i. pos <= i < len_contents newb ->
contents newb i = contents oldb (i+1))
let delete ()
ensures { if cursor_pos (old b) = 0
then b = old b
else cursor_pos b = old cursor_pos b - 1
/\ contents_deleted b (old b) (old b.l - 1) }
= if b.l <> 0
then b.l <- b.l - 1
else ()

end
```