Database system for managing exams

June 22, 2010 – 6 years, 10 months ago, by eifler

Short Description

This example is a small database system for managing exams and providing data and statistics (such as the average mark) about their outcome. For this several sums (such as the sum of marks achieved by all students) need to be computed.


Download link


The specification is provided in form of JML annotations declared directly in the source files. This example uses two non-standard JML constructs: assignable clauses for loops and an \object_creation(T) construct usable in assignable clauses and indicating the creation of objects of a given type T.

Long Description

Supplementary Materials

Submitted by

Timo Eifler



Verified with Key.

The following proof search strategy was used:
Loop treatment: Invariant
Query treatment: Expand
Method treatment: For methods getFirstname, getSurname, getPoints, getBonusPoints, getBackedOut : Expand
In all other cases: Contract


Solution-problem relationship

Interactivity, effort needed

All method contracts can be verified with KeY, most automatically, some need interactive input.

How to reproduce

In the proofs of the contracts for method getGrade, one needs to use the taclet “strictlyPureMethodtoUpdate” at the beginning. For methods increaseStudent, addStudent, setPoints, setBonusPoints and setBackedOut it is advisable to first run an automatic proof search, then apply “update close right” manually and continue automatically. A small variation holds true for methods getNumWithGrade, getAverage and getPassedAverage. An automated proof search will produce several branches before stopping, here it is sensible to prune the proof tree before again applying “update close right”.

A table which shows for each method which of its contracts can be verified automatically with
KeY and which need interaction can be found in the original document submitted by Christian Engel.


Submitted by

Christian Engel

Uploaded by Timo Eifler