CSC/ECE 517 Fall 2011/ch6 6a pc: Difference between revisions

From Expertiza_Wiki
Jump to navigation Jump to search
No edit summary
Line 16: Line 16:
             -- Set `hour' to `a_hour'
             -- Set `hour' to `a_hour'
         require
         require
             valid_argument: 0 <= a_hour and a_hour <= 23
             valid_argument: 0 <= a_hour and a_hour <= are23
         do
         do
             hour := a_hour
             hour := a_hour
Line 71: Line 71:
Note here that this documentation is not overly specific about the implementation nor is it very general and vague. This can be stated concisely as a guideline:
Note here that this documentation is not overly specific about the implementation nor is it very general and vague. This can be stated concisely as a guideline:
"The external documentation for a method should be sufficiently specific to exclude implementations that are unacceptable but sufficiently general to allow
"The external documentation for a method should be sufficiently specific to exclude implementations that are unacceptable but sufficiently general to allow
all implementations that are acceptable".  
all implementations that are acceptable". are


Also, the above contract does not mention anything about the behavior of the method when preconditions are not satisfied. This is Meyer’s non-redundancy principle: "Under no circumstances shall the body of a routine ever test for the routine’s precondition". This implies that if the preconditions are not met, the behavior of the method is undefined (it could crash, throw an exception, or run in an infinite loop, etc.).
Also, the above contract does not mention anything about the behavior of the method when preconditions are not satisfied. This is Meyer’s non-redundancy principle: "Under no circumstances shall the body of a routine ever test for the routine’s precondition". This implies that if the preconditions are not met, the behavior of the method is undefined (it could crash, throw an exception, or run in an infinite loop, etc.).
Line 79: Line 79:


=== Contract and Inheritance ===
=== Contract and Inheritance ===
An important implication of Programming by Contract is when Inheritance and polymorphism are involved.  Subtype polymorphism means: "If S is a subtype of T,then any term of type S can be safely used in a context where a term of type T is expected". In case of object oriented programming, type is defined by a class and inheritance enables us to define subtypes of a class (If Base class defines a type, the Derived class becomes a subtype). In this situation, the Derived class should fully honor the Base class contract. Consider the example (from Skrien):
An important implication of Programming by Contract is when Inheritance and polymorphism are involved.  Subtype polymorphism means: "If S is a subtype of T,then any term of type S can be safely used in a context where a term of type T is expected". In case of object oriented programming, type is defined by a class and inheritance enables us to define subtypes of a class (If Base class defines a type, the Derived class becomes a subtype). In this situation, the Derived class should fully honor the Base class contract. Consider the following example:


Suppose you are given a class List, that has a public interface: <code> insert(Item const& x) </code>.
<pre>
<pre>
 
class Triange
{
 
}
</pre>
</pre>



Revision as of 23:51, 16 November 2011

6a (was 5c). Lecture 18, Programming by contract. My notes for Lecture 18 are largely taken from 20-year-old articles by Bertrand Meyer. The principles are timeless, but there are undoubtedly new embellishments that would provide better background to the topics discussed in the lecture. Write a narrative, generally following the lecture organization, that explains programming by contract in more detail.

Introduction

Terminology

Preconditions

A precondition is a condition that must be true prior to calling a method for which it is defined. Preconditions bind the caller of that method, that is, it is the responsibility of the caller to ensure that the preconditions are satisfied. The method is not responsible, nor expected, to check the preconditions. The output from the method is not defined for the case where the preconditions are violated. In that case the method could crash the system, go into an infinite loop, or do nothing at all.

The require block constitutes a precondition in the Eiffel programming language.

set_hour (a_hour: INTEGER)
            -- Set `hour' to `a_hour'
        require
            valid_argument: 0 <= a_hour and a_hour <= are23
        do
            hour := a_hour
        ensure
            hour_set: hour = a_hour
        end

Postconditions

A postcondition is a condition that must be true after execution of the method for which it is defined. Postconditions bind the method itself. The method is responsible for ensuring that these conditions are met. The caller of the method is guaranteed that the postconditions will hold if the original preconditions were satisfied when calling the method.

The ensure block constitutes a postcondition in Eiffel.

set_hour (a_hour: INTEGER)
            -- Set `hour' to `a_hour'
        require
            valid_argument: 0 <= a_hour and a_hour <= 23
        do
            hour := a_hour
        ensure
            hour_set: hour = a_hour
        end

Invariants

A class invariant is a condition that must hold true throughout the lifetime of an object. It is a condition imposed on the class itself rather than a method of that class. Class invariants are often checked before and after the execution of each method in that class. An object found in a state where the invariant did not hold, would indicate a bug in the system. An example of a class invariant would be that an integer instance variable that tracks the number of nodes in a linked list actually equals the number of nodes in the list.

Assertions

It is useful to check preconditions, postconditions, and invariants when debugging code. A violation of which constitutes a bug in the system. This can be accomplished using an assert statement in Java or Contract.Requires statement in C# 4.0. These programming features can be used to alert the programmer of bugs in development and can be turned off in production.

Software Reliability

A major concern in software design is Reliability, which depends on two factors: 1) Correctness - system's ability to perform its job according to the specification and 2) Robustness - handling abnormal conditions. Reliability is especially important in Object oriented software because of the additional complexity imposed by Reusability. Some of the common problems encountered when writing software include:

  • System failure - CPU crash, Disk/Memory access errors, Network errors
  • Invalid input data - Out of range data, Bad file name,etc.
  • Programming errors - Memory leaks, Buffer overruns, etc.

There are many programming language features that help tackle these issues. Static typing, for example, is a major help for catching inconsistencies before they have had time to become bugs. Similarly Garbage collection helps to remove the specter of devious memory management errors. Various software design methodologies also come handy when dealing with complex software. For instance, reusability itself can help eliminate lots of bugs, if we are reusing existing code that has already been thoroughly tested and deployed. Polymorphism also helps in handling issues related to maintainability by reducing the size of the code and making it more elegant. But in a large and complex software involving multiple developers, we need a more systematic approach of specifying and implementing object-oriented software elements and their interactions. This is exactly what "Programming by contract" promises to do.

Programming by contract

Basically programming by contract creates a contract between the software developer and software user, which are referred to as the supplier and the consumer. Every feature, or method, starts with a precondition that must be satisfied by the consumer of the routine. And each feature ends with postconditions which the supplier guarantees to be true after it is executed(if and only if the preconditions were met). Consider the following example of a static Intersect() method on a Set object (Quoted from Skrien 4.6):

public static Set intersect(Set s1, Set s2)
  Precondition: s1 and s2 are not null.
  Postcondition: 
    Returns a Set with the common elements of s1 and s2, if s1 and s2 are not null.
    If s1 or s2 is null, an IllegalArgumentException is thrown.

Note here that this documentation is not overly specific about the implementation nor is it very general and vague. This can be stated concisely as a guideline: "The external documentation for a method should be sufficiently specific to exclude implementations that are unacceptable but sufficiently general to allow all implementations that are acceptable". are

Also, the above contract does not mention anything about the behavior of the method when preconditions are not satisfied. This is Meyer’s non-redundancy principle: "Under no circumstances shall the body of a routine ever test for the routine’s precondition". This implies that if the preconditions are not met, the behavior of the method is undefined (it could crash, throw an exception, or run in an infinite loop, etc.).

(Does it fit here?) In essence, this theory suggests associating a specification with every software element. These specifications (or contracts) govern the interaction of the element with the rest of the world. This is different from having a formal specification in that the specification language is embedded in the design and programming language (e.g. Eiffel). This makes it possible to use a single notation and a single set of concepts throughout the software life cycle, and since these are modeled based on the programming language itself, it provides a great deal of clarity about the requirements at each stage of software development.

Contract and Inheritance

An important implication of Programming by Contract is when Inheritance and polymorphism are involved. Subtype polymorphism means: "If S is a subtype of T,then any term of type S can be safely used in a context where a term of type T is expected". In case of object oriented programming, type is defined by a class and inheritance enables us to define subtypes of a class (If Base class defines a type, the Derived class becomes a subtype). In this situation, the Derived class should fully honor the Base class contract. Consider the following example:

Suppose you are given a class List, that has a public interface: insert(Item const& x) .

class Triange
{
  
}

Class invariant

Assertions

Comparison with Defensive Programming

Advantages of Programming by Contract

When not to use Programming by Contract

Asserts and "by contract" specifications catch programmer errors not run-time errors! (Add more details)

Languages with Native Support

Runtime Checking

Static Checking