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