Database system for managing exams
June 22, 2010 – 6 years, 9 months ago, by eifler
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.
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.
Timo Eifler firstname.lastname@example.org
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
Interactivity, effort needed
All method contracts can be veriﬁed 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 ﬁrst 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 veriﬁed automatically with
KeY and which need interaction can be found in the original document submitted by Christian Engel.
Uploaded by Timo Eifler email@example.com