|title:||Sequences for Specification|
|topics:||Logics and semantics , Software Technology|
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 utwente.nl/vercors for a general description of the VerCors tool, and https://github.com/utwente-fmt/vercors/wiki/Axiomatic-Data-Types 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