Programmers Don't Write Specifications

In practice, programmers rarely seem to write specifications. Even well-educated programmers who understand formalisms do not write them as often as one might hope. One reason that programmers do not write specifications is that they (perhaps mistakenly) perceive that in most cases they do not get enough benefit for their time and effort.

However, having specifications for software is in everyone's interests:

• Specifications enable a wide range of software verification, testing (eg, [1]), and bug-finding (eg,  [2][3][4]) activities. Detecting flaws early makes it easier and less expensive to fix them.
• Specifications facilitate clear communication between programmers, managers, customers, and quality assurance engineers.
• The National Institute of Standards and Technology recently estimated the cost of inadequate software testing on the US economy at close to $60 billion [5].
• We would all be happier if the software that permeates the world around us was more reliable.

So how can we convince programmers to write specifications? All of these benefits of specifications are not immediate to the programmer: they require a sense of delayed-gratification to appreciate. By making specifications executable we can give them the same sense of immediate gratification and perceived cost/benefit ratio as writing code.

We have implemented a language extension to Java that allows the programmer to write specifications in a variant of the Alloy [6] language, and execute those specifications from within regular Java code.

Specification Without Implementation

With our system, a programmer can write a specification for a method and execute it on real input data. The method itself does not have to be implemented. It works like this:

1. The programmer writes the specification as a pred (predicate) inside the Java class of interest. A pred is a member of a class, as a field or a method is. The body of the pred is written in a variant of the Alloy [6] language.
2. Our source-to-source translator produces a .java file that javac compiles to a .class file.
3. Each time the pred in that class files executes:
   1. It dynamically constructs an Alloy model of the current state of the heap.
   2. It then invokes the Alloy analyzer to translate that model into a (large) boolean formula, which is given to an off-the-shelf SAT solver.
   3. The SAT solver finds a solution (if one exists).
   4. Alloy translates that solution back into terms of the executing program.
   5. Our system manipulates the heap so that it embodies the solution.

Specification With Implementation

If the programmer later writes an implementation to correspond to the specification, then he or she gains the usual benefits of having both an implementation and a specification. As mentioned above, these benefits include static verification and bug finding (eg  [2][3][4]), as well as automatic test input generation (eg, [1]).

By having both the specification and the implementation the programmer is more likely to produce software with fewer flaws, and to find and fix those flaws earlier in the development cycle -- ultimately producing a better product for a lower cost.

Example: Hamiltonian Path

(Recall that a Hamiltonian path through a graph is a path that visits every node exactly once. Finding a Hamiltonian path is NP-complete, and is a special case of the travelling salesman problem.)

Our extension to the Java language introduces pred (predicates) as class members, and a new kind of statement for using them. Here's an example of one of these new statements:

        graph | hamsort(graph, s, t)

It says: mutate the object referred to by graph such that it represents a Hamiltonian path from s to t. In this example we already know what we want the source and target nodes to be. In the more complete example that follows, we let the search find s and t for us:

    static void main(String[]) {
        // construct objects for the example
        List graph = new LinkedList();
        Node n0 = new Node("0");  graph.add(n0);
        Node n1 = new Node("1");  graph.add(n1);
        Node n2 = new Node("2");  graph.add(n2);
        n2.next = n0; n0.next = n1; n1.next = null;
        
        // the list is ordered    n0, n1, n2
        // the desired hampath is n2, n0, n1

        // mutate graph such that it represents a hampath from s to t
        Node s, Node t, graph | hamsort(graph, s, t)

        // s == n2
        // t == n1
        // graph is ordered n2, n0, n1

        // use the predicate to check the graph is sorted
        if ( hamsort(graph, s, t) )
            System.out.println("success!");
    }

We've seen three different ways to use a pred:

• to check if a condition holds
• to make a condition hold (ie, search for a solution, and then mutate the heap to embody that solution)
• to make a condition hold and search for multiple things (ie, search for the s, t, and the ordering of graph)

The hamsort predicate is listed below. First it defines the terms indices, firstIndex, and lastIndex in the way one would expect. Then it simply says, for all indices i, if there's an index j that immediately follows i, then the element at index j is the element after the one at index i. This local condition ensures that the ordering of the graph represents a path.

    pred hamsort (List graph, Node source, Node target) {
        let indices = (graph.elts).Node,
        firstIndex = graph'.elts.source,
        lastIndex = graph'.elts.target {
            no firstIndex.~next && no lastIndex.next
            graph.elts[indices] = graph'.elts[indices]
            all i : indices | let j = i.next | 
                some j implies graph'.elts[j] in (graph'.elts[i]).next
        } // end let
    }

Even though, for simplicity of exposition, the nodes in the above example have at most one next node, this predicate will work for nodes that have multiple successors.

There are many imperative algorithms for computing Hamiltonian paths (for example, the survey in [7] examines 13 such algorithms). Even the pseudo-code outline of what one of these algorithms looks like ( [7], figures 2.2 and 2.3) is much longer and more complicated than the above declarative specification. So in this case the programmer has not only gained all of the regular benefits of specifications, but has also found a simpler and more concise way to express the computation: the specification provides the instant-gratification and perceived cost-benefit ratio that the programmer normally associates only with code.

Research Funding

This research was supported by: grant 0086154 ('Design Conformant Software') from the ITR program of the National Science Foundation; and by the High Dependability Computing Program from NASA Ames cooperative agreement NCC-2-1298.

References

[1] Sarfraz Khurshid and Darko Marinov. TestEra: Specification-based Testing of Java Programs Using SAT. Automated Software Engineering Journal, October 2004.

[2] Mana Taghdiri. Inferring Specifications to Detect Errors in Code. In 19th International Conference on Automated Software Engineering (ASE 2004), Linz, Austria, September 2004.

[3] Mandana Vaziri and Daniel Jackson. Checking Heap-Manipulating Procedures with a Constraint Solver. In Tools and Algorithms for Construction and Analysis of Systems (TACAS'03), Warsaw, Poland, 2003.

[5] Gregory Tassey. The Economic Impacts of Inadequate Infrastructure for Software Testing. Technical Report: National Institute of Standards and Technology, 2002.

[6] MIT Software Design Group. Alloy Language and Analyzer.

[7] Basil Vandegriend. Finding Hamiltonian Cycles: Algorithms, Graphs and Performance. Master's Dissertation, University of Alberta, 1998.