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
