Wiki Agenda Contact English version

VerifyThis 2018: mind the gap

solution to VerifyThis 2018 challenge 1


Auteurs: Martin Clochard

Catégories: Array Data Structure / Data Structures

Outils: Why3

Références: 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 = S.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


download ZIP archive

Why3 Proof Results for Project "verifythis_2018_mind_the_gap_1"

Theory "verifythis_2018_mind_the_gap_1.Top": fully verified

ObligationsAlt-Ergo 2.1.0
VC for gap_buffer0.01
VC for left0.04
VC for right0.07
VC for delete0.06
VC for grow0.05
VC for insert0.32