David Crocker's Verification Blog

When RTCA released DO-178C – the long-awaited update to the DO-178B standard for airborne software – they added a number of supplements to cover specific software development techniques. One of those techniques is object-oriented software development, covered by supplement DO-332. This supplement mentions the Liskov Substitution principle (hereafter abbreviated LSP) in FAQ #14 “Why is the Liskov Substitution Principle (LSP) important?” and gives more detail in FAQ #15 and #16. So, what is the LSP, and how can we make sure that a software design adheres to it?

What is the LSP?

In the context of object-oriented software, the LSP states the conditions under which an object of a derived class may substitute for an object of one of its base classes. In other words, if the LSP is satisfied between a derived class D and its base class B, then we can say that an instance of D is-a B.

Let’s look at that in a C++ context. Suppose we have a base class B, and we declare pointers of type B* or references of type B&. Then we call some virtual member function f of B using the syntax p->f(…) or r.f(…). If p or r actually points or refers to an object of a derived class D, and that class contains its own definition of f that overrides the one in class B, then the behaviour of f in D must be compatible with the behaviour of f in B.

The LSP doesn’t only apply to object-oriented design. It applies whenever one function substitutes for another – for example when function pointers are used in C and C++. I covered this in a previous entry in this blog – see http://eschertech.com/articles/items/art110908.html for an archived copy.

An example to illustrate the LSP

Suppose we want to develop a system that displays multiple aviation instruments on LCD screens. We would like to make the system easy to extend and to be able to customize which instruments are displayed. So an object-oriented design seems natural.

We start by declaring an abstract class AircraftInstrument. From this, we derive classes AirspeedTape, Altimeter, and so on. The code to manage the display layout and populate the displays uses variables of type AircraftInstrument* so that it does not need to know the details of the individual instruments. It calls the place and draw methods of the individual instruments to draw them on the screens. Here’s the outline:

// Class to represent the screen that we display instruments on
class Display;

// Type to represent a row or column pixel number on the screen
typedef uint16_t PixelNumber;

// Base class for all aircraft instruments
class AircraftInstrument {
public:
  virtual PixelNumber width() const;  // returns the width needed in pixels
  virtual PixelNumber height() const; // returns the height needed in pixels
  Display* currentDisplay() const;    // get the display for this instrument

  // Assign this instrument to the specified position on the specified display
  virtual void place(Display* screen, PixelNumber x, PixelNumber y);

  // Draw this instrument on the display
  virtual void draw() const;
};

// Individual types of aircraft instrument
class Altimeter : public AircraftInstrument { 
… 
};

// Class used to manage the display of instruments on the screen
class DisplayManager {
private:
  AircraftInstrument* instruments[maxInstruments];
public:
  void drawAll();
};

Let’s suppose we have implemented all of this, and it is working. Now we wish to add a new type of instrument:

class HSI : public AircraftInstrument {
…
};

Will the existing DisplayManager class be able to handle an HSI? The answer is:

If DisplayManager is correctly written such that it requires only that instruments conform to the behaviour specified for the members of AircraftInstrument, and class HSI obeys the LSP with respect to class AircraftInstrument, then an HSI can be substituted for an AircraftInstrument and the DisplayManager will work properly with it.

So if we want to very the LSP, we need to describe how functions behave.

Describing how functions behave

For the purposes of verifying the LSP, we can sum up the behaviour of a function by describing three things:

• What conditions does the function assume are true? In other words, what conditions must be satisfied by the caller, in order that the function can be guaranteed to work correctly? These conditions are called preconditions.
• What variables does (or may) the function write to? In C++ this includes any global variables that the function may write, and variables addressed by any non-const pointers or references that are passed as parameters.
• What conditions does the function guarantee are satisfied when it returns? In other words, what conditions can the caller assume about the state of the system when the function returns? These are called postconditions.

In the next part of this series, I will show how these aspects of function behaviour can be described, first informally, and then formally in Escher C++ Verifier so that compliance with the LSP can be verified.