Verifying a queue

Verification example in which certain operations on a Queue are verified. The verification example also shows the use of methods/functions as lemmas to do certain parts of the proof.

General information

ID82
Articlenone
Back-endSilicon
LanguageJava
FeaturesAtomics, Lists
Sources
Path to example filelayers/LFQ.java
Date2017-06-19

Statistical information

Lines of code210 lines (comments not included)
Lines of specification80 lines (38.1% of the total)
Computation time39824 milliseconds

Example code

Note, verification may take a while and has a time-out of 20 seconds.