Software Verification: Design by Contract Principles

Overview of Design by Contract (DbC)

• Design by Contract is a software engineering methodology popularized and advocated by Bertrand Meyer.
• The concept is fundamentally connected with Object-Oriented (OO) design.
• Originally, DbC was implemented in the Eiffel programming language, but it has since manifested in other languages including $C++$, Java, and C#.
• DbC remains an active area of research.
• "Design by Contract" is a trademark; the generic name for this approach is Programming by Contract.

The Roles of the Supplier and the Client

Every class has two distinct roles associated with it:

• The Supplier:
  • Responsible for writing the class code.
  • Documents and maintains the class.
  • Possesses internal knowledge of the class implementation.
  • Publishes the class interface for others to use.
• The Client:
  • Uses the class within their own code.
  • Presumably reads the documentation provided by the supplier.
  • Knows about the class interface.
  • Has zero knowledge regarding the internal implementation details of the class.

Pitfalls of Conventional Software Development

Without using Design by Contract, several issues often arise:

• The client may not understand the specific situations or contexts in which a method can be safely used.
• The client may not fully grasp the consequences or side effects of executing a method.
• When a supplier changes an implementation, they lack a formal mechanism to ensure the interface is preserved (the "big rule" is to never break existing client code).
• If the interface must change, the supplier lacks a framework to ensure consistency across the software system.

Main Principles of Design by Contract

• Every public method is defined by a precondition and a postcondition.
• Precondition: Expresses the specific constraints or state under which a method will function properly.
• Postcondition: Expresses what the state of the system will be after the method executes successfully.
• Both preconditions and postconditions are boolean-valued expressions, meaning they must evaluate to either $\text{true}$ or $\text{false}$.

The Formal Contract

Defining these conditions establishes a formal contract between the supplier and the client:

• IF the client runs the method in a situation that satisfies the precondition,
• THEN the supplier guarantees that the method execution will always result in a state that satisfies the postcondition.

Obligations and Benefits Matrix

Precondition Guidelines for Suppliers

• Non-redundancy Principle: The body of a method shall not check to see if the precondition is $\text{true}$.
• DbC is the opposite of "defensive programming."
• By following this principle, developers reduce the overhead and complexity associated with redundant checks.
• If a client has already checked a precondition for another purpose, checking it again inside the method is unnecessary.

Precondition Availability Rule

• Every feature appearing in the precondition of a routine must be available to every client to which the routine is available.
• This is a necessary demand because the client is responsible for establishing the precondition before a call; if the precondition referred to private attributes, the client would have no way to verify it.
• Compilers can typically check if this rule holds.
• Conversely, postconditions may refer to private attributes, as the client is not responsible for establishing them.

Violating Assertions and Debugging

• If an assertion (precondition or postcondition) is not satisfied during runtime, an assertion violation occurs.
• An assertion violation indicates a bug in the code.
• When violated, an exception should be thrown to inform the user which assertion was violated (location) and how it was violated.
• Precondition Violation: Indicates the bug resides in the client’s code.
• Postcondition Violation: Indicates the bug resides in the supplier’s code.

Misconceptions Regarding Assertions

• Assertions are not input checking mechanisms: They are software-to-software contracts, not software-to-user or software-to-device checks. Erroneous input from external users or devices must be handled via standard input-handling code.
• Assertions are not control structures: A bug-free program should never throw an assertion. Code should not attempt to catch an assertion exception to "fix" a situation; they are markers of logic errors, not flow control.

Case Study: Stack Class in UML

Consider a Stack class where elements are of type ELEMENT:

• Attributes:
  • contents: Sequence(ELEMENT)
  • capacity: Integer
• Methods:
  • Stack(n:Integer) (Constructor)
  • pop(): ELEMENT
  • size(): Integer
  • isEmpty(): Boolean
  • isFull(): Boolean
  • push(x:ELEMENT): Void
  • top(): ELEMENT

Class Invariants

• A class invariant is an assertion involving the instance variables of a class.
• All objects must satisfy the invariant at all "stable times."
• Stable Times include:
  1. After the execution of any constructor.
  2. Before the execution of every public method.
  3. After the execution of every public method.
• Corollaries:
  • Private methods are permitted to violate the invariant temporarily during their execution.
  • It is the supplier’s responsibility to ensure constructors and public methods maintain the invariant.

Consequences of Class Invariants

• If no constructor is defined, the default constructor or initialization code must establish the invariant.
• The class invariant is conceptually joined via an "AND" operation with both the precondition and the postcondition of every public method.
• For the Supplier:
  • Benefit: They can assume the invariant holds at the start of the method.
  • Obligation: They must ensure the invariant holds at the end of the method.

Design by Contract and Inheritance

• If class $A$ is a superclass of $B$, then $B$ inherits all non-private methods and variables from $A$.
• $B$ can extend the class with new features or override existing method implementations.
• According to the Liskov Substitution Principle, if a program is expecting an $A$-object, a $B$-object must be able to behave exactly like an $A$-object at runtime.

Method Logic in Inheritance

When class $A$ is a superclass of $B$:

• Preconditions:
  • The client only knows about the preconditions of the superclass ($A$).
  • Therefore, methods in subclass $B$ cannot demand more than methods in $A$.
  • Preconditions in $B$ may be weakened (demand less).
  • Logic: The precondition of the method in $A$ must imply the precondition of the overridden version in $B$ ($\text{Pre}_A \rightarrow \text{Pre}_B$).
• Postconditions:
  • The supplier must ensure that $B$ establishes at least what $A$ promised.
  • Methods in $B$ may establish more (strengthened postconditions).
  • Logic: The postcondition of the method in $B$ must imply the postcondition of the method in $A$ ($\text{Post}_B \rightarrow \text{Post}_A$).

Class Invariants in Inheritance

• Class $B$ inherits all non-private invariants from superclass $A$.
• $B$ can add new invariants regarding inherited variables or its own unique variables.
• Logic: The invariants of subclass $B$ must imply the invariants of superclass $A$ ($\text{Inv}_B \rightarrow \text{Inv}_A$).

Summary of Inheritance Rules

When writing a subclass $B$ that inherits from $A$, the developer can:

• Strengthen the class invariant.
• Weaken the precondition of overridden methods.
• Strengthen the postcondition of overridden methods.
• The opposite actions (weakening invariants/postconditions or strengthening preconditions) are prohibited.

Reference Materials

• Book: Object-Oriented Software Construction (Second Edition) by Bertrand Meyer, Prentice-Hall, $1997$. Specifically Chapter $11$: "Design by Contract: building reliable software."
• Video: Design by Contract(TM) - Built in mechanism for bug prevention, available at the Eiffel website.