Formal Specifications Investigated: A Classification and Analysis of Annotations for Deductive Verifiers

Deductive verification can be used to ensure properties about all possible behaviours of a program, even when the program is parameterised and has an unbounded state space. But to achieve this, the user needs to specify what the desired properties are, and often needs to guide the prover with auxiliary annotations. This paper investigates what annotations are actually needed, and it provides a taxonomy to categorise these annotations. In particular, we identify several top-level categories, which are further divided into subcategories of annotations. This taxonomy is then used as a basis to investigate how often particular annotation categories occur, by inspecting over 10k lines of annotated programs. To determine whether the results are in line with expectations, we have interviewed several experts on deductive verification. Moreover, we show how the results can be used to evaluate the effectiveness of annotation generators. The knowledge from this analysis provides a gateway to guide further research in improving the efficiency of deductive verification, e.g.: it can serve as a guideline on what categories of annotations should be generated automatically, to evaluate the power of existing annotation generation techniques, and to improve the teaching of deductive verification.