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

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

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.Ada 2012 support for LSP
Ada 2012 directly supports LSP byallowing the definition of inheritable (‘class-wide’, in Ada parlance)pre- and postconditions – Pre’Class and Post’Class, respectively – thatcan only weaken preconditions and/or strengthen postconditions. If anoverriding operation specifies an explicit Pre’Class contract, then thisnew precondition is implicitly “or”ed with the inherited Pre’Class,thus weakening it. Analogously, if an overriding operation specifies anexplicit Post’Class contract, then this postcondition is implicitly“and”ed with the inherited Post’Class, thus strengthening it. If thereis no explicitly specified or inherited precondition, then the defaultvalue is True, and likewise for postconditions. An analogous facility isprovided for class-wide type invariants, with the same behavior asclass-wide postconditions.

An example of class-wide contracts is shown in Figure 3 , based on a suggestion by R. Duff in [11].

package Accounts is
   type Money is …;
   type Account is abstract tagged private
      with Type_Invariant'Class => Account.Balance >= 0.0;
   function Balance(A : Account) return Money;
   procedure Deposit(A : in out Account; M : in Money)
      with Pre'Class  => M >= 0.0,
           Post'Class => A.Balance >= A.Balance'Old;
   procedure Withdraw(A : in out Account; M : in Money) is abstract
      with Pre'Class  => M in 0.0 .. A.Balance,
           Post'Class => A.Balance <= A.Balance'Old;
private
   …
end Accounts;
package Accounts.Overdraft_Protected is
   type OP_Account is new Account with private
     with Type_Invariant'Class =>
       (if    OP_Account.Balance > 0.0 then OP_Account.Overdraft = 0.0
        elsif OP_Account.Balance = 0.0 then
              OP_Account.Overdraft in 0.0 .. OP_Account.Overdraft_Limit);
   overriding
   procedure Deposit(A : in out OP_Account; M : in Money);

   procedure Set_Overdraft_Limit(A : in out OP_Account; M : in Money)
      with Pre'Class => M >= 0.0,
           Post'Class => A.Overdraft_Limit = M;
   function Overdraft_Limit(A : OP_Account) return Money
      with Post'Class => Overdraft_Limit'Result >= 0.0;
   function Overdraft(A : OP_Account) return Money
      with Post'Class => Overdraft'Result in 0.0 .. A.Overdraft_Limit;
   overriding
   procedure Withdraw(A : in out OP_Account; M : in Money)
      with  Pre'Class => M in 0.0 .. A.Balance + A.Overdraft_Limit-A.Overdraft,
            Post'Class =>
             (if A'Old.Balance > 0.0 and M <= A'Old.Balance  then
                (A.Balance = A'Old.Balance – M and A.Overdraft = 0.0)
              elsif A'Old.Balance > 0.0 and M > A'Old.Balance then
                (A.Balance = 0.0  and  A.Overdraft = M – A'Old.Balance)
              else — A'Old.Balance = 0.0
                (A.Balance = 0.0 and A.Overdraft = A'Old.Overdraft + M));
private
   …
end Accounts.Overdraft_Protected

Figure 3: Example of class-wide contracts in Ada 2012

Inthis example the type OP_Account models an account with overdraftprotection. The Withdraw procedure for Account is overridden inOP_Account, with new pre- and postconditions. The precondition forOP_Account is weaker than for Account, since the withdrawal amount canexceed the balance. The postcondition is stronger, since it can moreprecisely specify the balance. Likewise the type invariant forOP_Account is stronger than for Account. The Deposit procedure isoverridden, since it needs to handle situations when the OP_Account ison overdraft mode, and a new postcondition should be supplied analogousto what was done for Withdraw. It was omitted here in the interest ofsimplicity.

An important semantic point in Ada 2012 concerns theprecondition check at a dispatching call. The class-wide preconditionthat is checked is the one that applies to the superclass operation,even if the actual operation invoked has a weaker version. This followsfrom LSP, and is needed for correct behavior in the presence of multipleinterface inheritance. The call should work for any subclass, and sincepreconditions are only weakened and not strengthened by subclasses, theonly way to ensure substitutability is to check that the superclassprecondition is satisfied. The situation for class-wide postconditionsis simpler, since these can only be strengthened by subclasses and notweakened. That is, if the subclass postcondition is satisfied then thesuperclass postcondition will automatically be satisfied.

Withthese semantics Ada 2012 directly supports LSP. However, it would havebeen overly constraining to require adherence to LSP, and thus thelanguage permits LSP violations. If the precondition for an overridingoperation needs to violate LSP, then a specific (versus class-wide)precondition – Pre rather than Pre’Class – should be specified. This isnot inherited, and it will be checked in addition to any class-widepreconditions. Analogously, if a postcondition has to be weakened by anoverriding operation, then specific (Post) rather than class-wide(Post’Class) postconditions should be used.

If LSP is violatedthen a dispatching call might fail in two ways: a stronger preconditionfor the subclass’s version of the operation, or a weaker postcondition.The programmer has several ways to deal with such situations. One optionis to perform data flow and control flow analysis, manually or throughan automated tool, to ensure statically that the violation will notoccur. Alternatively, one or both of the following approaches can betaken, depending on the nature of the potential violation:

  • If a precondition is strengthened then program defensively by making a dispatching call on a precondition check function before invoking the operation, or anticipate a precondition check failure and handle the resulting exception.
  • If a postcondition is weakened then be aware that a return from a dispatching call might not satisfy the specific postcondition for the superclass operation, and program accordingly.

Ada 2012’s contract-basedfeatures can help the developer meet a number of objectives in DO-178Cand DO-332. Pre-conditions, postconditions, and type invariants are,effectively, low-level requirements expressed directly in the sourcetext. Their explicit syntax makes it easier to develop both compliancetests and robustness tests and to demonstrate traceability torequirements, all of which are required by DO-178C. Further, Ada 2012’ssupport for LSP directly supports an important new objective in DO-332,“Local Type Consistency Verification”. This objective (OO 6.7.1) states:“Verify that all type substitutions are safe by testing or formalanalysis.” One of the activities (OO 6.7.2) contributing to thisobjective is to formally verify substitutability; i.e., in a dispatchingcall p.op(…) where p can reference an object from some classes C1, …,Cn in the class hierarchy rooted at p’s type, show that this call willsucceed regardless of which of these classes is referenced. If the classhierarchy uses class-wide contracts (explicit or inherited) to expressall pre- and postconditions, then formal analysis is facilitated sincethere will not be any cases where a preconditioned is strengthened or apostcondition weakened.

Conclusions
OOP offerssignificant potential for high-integrity systems, since it can be usedto deal with the growing complexity of modern software. The issue is howto realize its benefits without introducing its accompanyingvulnerabilities. Ada 2012 helps to meet this goal, in major part due tothe language’s comprehensive support for contract-based programmingintegrated into its OOP facility. As one of its most significantenhancements, Ada 2012 makes it easy to write contracts that comply withthe Liskov Substitution Principle for class inheritance and thusencourages robust design. In short, Ada 2012’s contract-based OOPapproach combines the full expressiveness of the object-orientedmethodology with the safety and security that have been the Adalanguage’s underpinnings since it was first designed.

Dr. Benjamin Brosgol is a senior member of the technical staff of AdaCore (www.adacore.com).He has been involved with programming language design andimplementation for more than 30 years, concentrating on languages andtechnologies for high-integrity systems. Dr. Brosgol was a member of thedesign team for Ada 95, and he has also served in the Expert Groups forseveral Java Specification Requests. He has presented papers andtutorials on safety and security certification on numerous occasionsincluding ESC (Embedded Systems Conference), ICSE (IEEE/ACMInternational Conference on Software Engineering), SSTC (Systems &Software Technology Conference), ACM SIGAda, and Ada-Europe. Dr. Brosgolholds a BA in Mathematics from Amherst College, and MS and PhD degreesin Applied Mathematics from Harvard University

References

1. FAA. Handbook for Object-Oriented Technology in Aviation (OOTiA), October 2004.

2. RTCA/EUROCAE DO-178B/ED-12B. “Software Considerations in Airborne Systems and Equipment Certification”, December 1992.

3. RTCA/EUROCAE DO-178C/ED-12C. “Software Considerations in Airborne Systems and Equipment Certification”, December 2011.

4.RTCA/EUROCAE DO-332/ED-217. “Object-Oriented Technology and RelatedTechniques Supplement to DO-178C and DO-278A”, December 2011.

5. AdaCore. High-Integrity Object-Oriented Programming in Ada ; June 2013.

6. B. Meyer. “Object-Oriented Software Construction” (Second Edition), Prentice Hall; 1997.

7. ISO/IEC 8652:2012(E); Ada Reference Manual: Language and Standard Libraries

8. J.G.P. Barnes, Programming in Ada 2012 ; Cambridge University Press; 2014.

9. SPARK 2014

10. B. Liskov and J. Wing. “A behavioral notion of subtyping”, ACM Transactions on Programming Languages and Systems (TOPLAS), Vol. 16, Issue 6 (November 1994), pp 1811-1841

11. ISO/IEC JTC1/WG9 Ada Rapporteur Group, Ada Issue ai05-0247-1, Preconditions, Postconditions, multiple inheritance, and dispatching calls

Leave a Reply

This site uses Akismet to reduce spam. Learn how your comment data is processed.