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