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

On 2013-02-05 17:57, bearophile wrote:
> 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.


There's been a lot of talk about properties lately.
If it's only a constraint on Foo.x, assert could go in setter.
But how to force using a setter in Foo(10) initialization?

Now, suppose there's a group constraint:

    struct Dist {
        double x, y; double d;
        invariant() { assert((abs(x) + abs(y) <= d)); }
    }

Normally I'd throw in: bool isValid() {return (abs..... );}
But let's say we let the invariant do automated checking.

When should Dist's state validity be checked?
On completed initialization and then on every write?
(also check every read if, God forbid, Dist isn't pure?)
Function contracts were easy compared to this. :)

FG:

> When should Dist's state validity be checked?

Maybe a good answer is written in the Ada2012 Standard.

Bye,
bearophile

Am 05.02.2013 19:26, schrieb bearophile:
> FG:
>
>> When should Dist's state validity be checked?
>
> Maybe a good answer is written in the Ada2012 Standard.
>
> Bye,
> bearophile

A look should also be given to Eiffel, after all it is the
language that created the notion of design by contract, AFAIK.

--
Paulo

On 2/5/2013 8:57 AM, bearophile wrote:
> D doesn't call the invariant even in that second case, as you see from this code
> that doesn't assert:

Invariants, per the spec, are called on the end of constructors, the beginning of destructors, and the beginning and end of public functions. Foo does not have any ctors/dtors/functions, hence no invariant call.

On Wednesday, 6 February 2013 at 04:05:23 UTC, Walter Bright wrote:
> On 2/5/2013 8:57 AM, bearophile wrote:
>> D doesn't call the invariant even in that second case, as you see from this code
>> that doesn't assert:
>
> Invariants, per the spec, are called on the end of constructors, the beginning of destructors, and the beginning and end of public functions. Foo does not have any ctors/dtors/functions, hence no invariant call.

Sounds like bug 519 to me.

Walter Bright:

> Invariants, per the spec, [...]

Right, I was proposing a little spec change.

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

Don:

> Sounds like bug 519 to me.

http://d.puremagic.com/issues/show_bug.cgi?id=519

Hours ago I have added this:
http://d.puremagic.com/issues/show_bug.cgi?id=9454

They are very similar, the test case from Issue 519 uses a new:


class Foo {
    invariant() {
        assert (false);
    }
}
void main() {
    Foo foo = new Foo();
}


While in Issue 9454 (just like in that Ada code) there is no new:


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


Maybe my Issue 9454 should be merged with Issue 519.

Bye,
bearophile

"bearophile" <bearophileHUGS@lycos.com> wrote in message news:dklglravazsxxbvrlplu@forum.dlang.org...
>
> They are very similar, the test case from Issue 519 uses a new:
>
[snip]
>
> While in Issue 9454 (just like in that Ada code) there is no new:
>
[snip]
>
> Maybe my Issue 9454 should be merged with Issue 519.
>

Issue 519 is about classes, while 9454 is about structs.  9454 uses a struct literal, not an autogenerated constructor call, so they are different bugs. 519 is an actual bug, while 9454 is an enhancement.

Daniel Murphy:

> Issue 519 is about classes, while 9454 is about structs.  9454 uses a struct
> literal, not an autogenerated constructor call, so they are different bugs.
> 519 is an actual bug, while 9454 is an enhancement.

Right, 9454 is tagged as enhancement since the beginning. But learning from other languages, like Ada, is good.

Bye,
bearophile

Not even mentioning Eiffel in an article about contract programming is weird..