Challenge one from the VerifyThis2018 competition: specifying and verifying the behaviour of a gap buffer; a data-structure commonly used in text editors. In particular, we verify the correctness of four standard operations on gap buffers, for moving the text cursor (functions 'left' and 'right'); for inserting a character at the cursors' position (function 'insert'); and for deleting the character at the cursors' position (function 'delete'). Our general approach to show functional correctness is to represent the buffer’s content as a sequence of integers. We prove that, after executing one of the four functions, the contents of the buffer is still validly represented by the proper integer sequence.

General Information

  • Backend: Silicon
  • Language: PVL
  • Features: Sequences, Arrays, Loop invariants
  • Path to Example File: verifythis2018/challenge1.pvl
  • Should Verify: Yes
  • Date: 2018-05-09
  • Lines of Code: 231 (comments not included)
  • Lines of Specification: 144 (62.3% of total)