13. Programming by Contract

1. Introduction

Sather inherits the design by contract (DBC) from Eiffel. DBC consists of precondition which callers (or clients) should guarantee and postcondition which the function (or server) should satisfies when return.

In addition, Sather offers other runtime safety nets such as assert and invariant.

These safety net is activated by adding the -chk flag when compiled. See sacomp man page for detailed information. It is recommended to activate the safety net when you write a big application as unexpected bugs may lurk in it.

2. Precondition

The precondition is a predicate that the callers should guarantee. If the predicate is not satisfied, the called function warns and the program terminates immediately.
Following is a part of array.sa. You should give a positive integer as an array size when you create an array (an instance of the ARRAY class) with size.

   create(n:INT):SAME pre n>=0 is 
      -- Create a new array of size `n' all of whose elements are void.
      return new(n) end;

3. Postcondition

The postcondition is the predicate that called function should guarantee. If not, the callers complain and program terminates immediately. A pre-defined word 'result' represents the return value of the method.

The following code is a safety version of the point.sa that I've showed previously.


   const eta:FLT:= 0.00001;       -- acceptable error

-- (snip)

   abs:FLT 
      post result >=0.0               -- check if the length is not negative
   is
      return (x*x+y*y).sqrt;
   end;

   rotate(theta:FLT):SAME 
      post result.abs/abs > 1.0-eta and result.abs/abs < 1.0+eta  -- Check if the difference of the distances from the orign before
   is                                                             -- and after rotation is in the acceptable error.
      theta := y.atan2(x)+theta;
      return #SAME(self.abs*theta.cos, self.abs*theta.sin);
   end;

4. assert

You can put this safety net inside of the method. If an assert returns false, the program complains and terminates.

Following is another safety version of the point.sa.

   out2file(a0,a1:ARRAY{POINT}) 
      pre a0.size > 0 and a1.size > 0  -- the size of the array should be positive.
   is
      f:FILE:=FILE::open_for_write(fout);
      assert ~f.error;        -- if file open error, terminate
      p0,p1:POINT;
      i:INT;
      loop
	 i:=(a0.size+1).times!;
	 if i = a0.size then i:=0; end;
	 p0:=a0[i];
	 p1:=a1[i];
	 f + p0.x + "\t" + p0.y + "\t" + p1.x + "\t" + p1.y + "\n";
      end;
      f.close;
   end;

5. invariant

The invariant:BOOL is somehow special. The program terminates when the instance does not satisfy this condition. It is seldom used and does not work properly in Sather-1.2.2.

6. The safety version of point.sa

Download and play with the safety version of the point.sa (point2.sa). Compile with the -chk option.

$ sacomp -chk point2.sa -o point2

7. Summerly

In this chapter, I've explained on the safety aspect of Sather breafly. This technique is usable in developing large scale applications. Use the safety feature as much as possible.