An article about contract programming

[bearophile]

An article about Contract-Driven Programming:

http://electronicdesign.com/contributing-technical-experts/contract-driven-programming-takes-specification-beyond-stone-age

The article presents a little problem to be solved with contracts 
and the like:

<<
a simple system where physical objects are moved in a 
two-dimensional environment. Each object is associated with an X 
and Y coordinate, a size, and an identifier. A function "iterate" 
is called at each cycle and is responsible for updating the 
object's position by a step. Objects will be stored on a list.

In addition to the structural specification, we'll add some 
behavioral requirements:

1. X and Y must be within the interval [-200, 200].

2. Size must be within the interval [0 .. 100].

3. Except when set to the special non-initialized value, all 
object IDs must be unique.

4. Iterate must only be called on objects that have been 
initialized.

5. Iterate cannot change an object's size or ID.

6. Each movement made by iterate must be smaller than a tenth of 
the object's size.
>>

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

Then it presents three implementations (no D, unfortunately), 
this one is in Ada:

http://electronicdesign.com/site-files/electronicdesign.com/files/uploads/2013/02/0307RequiemCode3.gif

Among other things that Ada code shows the usage ranged values 
(X, Y and Size), and pre-state ( V.Y'Old ).

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

<<
In Ada 2012, predicates on a type (one particular type of 
invariant) are checked on parameter passing and assignment. So if 
we have Code 4, there will be a check failure on the assignment, 
since the predicate is not true. No check is generated on 
individual field modifications, though, so Code 5 does not raise 
an exception.
>>

http://electronicdesign.com/site-files/electronicdesign.com/files/uploads/2013/02/0307RequiemCode4.gif

http://electronicdesign.com/site-files/electronicdesign.com/files/uploads/2013/02/0307RequiemCode5.gif


In D this code doesn't asserts:


struct Foo {
     int x = 200;
     invariant() { assert(x > 100); }
}
void main() {
     auto f = Foo(10);
}


Maybe it's good to introduce in D as in Ada a call to the 
invariant when the whole struct is assigned.


<<
Although the assignment to the V fields breaks the invariant 
[figure 5], no exception is raised on these two statements. 
Thankfully, as soon as a call using V as a parameter is done, a 
subtype check will occur and the inconsistency will be pointed 
out. Hopefully, this will not be too far from the introduction of 
the problem.
>>


D doesn't call the invariant even in that second case, as you see 
from this code that doesn't assert:


struct Foo {
     int x = 200;
     invariant() { assert(x > 100); }
}
void bar(Foo f) {}
void main() {
     auto f = Foo(10);
     bar(f);
}

Bye,
bearophile