Electronicdesign 6017 59321promo
Electronicdesign 6017 59321promo
Electronicdesign 6017 59321promo
Electronicdesign 6017 59321promo
Electronicdesign 6017 59321promo

Contract-Driven Programming Takes Specification Beyond The Stone Age

Feb. 4, 2013
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.

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

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

Quentin Ochem has a software engineering background, specialized in software development for critical applications. He has over 10 years of experience in Ada development. He works today as a technical account manager for AdaCore, following projects related to the avionics, railroad, space, and defense industries. He also teaches the avionics standard DO-178B course at the EPITA University in Paris. He can be reached at [email protected].

Sponsored Recommendations

Board-Mount DC/DC Converters in Medical Applications

March 27, 2024
AC/DC or board-mount DC/DC converters provide power for medical devices. This article explains why isolation might be needed and which safety standards apply.

Use Rugged Multiband Antennas to Solve the Mobile Connectivity Challenge

March 27, 2024
Selecting and using antennas for mobile applications requires attention to electrical, mechanical, and environmental characteristics: TE modules can help.

Out-of-the-box Cellular and Wi-Fi connectivity with AWS IoT ExpressLink

March 27, 2024
This demo shows how to enroll LTE-M and Wi-Fi evaluation boards with AWS IoT Core, set up a Connected Health Solution as well as AWS AT commands and AWS IoT ExpressLink security...

How to Quickly Leverage Bluetooth AoA and AoD for Indoor Logistics Tracking

March 27, 2024
Real-time asset tracking is an important aspect of Industry 4.0. Various technologies are available for deploying Real-Time Location.

Comments

To join the conversation, and become an exclusive member of Electronic Design, create an account today!