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

ArticleFTfJP 2018: An Exercise in Verifying Sequential Programs with VerCors
FeaturesArrays, Loop invariants, Sequences
SourcesVerifyThis competition 2018
Path to example fileverifythis2018/challenge1.pvl

Statistical information

Lines of code231 lines (comments not included)
Lines of specification144 lines (62.34% of the total)
Computation timeunknown

Example code

Note, verification may take a while and has a time-out of 20 seconds.