CSC/ECE 517 Fall 2011/ch6 6a am

Introduction

Programming by contract was a paradigm that was initially introduced with the Eiffel programming language by Bertrand Meyer. It was developed to form a system of obligations and benefits between two parties. This system can be used to formulate and describe method calls and passing objects between to separate parties. When designing these methods there are three primary things to consider:

• What does it expect?
• What does it guarantee?
• What does it maintain?
  

Each method being called has a precondition or set of preconditions that must be met by the client. Each method also ends with a set of postconditions which the supplier guarantees to be true (if and only if the preconditions were met). Also, each class has an invariant, a set of properties that remain uncompromised, which must be satisfied after any changes to the an object are made. This insures that the object being operated on is always in a valid state.
There are several advantages to designing software in this manner. The client obligation of meeting all preconditions by providing a certain product is a benefit for the supplier. It allows the supplier to handle only cases that fall within the precondition's restraints. The postcondition provides a benefit for the client by guaranteeing a certain product is returned by the supplier (their obligation).

Writing robust code

Using the programming by contract paradigm has the secondary benefit of increasing the robustness of our code. Out assertions and "contract" specifications allow us to catch programmer errors by catching invalid or unknown state problems. Programming by contract forces you to think about the specification and thus the method will be more likely to comply with its specification. Adding these kinds of checks tends to reduce the propogation of errors. <ref>http://www.cs.usfca.edu/~parrt/course/601/lectures/programming.by.contract.html</ref>

Readability

“Programs must be written for people to read, and only incidentally for machines to execute.”—Abelson & Sussman

In order to make code readable, we must first determine what readable code looks like. How many comment should one leave? How long or short should I make my variable names? Should I use CamelCase or underscores? These are just a few questions novice and experienced programmers are forced to answer. Experienced programmers rely on coding conventions and guidelines to help them code and refactor.

One example of unreadable code is below:

   if (b == true)
       return true;
   else
       return false;

This code is much too complicated to do such a simple job. It can simply be replaced with:

   return b;

Another example would be allow code to become too nested. It causes the reader to lose track of which block they are currently in make code too difficult to follow.

   if (something happens {
       doStuff...
       if (something else) {
           doStuff...
           if (something else) {
               doStuff...
           }
       }
   }

Make changes to your code to reduce the level of nesting. Some languages, such as Java, have their own set of codding conventions. Othera have developed their own set of guidlines to follow.

Assertions

Assertions are used to help specify a programs correctness. It is only correct if it does what it is suppose to do. We can know what a program is suppose to do by defining assertions. In Eiffel, assertions form part of the design process. It integrates these assertions into the language and automatically extracts them to help with class documentation. Assertions can describe the state the code expects to be in before a routine is called, and after. They can also help us to determine class invariants.<ref>http://courses.ncsu.edu/csc517//common/lectures/notes/lec18.pdf</ref>

Pre-Conditions

As stated earlier, the precondition is a predicate that must always be true, or satisfied, prior to method execution. This is the routine callers part of the contract. If the precondition is not satisfied, the client can no longer guarantee the validity of what is returned, if anything can be returned at all.
The following example written in Eiffel, demonstrates proper use of preconditions. The value being passed to the routine, a_hour, must be a valid value for an hour of the day, 0-23. The precondition itself comes after the require keyword.

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

<ref>http://en.wikipedia.org/wiki/Precondition</ref>

Post-Conditions

Like the precondition, the post condition is a predicate that must be satisfied after the execution of some method or routine. The postcondition is a statement of all guaranteed properties of a system after the routine as completed. The duty of satisfying the post condition falls to the supplier. Whereas the client or caller of the routine is offered assurance that the routine is called in a state where the postcondition must hold, assuming the precondition was valid. According to Meyer, "Under no circumstances shall the body of a routine ever test for the routine’s precondition".
The following example written in Eiffel, demonstrates proper use of postconditions. The value being passed to the routine, a_hour, must be a valid value for an hour of the day, 0-23. The postcondition itself comes after the ensure keyword. In the example, if the precondition is satisfied with a proper integer, the hour will get set to the value being passed in.

   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

Another short example in java shows a push method for a stack. Here our conditions are located in comments.

   public void push(Object o)
       // require top<(n-1);
       // ensure top==o;
       // ensure top = old top + 1;
   {
       top++;
       data[top] = o;
   }

<ref>http://en.wikipedia.org/wiki/Postcondition</ref>

Class Invariants

A class invariant is a predicate that must be true at all points during a program. This is should hold no matter what a method does in the class.

Consider a stack. In a stack, the size should always be greater than 0 and less than the capacity. This should always hold. This property of a stack can neither be represented by a pre-condition nor by a post-condition. Such properties of a class are called as Class invariants.

The useful effect of class invariants in object-oriented software is enhanced in the presence of inheritance. Class invariants are inherited, that is, "the invariants of all the parents of a class apply to the class itself."<ref> Meyer, Bertrand. Object-Oriented Software Construction, second edition, Prentice Hall, 1997, p. 570</ref>

Programming By Contract

Programming by Contract is known under the name of Design by Contract™ first implemented by Eiffel, a programming language introduced by Bertrand Meyer.It provides the programmers a way to verify that the execution of their methods does not corrupt the state of the data structures.

Definition

According to Bertrand Meyer,

By associating pre- and postcondition assertions with a method m,the class tells its clients1 “If you promise to call m with pre satisfied then I, in return, promise to deliver a final state in which post is satisfied"<ref> Meyer, Bertrand. Object-Oriented Software Construction, second edition, Prentice Hall, 1997, p. 570</ref>

In other words, "Basically programming by contract creates a contract between the software developer and software user - in Meyer's terms 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 (if and only if the preconditions were met). Also, each class has an invariant which must be satisfied after any changes to the object represented by the class. In the other words, the invariant guarantees the object is in a valid state."<ref>http://www.cs.unc.edu/~stotts/COMP204/contract.html</ref>

Obligations and benefits

There are two main elements in Software System- User and Programmer. In order to understand Obligations and benefits correctly, let us first consider a metaphor and later apply that to Software. The metaphor comes from business life, where a "client" and a "supplier" agree on a "contract" which documents that:

* The supplier must provide a certain product (obligation) and is entitled to expect that the client has paid its fee (benefit).

* The client must pay the fee (obligation) and is entitled to get the product (benefit).

* Both parties must satisfy certain obligations, such as laws and regulations, applying to all contracts.<ref>http://www.eiffel.com/developers/design_by_contract.html</ref>

The metaphor relates to a Software System as below:

* The Programmer must provide the user with a valid outcome(obligation) and can expect that the User has given a correct and valid input(benefit).

* The User must provide a valid input(obligation) to a method and can expect the Programmer to give the correct output(benefit).

* Some properties such as stack size discussed earlier are satisfied by the system at all points of time.

Thus, it is not the responsibility of the Programmer to satisfy the pre-condition. In fact, if the pre-condition is not satisfied by the user, the programmer need not have to do anything. Once the pre-condition is failed, it is not the Programmers' fault even if the system crashes or gives blunders as results.

In order to gain an insight about how programming By Contract actually works, consider the webAssign example from our class:

All the students are supposed to give the tests through WebAssign. During the test process, each student is expected to write their answers in the designated text boxes and save the test no more than 4 times. This is as an obligation for the student. The student in turn is ensured that all his answers are correctly recorded and rendered to the professor for evaluation. This is a benefit for the student.

WebAssign is supposed to record the answers given by the student appropriately and render them to the professor for evaluation. This is an obligation for WebAssign. WebAssign is entitled to ensure that the user has answered in the designated text boxes and saved no more than 4 times. This is a benefit to WebAssign.

Programming 'By Contract' in JAVA

In JAVA, although the exact Programming by contract facility is not provided, it provides an informal "similar" kind of functionality through Programming By Assertions.

Assertions in Java

"An assertion is a statement in the Java programming language that enables you to test your assumptions about your program."<ref>http://download.oracle.com/javase/1.4.2/docs/guide/lang/assert.html</ref>

Each assertion contains a boolean expression which we believe should be true. If the boolean expression does not return true, the program throws an error and the further execution of the code is terminated.

There are two forms of assertions in Java:

1. assert Expression; Here, assert is a keyword and Expression is a Boolean expression. If the expression returns true, the method execution is continued. If the expression returns false, then an AssertionError with no much detail is thrown and the method execution is terminated.

2. assert Expression1 :Expression2; Here, we use assert statement to provide a detail message for the AssertionError. The system passes the value of Expression2 to the appropriate AssertionError constructor, which uses the string representation of the value as the error's detail message.

e.g.

assert !true : "assert is not true";

The output will be:

Exception in thread "main" java.lang.AssertionError:assert is not true

Example

Consider the following requirement:

The job is to pour water in a glass. The method has to pour water in the glass assuming that glass is not full. This is a precondition and can be checked using a assert statement. After the method is called, the amount of water in the class should be greater than before. This is a postcondition and can be checked by a asseret statement. At all times, the water level should be maximum if the glass is full and should be less than maximum if the glass is not full. This is Class Invariant and is checked through a method.

public class WaterGlass{
	boolean isFull;
	int water_level;
	final int max_level= 10;
	WaterGlass()
	{
		isFull = false;
		water_level = 0;
	}
	// this is the class invariant. This always returns true
	public boolean invariant()
	{
		
		return ( (this.isFull == true && water_level==max_level)|| ( this.isFull == false && water_level<max_level));
				 
	}
	//this is the method pourWater
	public void pourWater()
	{
			// Pre Condition. we check that the glass is not full before going into the method.
			// If the glass is full, we print the message and stop the function execution.
			assert !this.isFull : "Glass is already full. cant fill in more water";
	
			int prev_level = this.water_level;
			this.water_level= this.water_level+1;
			if(this.water_level == max_level)
			{
				isFull=true;
			}
			System.out.println("the water level is " + this.water_level);
			
			// Post Condition. we check that whenever the pre condition is met, 
			// the new water level is always greater than the original water level
			
			assert this.water_level>prev_level;
	}
	public static void main(String[] args)
	{
		WaterGlass myGlass=new WaterGlass();
		
		for(int i=0;i<=10;i++)
		{
			myGlass.pourWater();
			System.out.println("invariant is " + myGlass.invariant());
		}
	}
}

The output of this code is :

the water level is 1
invariant is true
the water level is 2
invariant is true
the water level is 3
invariant is true
the water level is 4
invariant is true
the water level is 5
invariant is true
the water level is 6
invariant is true
the water level is 7
invariant is true
the water level is 8
invariant is true
the water level is 9
invariant is true
the water level is 10
invariant is true
Exception in thread "main" java.lang.AssertionError: Glass is already full. cant fill in more water
	at WaterGlass.pourWater(WaterGlass.java:22)
	at WaterGlass.main(WaterGlass.java:43)

This is a way of implementing programming By Contract in Java.

Pre-Condition Check:

assert !this.isFull : "Glass is already full. cant fill in more water";

This checks if the glass is already full. If it is not full, the method executes. If it is full, the execution terminates.

Post-Condition Check:

assert this.water_level>prev_level;

This checks if the level of water is greater than the previous level. This should always be true given the pre-Condition is satisfied.

Class Invariant:

public boolean invariant()
	{
		
		return ( (this.isFull == true && water_level==max_level)|| ( this.isFull == false && water_level<max_level));
				 
	}

This checks that at any point of time during the execution of the class, if the glass is full, the water level should be maximum. If the glass is not full, the water level should be less than the maximum level.

This is an "almost similar" approach to Programming By Contract. When asked about why Java does not provide a full-fledged design-by-contract facility with preconditions, postconditions and class invariants, like the one in the Eiffel programming language, the answer is

"We considered providing such a facility, but were unable to convince ourselves that it is possible to graft it onto the Java programming language without massive changes to the Java platform libraries, and massive inconsistencies between old and new libraries. Further, we were not convinced that such a facility would preserve the simplicity that is the hallmark of the Java programming language. On balance, we came to the conclusion that a simple boolean assertion facility was a fairly straight-forward solution and far less risky. It's worth noting that adding a boolean assertion facility to the language doesn't preclude adding a full-fledged design-by-contract facility at some time in the future.

The simple assertion facility does enable a limited form of design-by-contract style programming. The assert statement is appropriate for nonpublic precondition, postcondition and class invariant checking. Public precondition checking should still be performed by checks inside methods that result in particular, documented exceptions, such as IllegalArgumentException and IllegalStateException."<ref>http://download.oracle.com/javase/1.4.2/docs/guide/lang/assert.html#design-faq</ref>

Conclusion

To the programmers, Programming By Contract guarantees that bugs will be prevented by a well defined mechanism.This is based on checks for pre-conditions. For customers, it offers a label of quality, seriousness, and a job well done.

To meet the needs of today's large-scale and mission critical applications, this unique solution is a must.<ref>http://www.eiffel.com/developers/design_by_contract.html</ref>

References

<references/>