Contract-Driven Programming Takes Specification Beyond The Stone Age

This article is part of the Embedded Software Series: Enforced Coding Using Ada Contracts

Take any interface you use in your daily work. It may be the application programming interface (API) from a standard component, some internal library shared within your company, or a piece of code some guy in the next cubicle is developing for you. How would you know what to call it?

Modern languages provide various ways to identify services as well as various means to refer to those services, through typing, function declarations, or parameter specifications. Certain languages may give you a little bit more. Java specifies what exceptions may be thrown, Ada enables you to specify type ranges, C allows… um, never mind.

This level of specification reveals little about the behavior of the application, though, so there’s the need for something else, informal, not checked by any tool: the infamous documentation, almost exclusively in the form of comments. “Now why is that a problem?” you might say. “It’s already hard enough to get people to comment!”

Documentation is an achievement in a number of situations. But when reliability is at stake, it’s merely a Stone Age specification. How about verifying that the specification is correct? How about verifying that callers make the calls the way they’re supposed to and that they rely on properties they’re supposed to rely on? How about ensuring throughout the lifetime of the project that the specification stays consistent after various fixes, refactorings, and rewritings?

Some alternative techniques go beyond bare comments for specifying behavior and use formalisms checked by tools. Here, we’ll consider three languages in particular: C, Java, and Ada. We’ll also show how, once a specification is written, it can be used not only for documentation but also directly by testing and static analysis tools.

Table of Contents

• Precondition, Postcondition, And Type Invariant
• Java And JML
• C And ACSL
• Ada And Ada 2012
• Testing Executable Annotations
• Helping Static Analysis
• All The Way To Formal Proof?
• Conclusions

Precondition, Postcondition, And Type Invariant

Let’s first introduce the notion of a contract. In programming languages, a contract is typically a Boolean expression that’s verified at certain points in the program. The most interesting contract is probably the postcondition. It defines the properties that must be true after a function call. Typically, it can be a means of specifying the behavior or requirements of that function. It’s a constraint put on the implementer (who must fulfill the postcondition in the implementation) and a guarantee given to the caller (who can rely on the postcondition after the call).

To fulfill the postcondition, we normally need two things: a correct implementation of the function and a set of properties that need to be met before the call. These properties are called preconditions. A precondition is a constraint put on the caller (who must fulfill it before the call to ensure proper behavior) and a guarantee given to the implementer (who can rely on the precondition in its implementation). A postcondition is a guarantee given to the caller (the state of the environment after the call) and a constraint on the implementer (what the function has to perform).

A type invariant is a property that must be true at all times for every object of a given type. It can describe value ranges, relationships between fields, and similar properties.

Here, we’ll consider a simple system where physical objects are moved in a two-dimensional environment. Each object is associated with an X and Y coordinate, a size, and an identifier. A function “iterate” is called at each cycle and is responsible for updating the object’s position by a step. Objects will be stored on a list.

In addition to the structural specification, we’ll add some behavioral requirements:

1. X and Y must be within the interval [–200.0, 200].
2. Size must be within the interval [0 .. 100].
3. Except when set to the special non-initialized value, all object IDs must be unique.
4. Iterate must only be called on objects that have been initialized.
5. Iterate cannot change an object’s size or ID.
6. Each movement made by iterate must be smaller than a tenth of the object’s size.

Some of these requirements can clearly be mapped to type invariants, namely 1, 2, and 3, which are proprieties of types and data that must be true throughout the entire life of the program. Others can be mapped to pre-conditions, in particular 4. Finally, requirements 5 and 6 describe the function’s behavior, therefore mapping to post-conditions. Now, it’s possible to implement the above specification using three different languages based on Java, C, and Ada.

Java And JML

Java Modeling Language (JML) is an extension to Java, where the Java code should be compliable using a regular Java complier. Therefore, all JML annotations are written in special java comments, starting with //@ or /*@. Let’s first translate and then comment the code below.

public class Object {
    public static String NO_INIT = 0;

    public int id = NO_INIT;
    public float x, y, size = 0;

    // @ public invariant x >= -200 && x <= 200;
    // @ public invariant y >= -220 && y <= 200;
    // @ public invariant sie >= 0 && size <= 100;

    // @ requires id /= NO_INIT;
    // @ assignable x
    // @ assignable y
    // @ ensures Math.sqrt (Math.pw (\old (x) – x, 2)
    // @   + Math.pow (\old (y) – y, 2)) <= size / 10;
    
    public void iterate () ( { … } )

    public static Object [] list = new Object [100];
    
    // @ public invariant
    // @   (\forall int j; j >= 0 && j < list.size;
    // @     list [j].id.equals (NO_INIT) ||
    // @       (\forall int k; k >= j + 1 && k < list.size;
    // @        !list [j].id.equals (list [k].id)));

The first notable difference between the ACSL and JML examples is that, while JML allows the introduction of executable contracts that can refer to the actual entities in the code, ACSL is currently purely formal. Therefore, the ACSL cannot call “real” functions, but only formal ones, and can reason only on the corresponding formal properties. This is the particular intent of the Math axiomatic, introducing the pow and sqrt formal functions.

The Range_Object axiomatic is defining the range of values for x, y and the size fields of an object. This axiomatic is then used in the type invariant to verify that all instances of the object type respect this axiom. Note as well the \valid (v) construct, which specifies that the pointer must be valid (can be dereferenced).

Other than these two differences, this is pretty close to the JML example. More information on ACSL can be found at http://frama-c.com/acsl.html.

Ada And Ada 2012

One of the major new features of the Ada 2012 language is its ability to include significant contract information in the language definition, without the need for external tools, along with the corresponding dynamic semantics. The code below shows how the same specifications in the previous examples can be written in Ada 2012.

package Object is
  No_Init : constant := 0;
  
  type Object is record
    Id   : Integer := No_Init;
    X, Y : Float range -200.0 .. 200.0 := 0.0;
    Size : Float range 0.0 .. 100.0 := 0.0; 
  end record;
  
  procedure Iterate (V : in out Object)
  with 
    Pre => V.Id /= No_Init,
    Post =>
      V.Size = V.Size'Old and then
      V.Id = V.Id'Old and then
      Sqrt (( V.X = V.X'Old ) ** 2 + (V.Y -V.Y'Old) ** )
        <= V.Size / 10.0;
        
  type Arr is array (Integer range <>) of Object
    with Dynamic_Predicate => 
      (for all J in Arr'Range => 
        Arr (J).Id = No_Init or else
          (for all K in J + 1 .. Arr'Last => 
            Arr (J).Id /= Arr (K.Id));
  List : Arr (1 .. 100);
end Object ;

This is just one example illustrating the kinds of constraints that arise when trying to introduce strong formal prove techniques. This kind of problem can be detected by using constructs a bit more constrained than low-level pointers, such as references in SPARK. There’s much more to say here, but it’s probably the topic for a forthcoming paper.

Conclusion

The industrialization age of programming by contract is opening a new era in software development. Just as development techniques went from assembly to structured languages and from structured languages to object orientation, contract-based programming is providing one more abstraction to software design.

For a long time, these techniques were only available to developers who had some extended mathematical knowledge. Thanks to new formalisms such as Ada 2012, they are now based on semantics understandable by any software developer, democratizing their usage. This is a good time to try them out!

Read more from the Embedded Software Series: Enforced Coding Using Ada Contracts