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
