Specification Languages Survey Examples

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	Spec#
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