Wiki Agenda Contact Version française

VerifyThis 2018: mind the gap (alt)

solution to VerifyThis 2018 challenge 1


Authors: Raphaël Rieu-Helft

Topics: Array Data Structure / Data Structures

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

download ZIP archive

Why3 Proof Results for Project "verifythis_2018_mind_the_gap_2"

Theory "verifythis_2018_mind_the_gap_2.GapBuffer": fully verified

ObligationsAlt-Ergo 1.30Z3 4.5.0
VC dummy_char---0.00
VC buffer---0.01
VC left------
split_vc
VC left.0---0.02
VC left.1---0.02
VC left.2---0.02
VC left.3---0.01
VC left.40.02---
VC left.5---0.02
VC left.60.02---
VC right------
split_vc
VC right.0---0.02
VC right.1---0.03
VC right.2---0.02
VC right.3---0.02
VC right.40.02---
VC right.5---0.02
VC right.60.02---
VC k---0.02
VC grow------
split_vc
VC grow.0---0.02
VC grow.1---0.02
VC grow.2---0.02
VC grow.3---0.03
VC grow.4------
split_vc
VC grow.4.0---0.02
VC grow.4.1---0.03
VC grow.5---0.02
VC grow.6---0.02
VC grow.7---0.01
VC grow.8---0.03
VC insert------
split_vc
VC insert.0---0.02
VC insert.1---0.02
VC insert.2---0.04
VC insert.30.02Timeout (1s)
VC insert.4---0.02
VC insert.5---0.02
VC insert.6---0.01
VC insert.70.03Timeout (1s)
VC delete------
split_vc
VC delete.0---0.04
VC delete.1------
split_vc
VC delete.1.0---0.01
VC delete.1.1---0.01
VC delete.1.2------
introduce_premises
VC delete.1.2.0------
inline_goal
VC delete.1.2.0.0------
split_vc
VC delete.1.2.0.0.0---0.04
VC delete.1.2.0.0.1---0.03
VC delete.1.2.0.0.2---0.02
VC delete.1.2.0.0.3---0.02
VC delete.1.2.0.0.4---0.04
VC delete.2---0.01