Download Samples
Below you can download the source code of a few of the case studies used to test the performance, and the output of the tool. All the packages are composed by Java classes with JML annotations.
Linked Queue (zip 8Kbs)
| LinkedNode.java | LinkedQueue.java | LinkedQueueDriver.java | Process.java
Bounded Buffer (zip 8Kbs)
| BoundedBuffer.java | Consumer.java | Producer.java | ProducerConsumer.java
Dinning Philosophers (zip 4Kbs)
| DiningPhilosophers.java | DiningServer.java | Philosopher.java
Mathematical Functions (zip 4Kbs)
| AuxFunctions.java | Functions.java | Math.java