Sequences for Specification

title:Sequences for Specification
topics:Logics and semantics, Software Technology
contact:prof.dr. M. Huisman & S.J.C. Joosten


Sequences are a very useful mechanism to describe the intended behaviour of a program. Many program verification tools provide some built-in support to use sequences in the program annotations.

This project considers sequences as they are built-in to the annotation language of the VerCors program verification tool (see for a general description of the VerCors tool, and for a description of the current support for sequences). The support for sequences is still very limited. Goal of this exercise is to extend the built-in support, by adding several useful functions and properties.

Steps to be taken:

  • understand how sequences are built-in to the VerCors annotation language
  • define several useful functions for sequences, including an indexing operator, and add those to the built-in annotation language
  • define properties for the new functions, such that they can be used in the verification