Safe and secure object-oriented programming with Ada 2012's contracts

Benjamin M. Brosgol, AdaCore

August 09, 2014

Benjamin M. Brosgol, AdaCoreAugust 09, 2014

Object-Oriented Programming (OOP) has been a mainstream methodology in many application domains for several decades, since it can help reduce the development and maintenance effort on complex systems as they evolve to meet new requirements.

However, for many reasons OOP has been a hard sell to the high-integrity software community. Software standards such as DO-178C for airborne systems require extensive verification based on reviews and analyses of the static program text, and these activities are complicated by the dynamic flexibility characteristic of OOP.

The Ada 2012 language revision includes several new features that help developers exploit OOP’s advantages while avoiding its vulnerabilities. This article explains one particular facility, the integration of contract-based programming with OOP. Ada 2012 directly supports an important precept of object orientation known as the Liskov Substitution Principle (LSP), and facilitates compliance with both DO-178C and its supplement on Object-Oriented Technology and Related Techniques.

The importance of OOP
With its effective support for component reuse, module encapsulation, and system extensibility, OOP has long been a popular development method in many domains. However, a number of technical issues have stymied its adoption in high-integrity systems such as avionics. Inheritance provides opportunities for a variety of programming errors, and if misused it can complicate verification efforts. Polymorphism brings in the complications of references (‘pointers’) and storage management. Dynamic binding (dispatch) raises issues with code coverage analysis, and more generally highlights the conflict between the run-time flexibility offered by OOP and the need to demonstrate safety and/or security properties based on the static program text.

These issues were elaborated upon and discussed in a series of FAA- and NASA-sponsored workshops on Object-Oriented Technology in Aviation, or OOTiA [1]. During the process of revising the DO-178B software standard [2] to produce DO-178C [3] the potential benefits of OOP were acknowledged, and a working group was established to formulate appropriate guidance. The OOTiA study was used as the starting point, and the end result was DO-332 [4], the DO-178C supplement on Object-Oriented Technology and Related Techniques. DO-332 provides a comprehensive analysis of the vulnerabilities raised by OOP and adapts and extends the DO-178C guidance to deal with them.

Concepts of Object Orientation. A class is a module that defines data fields and operations. A class is also a type for a polymorphic variable and a template that can be instantiated to create objects.

An abstract class is a class that cannot be instantiated to create objects, and that may contain abstract operations (operations without an implementation). An interface is an abstract class with no data fields and no operation implementations (i.e., all operations are abstract).

A class (as a module) can encapsulate its fields and operations by specifying their accessibility from different parts of the program.

A new class (the subclass) can extend another class (the superclass) through inheritance. The subclass inherits all of the fields of the superclass, can either inherit or override the superclass operations, and can add new fields and operations. Inheritance from an interface is called interface inheritance; inheritance from other classes is called implementation inheritance.

A variable having a given class as its type can reference an object from that class or any of its subclasses, direct or indirect. The variable is said to be polymorphic.

An operation applied to a polymorphic variable is determined either with static binding based on the variable’s type, or with dynamic binding (also known as dispatching) based on the type of the object that is referenced. Language-specific rules dictate whether the binding is static or dynamic.

OOP in Ada 2012. A class corresponds to a tagged type declared in a package. A tagged type may be declared as abstract, modeling an abstract class. An interface corresponds to an interface type (a special kind of tagged type).

Encapsulation is based on where an entity is declared in a package. An encapsulated type is declared as a private type in the visible (public) part of the package; the implementation of the type is specified in the private part.

Inheritance in Ada is obtained through type derivation:

type subclass_type is new superclass_type with extension_part;

Ada supports single implementation inheritance and multiple interface inheritance. A polymorphic variable for a tagged type T is a reference to an object of the class-wide type T’Class, which denotes the set of types in the derivation hierarchy rooted at T.

An operation taking a parameter, or returning a result, of a tagged type T and declared along with T (in the same package) is said to be a primitive operation for T. If (a reference to) an object of a class-wide type is passed as a parameter to a primitive operation of T, or returned as a result, then the operation is bound dynamically, otherwise it is bound statically.

A detailed treatment of how Ada’s OOP features can be used for high-integrity applications, including a discussion of how the OOP vulnerabilities described in DO-332 can be mitigated, appears in [5]. This article focuses on one particular aspect: using Ada 2012’s contract-based programming in connection with OOP.

Contracts in software
A contract in a piece of software is basically a specification of some property that must be satisfied by the program. It doesn’t add any functionality, but instead identifies some constraint. A contract may be explicit in the source code in some syntactically distinguished manner, or implicit in the program logic. An explicit syntax is preferable, since it clearly expresses the program’s intent and can be analyzed by the compiler or static analysis tools, and in the following discussion the term “contract” will be assumed to mean “explicitly specified contract.”

Contracts come in many shapes and sizes, but the main varieties relevant to OOP are preconditions and postconditions for a class’s operations, and type invariants for the class itself. A precondition identifies both a responsibility of the caller (which must ensure that the precondition is met) and a guarantee for the called operation (which can assume that the precondition is satisfied). In Ada 2012 a precondition is realized by a Boolean expression that can reference the operation’s parameters and non-local data.

A postcondition identifies a responsibility of the called operation and a guarantee for the caller. In Ada 2012 it is realized by a Boolean expression that can reference the operation’s parameters and non-local data – both the final values at the point of return and “old” values evaluated at the start of the operation’s execution – and, for a function, a postcondition can also reference the function’s result.

A type invariant for a class is a special kind of postcondition that applies to each public operation (and also serves as an implicit precondition that can be assumed for such operations). In Ada 2012 it is realized by a Boolean expression associated with an encapsulated (private) type.

Figure 1 shows an example of contracts in Ada 2012 for a GCD (Greatest Common Divisor) function, in essence providing a precise documentation of the function’s requirements.

function GCD(N1, N2 : Integer) return Integer
   with Pre  =>
          N1>0 and N2>0,
        Post =>
          N1 rem GCD'Result = 0 and
          N2 rem GCD'Result = 0 and
          (for all I in 1 .. Integer'Min(N1, N2) =>
            (if N1 rem I = 0 and N2 rem I = 0 then GCD'Result >= I));

Figure 1: Example of pre- and postconditions for a function

The precondition expresses the requirement that both parameters are positive. The precondition would have been unnecessary if we had declared the formal parameters N1 and N2 to be of subtype Positive, which is the set of Integer values greater than 0. In effect, a subtype in Ada is a kind of contract that indicates a constrained range of values for a type.

The first two terms in the postcondition reflect that the function result is a common divisor of both parameters, and the third states that it is the largest of all common divisors. This example illustrates quantified expressions (for all I …) and conditional expressions (if … then), both of which are new in Ada 2012.

Figure 2 shows an example of an Ada 2012 postcondition for a procedure that substitutes a replacement Character (By) for each occurrence of a given Character (Char) in a String (S). There is no explicit precondition so by default the precondition is True. The postcondition illustrates the use of the ‘Old attribute for a formal parameter.

procedure Replace(S : in out String; Char, By : Character)
   with Post =>
          (for all I in S'Range =>
            S(I) = (if S'Old(I) = Char then By else S'Old(I)));

Figure 2: Example of postconditions for a procedure

Depending on the language and its support tools, contracts may be checked at run time (with an exception raised on failure), verified statically to ensure consistency with the program logic, or treated as comments to the reader. A typical scenario when contracts are checked at run time – especially when they involve quantified expressions, which may be expensive in execution time – is to enable checks during development and then, after sufficient analysis and testing to provide confidence that the contracts will never fail, to disable the checks in the interest of performance.

The concept of a software contract, including pre- and postconditions, is not new. It was proposed several decades ago in connection with formal proofs of program correctness, and fleshed out with run-time semantics in the Eiffel language [6], which also treated its interaction with OOP. Ada 2012 [7, 8] has advanced the state of the art by allowing both dynamic and static checking of contracts (the latter can be conducted by external proof tools such as for the SPARK 2014 [9] subset of Ada). Ada 2012 also includes direct support for an important OOP precept known as the Liskov Substitution Principle.

Liskov Substitution Principle
At the heart of OOP is the concept of inheritance. By inheriting from a superclass, a subclass can extend its parent with new operations and fields, and either override existing operations to provide specialized behavior or else inherit them unchanged. There is, however, an important consequence: any operation applied to a superclass instance should also be valid for instances of the subclass. This concept is sometimes known as the Liskov Substitution Principle (LSP) [10]. For example, if a general Shape superclass has an Area operation, and Rectangle is a subclass of Shape, then Area should also be a meaningful operation for Rectangle (likely with a more efficient implementation).

LSP means that the inheritance mechanism in OOP should only be used to model the specialization relationship between classes. If inheritance is used for other purposes, then an operation that applies to the superclass may be inapplicable to some instances of the subclass, resulting in two kinds of run-time errors:
  • A dispatching call might satisfy the precondition for the superclass’s operation but violate the precondition of the actual operation that is invoked. The invoked operation will fail.
  • The actual operation invoked by a dispatching call might satisfy the postcondition for the subclass’s version of the operation but fail to comply with the postcondition for the superclass’s version. A caller assuming the superclass postcondition might then make faulty assumptions about the state of the program (values of variables).

The LSP requirements for the contracts associated with a subclass’s version of an operation may therefore be summarized as follows:
  • The precondition for a subclass operation must be the same as, or weaker than, the superclass’s precondition (i.e., the superclass precondition implies the subclass precondition), and
  • The postcondition for a subclass operation must be the same as, or stronger than, the superclass’s postcondition (i.e., the subclass postcondition implies the superclass postcondition).

The requirements for a type invariant are the same as those for a postcondition.

The LSP semantics, especially for preconditions, might seem counterintuitive at first glance. After all, a subclass typically constrains the superclass’s value space, so it might seem natural for a subclass’s version of an operation to demand more, not less, than the superclass’s operation. However, such a scenario would violate LSP. When designing a class hierarchy it is important to anticipate potential extensions and to define a superclass operation’s pre- and postconditions keeping LSP in mind.

To comply with LSP, the precondition for a superclass operation should either be the strongest precondition anticipated for any version of the operation in the class hierarchy, or else an invocation of a dispatching function that performs the check relevant to the corresponding subclass. And to comply with LSP the postcondition for a superclass operation should be the weakest postcondition anticipated for any version of the operation in the class hierarchy.

This may sound contrary to the OOP principle of class extension (i.e., a class author does not know in general how the class will be extended) but if LSP is violated then some operation invocations may fail. Class hierarchy design requires planning, and pre- and postconditions need to be carefully considered. This guidance relates to OOP in general, and Ada 2012 offers specific semantics that can help.

< Previous
Page 1 of 2
Next >

Loading comments...