Specification Languages Survey Examples

We have attempted to write our survey paper's examples in each of several specification languages. This page gives access to (text) files containing these examples.

Example	Dafny	JML	J Star	Spark
Examples from Section 2: Input/Output Behavior
Structured Assertions (Figs. 1, 4, and 5)	Find.dfy	StructuredAssertions.java	StructuredAssertions.ada	StructuredAssertions.ssc
Refinement (Fig. 2)	RefinementPackage.java RefinementBody.java	Refinement.ada	Refinement.ssc
Relational Postconditions (Fig. 3)	Relational.dfy	Relational.java	Relational.ada	RelationalPostcondition.ssc
Exceptional Behavior (Fig. 6)	Stack.java	ExceptionalBehavior.ssc
Examples from Section 3: Modules
Ghost Variables (Fig. 7)	Counter-ghost.dfy	CounterGhost.java	Counter-ghost.ssc
Model Variables (Fig. 8)	CounterModel.java	Counter-model.ssc
Logic Functions	Counter-function.dfy	CounterFunction.java	not supported by Spec#
Pure Methods (Fig. 9)	CounterPureMethod.java	Counter-puremethod.ssc
Examples from Section 4: Objects and the Heap
Unbounded Stack (Figs. 10-14)	DNode.dfy Node.dfy DUnboundedStack.dfy UnboundedStack.dfy	UnboundedStack.java	UnboundedStack.jstar	UnboundedStack.ssc (does not verify) UnboundedStack_NotGeneric.ssc
Examples from Section 5: Subtyping and Inheritance
Collection (Figs. 15 and 16)	Collection.dfy	Collection.java CollectionTest.java	Collection.ssc
ArrayList (Fig. 17)	ArrayList.dfy	ArrayList.java	ArrayList.ssc