Examples

A list of examples is presented categorized in several groups:

Sequential Examples.

This section contains examples that show how sequential code can be annotated and verified with Boogie as a backend.

Java examples
BoogieTest.java - A class containing a list of simple sequential methods.
LoopInv.java - A class with a loop, showing a specification with a loop invariant.
BoogieExample.java - An example of a recursive method.
BoogieWithGlobals.java - An example of a class with static fields.

PVL examples
boogie-example.pvl - An example of a recursive method.
loopinv-pvl.pvl - A class with a loop, showing a specification with a loop invariant.
nested-loops.pvl - A class with nested loops.

Concurrent Examples.

Contains a series of examples that show how a program with separation logic annotations, such as (abstract) predicates and the magic wand can be verified. This verification uses a style of annotations in which at the specification or ghost level, the resources are treated as objects called witnesses. Intuitively witnesses are objects, which stand for resources such as variables access permissions. Methods on witness objects correspond to proofs.

Specifications with separation logic permissions

Java examples
BadLoop1.java - An example with a loop iteration, with invalidated assertions.
BadLoop2.java - An example with a loop iteration, with invalidated assertions.
Counter.java - Using permissions in Counter class implementation.
Incr.java - Using permissions in incrementing a value.
MultiIncrement.java - Using permissions in incrementing values.
RosterFixed.java - An example using permissions in predicates (The example is taken from C. Hurlin. Speci cation and Veri cation of Multithreaded Object-Oriented Programs with Separation Logic. PhD thesis.)
SwapDouble.java - An example of swapping two double values.
SwapInteger.java - An example of swapping two integer values.
SwapLong.java - An example of swapping two long values.
TreeStack.java - An example of a stack of binary trees.

PVL examples
box.pvl - A simple PVL example verified in Chalice.

Specifications with predicates without arguments

Java examples
IntegerList.java - Using recursive predicates in a linked list of integers.
TreeRecursive.java - Using recursive predicates in a binary tree with integer data.
WandDemo.java - An example of using magic wand.

PVL examples
minimax-list.pvl - Using predicates in a PVL linked list.

Encoding of predicates with arguments
CounterState.java - A class representing a counter using witness encoding of predicates with arguments.
Getters.java - An example of using getters in combination with the witness encoding of predicates with arguments
List.java - An example showing the use of the given keyword and a magic wand to prove the iterative implementation of list append correct.
ListIterator.java - An example of a ListIterator, using encoding of predicates with arguments.
Roster.java - An example of using witness encoding of predicates with arguments taken from C. Hurlin. Speci cation and Veri cation of Multithreaded Object-Oriented Programs with Separation Logic. PhD thesis..
TreeWand.java - Shows the deletion of a node from a binary search tree.
Twice.java - An example of using witness encoding of predicates with arguments.

Verification of arrays
ZeroArray.java - An example of using an array.

Verification of programs with class inheritance
Thread.java - Specification of a Thread class.
Fibonacci.java - Implementation of Fibonacci class that extends the Thread class.
Instance.java - A class representing a thread instance (extends the Thread class).
Main.java - A class that uses a thread Instance class.
Point.java - A class representing a two-dimensional point.
PointZ.java - A class representing a three-dimensional point (extends the Point class).
SimpleThread.java - Specification of a Thread class.
SimpleThreadInstance.java - A class representing a thread instance (extends the SimpleThread class).
SimpleThreadMain.java - A class that uses a SimpleThreadInstance class.
Visitor.java - Using inheritance within the Visitor pattern.

Atomic Classes
AtomicReadWrite.java
DWLock.java - A single-entrant lock which uses deposit-withdraw approach of AtomicInteger specification.
RBLock.java - A single-entrant spin lock using AtomicInteger as synchronizer.
RBProdCons.java - Single producer and single-consumer verification using AtomicInteger.
RBSingleCell.java - A simplified version of the single method lock-less hash-table using AtomicInteger as synchronizer.
The contracts for the AtomicInteger is the version without magic-wand (delta)
ReentLock.java - ReentrantLock class, a synchronizer that uses AtomicInteger as a synchronization primitive.
SingleCell.java - An example of using AtomicInteger to protect data field of SingleCell.

AtomicInteger as a primitive synchronizer: Exclusive ownership

AtomicInteger.java (Exclusive) - Specification of AtomicInteger class as an exclusive primitive synchronizer.
ProdCons.java - SingleProducer-SingleConsumer - an example of pure cooperative pattern synchronized using AtomicInteger.
SpinLock.java - Pure competitive pattern synchronizer using AtomicInteger.

Shared-Reading synchronizers using AtomicInteger

AtomicInteger.java (Shared) - Specification of AtomicInteger class as a shared primitive synchronizer.
ReentLock.java - Specification of a ReentrantLock synchronizer using AtomicInteger as a synchronization primitive.
Semaphore.java - Specification of a Semaphore synchronizer using AtomicInteger as a synchronization primitive.
CountDownLatch.java - Specification of a CountDownLatch synchronizer using AtomicInteger as a synchronization primitive.

Verification of programs with Locks
Lock.java - A simple implementation of a Lock class and a client that uses a Lock object.

Examples using forking and joining threads
fibonacci.pvl - An implementation of Fibonacci.
update-point.pvl - Simple example of a client class starting two parallel threads.

Examples using Java generics
GenericVar.java - Simple example using generics.

Examples using CaseSet
CaseSetTest.java - Simple example using CaseSet.

OpenCL Kernel Examples.

In this section the OpenCL kernel verfication method of the CARP project is demonstrated.
zero.pvl - A simple kernel example.
zero-e1.pvl - A simple kernel example with violated assertion.
scp-example.pvl - An example of a kernel using barrier.
scp-example-e1.pvl - An example of a kernel using barrier with violated assertion.
binomial.pvl - An example of a kernel using barrier in a loop.
binomial-e1.pvl - An example of a kernel using barrier in a loop with violated assertion.