Misleading contract syntax

[Norbert Nemec]

Hi there,

following the recent thread on contracts, I come to the conclusion that 
the current syntax is misleading and counterproductive.

* The concept of a contract is an expression, not a statement.
* A contract should *never* have side effects, otherwise debugging code 
may behave differently from release mode (which is the ultimate nightmare).
* Any reasonable example with contracts contains just a list of assertions.
* There is a fundamental distinction between assertions and contracts 
(see recent thread: contracts are part of interface design, assertions 
are computable comments)

=> Why are contracts defined as lists of statements in the first place? 
Defining contracts as side-effect free expressions would solve all of 
the above problems at once, decoupling the concepts of assertions and 
contracts and resulting in safer, much more concise code.

Just consider the example from 
http://en.wikipedia.org/wiki/Class_invariant#D rewritting using 
expressions as contracts. The strange "body" keyword becomes 
unnecessary. Inheritance of contracts can be achieved easily by 
concatenating in contract by 'or' operations and concatenating 
invariants and out contracts by 'and' operations.

-----------------

class Date {
     private int day, hour;

     invariant(1 <= day && day <= 31);
     invariant(0 <= hour && hour < 24);

     this(int d, int h) //constructor
         in (1 <= d && d <= 31 && 0 <= h && h < 24)
         out (day == d && hour == h)
         {
             day = d;
             hour = h;
         }

     public void setDay(int d)
         in (1 <= d && d <= 31)
         out (day == d)
         {
             day = d;
         }

     public void setHour(int h)
         in (0 <= h && h < 24)
         out (hour == h)
         {
             hour = h;
         }
}

void main() {
     Date d = new Date(/*d=*/10, /*h=*/5);
     d.setHour(30); // throws
}

----------------

B.t.w: to a useful, addition (orthogonal to the above change) would be 
access to the original state of the class in the out contract, e.g.:

----------------
     public void nextDay()
         out(day >= in.day)
         { day = day+1; }
----------------

Greetings,
Norbert