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.
FTfJP 2018: An Exercise in Verifying Sequential Programs with VerCors
Arrays, Loop invariants, Sequences
VerifyThis competition 2018
Path to example file
Lines of code
231 lines (comments not included)
Lines of specification
144 lines (62.34% of the total)
Note, verification may take a while and has a time-out of 20 seconds.