CSC/ECE 517 Fall 2009/wiki3 15 SJ3

Programming by Assertion

Introduction to Assertions

Assertions is statement used in code that indicates what a programmer assumes to be true at that point during execution. They are used to help clarify program constraints and assumptions and ensure program correctness. In general they can be thought of as way of testing. Unlike test cases which apply external stimuli to objects and validate their state, assertions checks are used to check assumptions and constraints internally.

Here is a basic assertion statement.

assert(expression);

The way the assertion statement behaves is based on the expression. If the expression evaluates to true execution proceeds past the statement without notice. If the expression evaluates false and exception is thrown causing the program to abort or execute an exception handler. Typically if program is aborted the expression and line number are displayed to standard error as well.

Design by Contract

Assertions are used in a facility called Design by Contract. Contracts are a breakthrough technique to reduce the programming effort for large projects. Contracts are the concept of preconditions, postconditions, invariants, and general errors. These specifications of "contract" define the interface of different element of software includes method, class, module, etc.

Design by Contract Benefits

• A better understanding of the object-oriented method and, more generally, of software construction.
• A systematic approach to building bug-free object-oriented systems.
• An effective framework for debugging, testing and, more generally, quality assurance.
• A method for documenting software components.
• Better understanding and control of the inheritance mechanism.
• A technique for dealing with abnormal cases, leading to a safe and effective language construct for exception handling.

Precondition and Postcondition contract

The pre contracts specify the preconditions before a statement is executed. The most typical use of this would be in validating the parameters to a function. The post contracts validate the result of the statement. The most typical use of this would be in validating the return value of a function and of any side effects it has. The syntax is:

long square_root(long x)
in
{
    assert(x >= 0);
}
out (result)
{
    assert((result * result) <= x && (result+1) * (result+1) >= x);
}
body
{
    return cast(long)std.math.sqrt(cast(real)x);
}

Invariant contract

Here is simple example of invariant condition. Physically a size of a container should be 0 or positive.

assert(size >= 0)

In, Out and Inheritance

If a function in a derived class overrides a function in its super class, then only one of the in contracts of the function and its base functions must be satisfied. Overriding functions then becomes a process of loosening the in contracts.

for detail information of contract, please refers to the helpful reading list in [2].

References

[1] wiki page of "Design by Contract", http://en.wikipedia.org/wiki/Design_by_contract [2] reading list of contract, http://www.eecs.northwestern.edu/~robby/contract-reading-list/