Kurt Nørmark ©
Department of Computer Science, Aalborg University, Denmark

Abstract Previous lecture Next lecture Index References Contents

This lecture is about program correctness relative to specifications given by assertions. We discuss preconditions, postconditions, and invariants. The use of assertions for specifications of object-oriented program is known as Design by Contract.

A software quality is a positive property of a program There are many different software qualities that may be considered and promoted

Table. Different program qualities listed by name, description, and (for selected qualities) a contrasting, opposite quality

Quality Description Contrast Correct Satisfies expectations, intentions, or requirements Erroneous Robust Can resist unexpected events Fragile Reusable Can be used in several contexts Application specific Simple Avoids complicated solutions Complex Testable Constructed to ease revelation of errors - Understandable Mental manageability Cryptic

Of all software qualities correctness play a particular important role

Correctness Slide Annotated slide Contents Index References Textbook

A correct program - in relation to what?

The programmers own, immediate comprehension Not formulated - not documented - volatile - easily forgotten Sometimes incomplete A program specification Formulated - written Well-considered and agreed upon Formal or informal Part of the program

Specifications Slide Annotated slide Contents Index References Textbook

The concept program specification: A program specification is a definition of what a computer program is expected to do [Wikipedia]. What - not how.

Reference Abstract Datatypes - Specification of

Formal techniques for specification of abstract datatypes Algebraic specifications Equations that define how certain operations work on constructor expressions Axiomatic specifications Logical expressions - assertions - associated with classes and operations Often divided into invariants, preconditions, and postconditions

Program: An algebraic specification of a stack.

Type stack [int] declare constructors new () -> stack; push (int, stack) -> stack; destructors pop (stack) -> stack; selectors top (stack) -> int; isnew (stack) -> bool; for all i in int; s in stack; let pop (new()) = error; pop (push (i,s)) = s; top (new()) = error; top (push (i,s)) = i; isnew (new()) = true; isnew (push(i,s)) = false; end end stack.

Program: An axiomatic specification of the squareroot function.

sqrt(x: Real) -> Real precondition: x >= 0; postcondition: abs(result * result - x) <= 0.000001

The concept logical expression: A logical expression is an expression of type boolean
The concept assertion: An assertion is a logical expression, which, if false, indicates an error [Foldoc]
The concept precondition: A precondition of an operation is an assertion which must be true just before the operation is called
The concept postcondition: A postcondition of an operation is an assertion which must be true just after the operation has been completed

Precondition A precondition states if it makes sense to call an operation The precondition is a prerequisite for the activation

Postcondition A postcondition states if the operation returns the desired result, or has the desired effect, relative to the given parameters that satisfy the precondition The postcondition defines the meaning of the operation

Examples of preconditions and postconditions Slide Annotated slide Contents Index References Textbook

Preconditions and postconditions in a circular list

A circular list. The large yellow object represents the circular list as such. The circular green nodes represent the elements of the list. The rectangular nodes are instances of a class akin to LinkedListNode, which connect the constituents of the list together.

Program: Circular list with preconditions and postconditions.

class CircularList { // Construct an empty circular list public CircularList() require true; ensure Empty(); // Return my number of elements public int Size() require true; ensure size = CountElements() && noChange; // Insert el as a new first element public void InsertFirst(Object el) require !Full(); ensure !Empty() && IsCircular() && IsFirst(el); // Insert el as a new last element public void InsertLast(Object el) require !Full(); ensure !Empty() && IsCircular() && IsLast(el); // Delete my first element public void DeleteFirst() require !Empty(); ensure Empty() || (IsCircular() && IsFirst(old RetrieveSecond())); // Delete my last element public void DeleteLast() require !Empty(); ensure Empty() || (IsCircular() && isLast(old RetrieveButLast())); // Return the first element in the list Object RetrieveFirst() require !Empty(); ensure IsFirst(result) && noChange; // Return the last element in the list Object RetrieveLast() require !Empty(); ensure IsLast(result) && noChange; }

An Assertion Language Slide Annotated slide Contents Index References Textbook

We need an assertion language in which to write preconditions, postconditions, and other assertions We want to check the assertions when the program runs

A possible assertion language Logical expressions - as in the programming language Programmed assertions - via boolean functions of the programming language Should be simple functions Problems if there are errors in these Universal ("for all...") and existential ("there exists...") quantifiers Requires programming - iteration - traversal It may be expensive to check assertions with quantifiers Informal assertions, written in natural language Cannot be checked Much better than nothing Special means of expression old Expr - The value of the expression at the beginning of the operation nochange - A simple way to state that the operation has not changed the state of the object

Is there an even and balanced distribution of responsibility among the objects? Are there objects around that are burdened by unreasonable amounts of responsibility? And presumably hereby also by too much complexity. Are there responsibilities that no object care about? Are the responsibilities that two objects redundantly care about? Due to weak rules about division of responsibilities.

Division of Responsibilities Slide Annotated slide Contents Index References Textbook

A class manages a certain responsibility We wish to avoid that a set of classes escape from responsibilities We also wish to avoid overlapping responsibilities between pair of classes

Reference Responsibility

Division of responsibilities Without well-defined division of responsibilities All classes accept a large responsibility All program parts check all possible conditions (defensive programming) Makes a large program even larger With well-defined division of responsibilities Operations can safely operate under given assumptions It is well-defined which parts should check which conditions Simplifies the program

The highly responsible program Slide Annotated slide Contents Index References Textbook

We illustrate and exaggerate the interaction between a BankAccount and Client An illustration of overlapping responsibilities

Program: Excerpt of highly responsible class Client of BankAccount.

public class Client{ public static void Main(){ BankAccount ba = new BankAccount("Peter"); if (ba.AccountOK && ba.EnoughMoney(1000)) ba.WithDraw(1000); else WithdrawingProblems("..."); if (!ba.AccountOK) MajorProblem("..."); if (ba.Balance <= 0) BankAccountOverdrawn(ba); ... if (ba.AccountOK) ba.Deposit(1500); if (!ba.AccountOK) MajorProblem("..."); } }

Program: Excerpt of highly responsible class BankAccount.

public class BankAccount { private double interestRate; private string owner; private double balance; // ... public void Withdraw (double amount) { if (!AccountOK) ComplainAboutNonValidAccount(); else if (!this.EnoughMoney(amount)) ComplainAboutMissingMoney(); else balance -= amount; } public void Deposit (double amount) { if (amount >= 10000000) CheckIfMoneyHaveBeenStolen(); else if (!AccountOK) ComplainAboutNonValidAccount(); alse balance += amount; } }

Responsibility division by pre and postconditions Slide Annotated slide Contents Index References Textbook

Preconditions and postconditions can be used to divide the responsibility between classes in an object-oriented program

Fulfillment of the precondition The responsibility of the caller The responsibility of the client in an object-oriented program Fulfillment of the postcondition The responsibility of the called operation The responsibility of the server in an object-oriented program

Blame the caller if a precondition of an operation fails Blame the called operation if the postcondition of an operation fails

Contracts Slide Annotated slide Contents Index References Textbook

The preconditions and the postconditions together form a contract between the client class and the server class

The concept contract: A contract expresses the mutual obligations in between parts of a program that cooperate about the solution of some problem

Violating the contract A serious problem An error relative to the specification Should raise an exception Most likely stops the program execution

Everyday Contracts Slide Annotated slide Contents Index References Textbook

Contracts are all around us in our everyday life

Student and University The student enrolls some course The university offers a teacher, a room, supervision and other resources Citizen and Tax office The citizen does a tax return The tax office calculates the taxes, and regulates the paid amount of money Football player and Football club The player promises to play 50 games per season The football club pays 10.000.000 kroner to the player pr. month Citizen and Insurance company The insurance holder pays the insurance and promises to avoid insurance fraud In case of a damage or accident, the insurance company pays compensation

Contracts: Obligations and Benefits Slide Annotated slide Contents Index References Textbook

Figure. A give-and-take situation involving a client and a server (supplier) class.

Obligation - May involve hard work Benefit - A delight. No work involved

Obligations and Benefits in Sqrt Slide Annotated slide Contents Index References Textbook

Program: An axiomatic specification of the squareroot function.

sqrt(x: Real) -> Real precondition: x >= 0; postcondition: abs(result * result - x) <= 0.000001

Table. A tabular presentation of the obligations and benefits of the squareroot function (in a server role) and its callers (in a client role).

- Obligation Benefit Client Must pass a non-negative number Receives the squareroot of the input Server Returns a number r for which r * r = x Take for granted that x is non-negative

Notice in particular the obligation of the client and the benefit of the server

A class invariant expresses some constraints that must be true at every stable point in time during the life of an object

The concept class invariant: A class invariant expresses properties of an object which are stable in between operations initiated via the public client interface

A class invariant acts as a general strengthening of both the precondition and postcondition expresses a "health criterion" of the object must be fulfilled by the constructor must be maintained by the public operations must not necessarily be maintained by private and protected operations

Everyday invariants Slide Annotated slide Contents Index References Textbook

Adherence to invariants is the key to order in our daily lives

Coffee Machine In between operations there is always at least one cup of coffee available Toilet In between "transactions" there is always at least 0.75 meter of toilet paper on the roll Keys and wallet In between using keys and/or wallet During daytime: Keys and wallet are in the pocket During nighttime: Keys are wallet are located on the bedside table or underneath the pillow

An example of a class invariant Slide Annotated slide Contents Index References Textbook

The class invariant of a circular lists expresses that the list is circular whenever it is non-empty

Program: Circular list with a class invariant.

class CircularList { // Construct an empty circular list public CircularList() require true; ensure empty(); // Return my number of elements public int size() require true; ensure (size = countElements) && noChange; // Insert el as a new first element public void insertFirst(Object el) require !full(); ensure !empty() && isFirst(el); // Insert el as a new last element public void insertLast(Object el) require !full(); ensure !empty() && isLast(el); // Delete my first element public void deleteFirst() require !empty(); ensure (empty() || isFirst(old retrieveSecond)); // Delete my last element public void deleteLast() require !empty(); ensure (empty() || isLast(old retrieveButLast())); // Return the first element in the list Object retrieveFirst() require !empty(); ensure isFirst(result) && noChange; // Return the last element in the list Object retrieveLast() require !empty(); ensure isLast(result) && noChange; invariant !empty() implies isCircular() and empty() implies (size() = 0); }

Reference A circular list with pre and postconditions

How do the assertions in a subclass relate to the similar assertions in the superclass?

Figure. The relationship between inheritance and contracts

Subcontracting Slide Annotated slide Contents Index References Textbook

Due to polymorphism an instance of a subclass can act as stand in for an instance of the superclass Consequently, the contracts of the subclass must comply with the contract of the superclass The contract of a subclass must therefore be a subcontract of the superclass' contract

Assertions in a subclass The precondition must not be stronger than the precondition in the superclass The postcondition must not be weaker than the postcondition in the superclass The class invariant must not be weaker than the invariant in the superclass

Operations in subclasses cannot arbitrarily redefine/override operations in superclasses

Class invariants in the triangle class hierarchy Slide Annotated slide Contents Index References Textbook

Figure. Most general triangle: 3 non-zero angles 3 non-zero edges Sum of angles: 180 degrees Isosceles triangle Invariant of general triangle 2 edges of equal length Equilateral triangle: Invariant of isosceles triangle 3 edges of equal length Right triangle: Invariant of general triangle Pythagoras Isosceles right triangle: Invariant of isosceles triangle Invariant of right triangle

Reference Geometric shapes

Assertions in Abstract classes Slide Annotated slide Contents Index References Textbook

It is - in particular - useful to supply assertions in abstract classes

Program: An abstract class with preconditions and postconditions.

using System; public abstract class Stack{ abstract public void Push(Object el); require !full; ensure !empty && top() = el && size() = old size() + 1 && "all elements below el are unaffected"; abstract public void Pop(); require !empty(); ensure !full() && size() = old size() - 1 && "all elements remaining are unaffected"; abstract public Object Top require !empty(); ensure nochange && Top = "the most recently pushed element"; { get; } abstract public bool Full require true; ensure nochange && Full = (size() = capacity); { get; } abstract public bool Empty require true; ensure nochange && Empty = (size() = 0); { get;} abstract public int Size require true; ensure nochange && Size = "number of elements on stack"; { get;} public void ToggleTop() require size() >= 2; { if (Size >= 2){ Object topEl1 = Top; Pop(); Object topEl2 = Top; Pop(); Push(topEl1); Push(topEl2); } ensure size() = old size() && "top and element below top have been exchanged" && "all other elements are unaffected"; } public override String ToString(){ return("Stack"); } }

Reference The abstract class Stack

Design by ContractTM (DBC) represents the idea of designing and specifying programs by means of assertions

Use of contracts in the phases and activities of software development Design: A pragmatic approach to program specification Documentation: Adds very important information to interface documentation of the classes Implementation: Guides and constrains the actual programming Verification: The program can be checked against the specification every time it is executed Test: Preconditions limit the testing work The check of postconditions and class invariants do part of the testing work End use: Trigger exception handling if assertions are violated

DBC and Programming Languages Slide Annotated slide Contents Index References Textbook

Design by Contract is most strongly supported in the programming language Eiffel Betrand Meyer - the creator of Eiffel - has coined and developed the concept of Design By Contract

Design by contract in other languages Several implementations in Java Three implementations in C#-like languages Many others

Reference Wikipedia about Design by Contract and programming languages

Code contract and DBC is now supported in C# 4.0

Code Contracts in C# 4.0 Slide Annotated slide Contents Index References

Code contracts in C# 4.0 is modelled after DBCTM in Eiffel In addition, contract concepts are inspired from MS Spec# Code contracts in C# is an afterthought - in contrast to Eiffel DBC which is a forethought

Code contract characteristics: Conceptually similar to DBC in Eiffel. Supplied via the class library - not the programming language. Relies on static methods in class Contracts. A binary rewritter patches the compiled C# code in order to enable and relocate assertions in the compiled assembly A static contract checker is also supported Based on assertions, the static contract checker attempts to prove program correctness

Invariants are not limited to classes Loop invariants are the primary means to control and reason about loops

Program: Division by repeated subtraction.

using System; class LoopInvariantDemo{ static int Div(int x, int y){ // require x >= 0 && y > 0; int rest = x; int quotient = 0; while (rest >= y) { // invariant rest + quotient * y = x; rest = rest - y; quotient = quotient + 1; } return quotient; // ensure rest + quotient * y = x && rest < y && rest >= 0; } public static void Main(){ Console.WriteLine("Div({0}, {1}) = {2}", 10, 2, Div(10, 2)); Console.WriteLine("Div({0}, {1}) = {2}", 100, 25, Div(100, 25)); Console.WriteLine("Div({0}, {1}) = {2}", 1234567, 89, Div(1234567, 89)); } }

Program: Output of the division program.

Div(10, 2) = 5 Div(100, 25) = 4 Div(1234567, 89) = 13871

Program: Division by repeated subtraction - instrumented with output inside loop.

using System; class LoopInvariantDemo{ static int Div(int x, int y){ // require x >= 0 && y > 0; int rest = x; int quotient = 0; while (rest >= y) { // invariant rest + quotient * y = x; Console.WriteLine("{0,-3} + {1,-3} * {2,-3} = {3,-3}", rest, quotient, y, x); rest = rest - y; quotient = quotient + 1; } Console.WriteLine("{0,-3} + {1,-3} * {2,-3} = {3,-3}", rest, quotient, y, x); return quotient; // ensure rest + quotient * y = x && rest < y && rest >= 0; } public static void Main(){ Console.WriteLine("Div({0}, {1}) = {2}\n", 10, 2, Div(10, 2)); Console.WriteLine("Div({0}, {1}) = {2}\n", 11, 2, Div(11, 2)); Console.WriteLine("Div({0}, {1}) = {2}\n", 100, 25, Div(100, 25)); } }

Program: Output of the instrumented division program.

10 + 0 * 2 = 10 8 + 1 * 2 = 10 6 + 2 * 2 = 10 4 + 3 * 2 = 10 2 + 4 * 2 = 10 0 + 5 * 2 = 10 Div(10, 2) = 5 11 + 0 * 2 = 11 9 + 1 * 2 = 11 7 + 2 * 2 = 11 5 + 3 * 2 = 11 3 + 4 * 2 = 11 1 + 5 * 2 = 11 Div(11, 2) = 5 100 + 0 * 25 = 100 75 + 1 * 25 = 100 50 + 2 * 25 = 100 25 + 3 * 25 = 100 0 + 4 * 25 = 100 Div(100, 25) = 4

Collected references Contents Index

Abstract Datatypes - Specification of Responsibility A circular list with pre and postconditions Geometric shapes The abstract class Stack Wikipedia about Design by Contract and programming languages

Chapter 13: Contracts and Assertions
Course home     Author home     About producing this web     Previous lecture (top)     Next lecture (top)     Previous lecture (bund)     Next lecture (bund)     
Generated: February 7, 2011, 12:22:05