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.
|Path to example file||layers/LFQ.java|
|Lines of code||210 lines (comments not included)|
|Lines of specification||80 lines (38.1% of the total)|
|Computation time||39824 milliseconds|
Note, verification may take a while and has a time-out of 20 seconds.