www.digitalmars.com         C & C++   DMDScript  

digitalmars.D.announce - An article about contract programming

reply "bearophile" <bearophileHUGS lycos.com> writes:
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



 Feb 05 2013



 next sibling parent reply FG <home fgda.pl>  writes:


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. :)



 Feb 05 2013



  parent reply "bearophile" <bearophileHUGS lycos.com>  writes:


FG:


 When should Dist's state validity be checked?


Maybe a good answer is written in the Ada2012 Standard.

Bye,
bearophile



 Feb 05 2013



  parent  Paulo Pinto <pjmlp progtools.org>  writes:


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



 Feb 05 2013



prev sibling next sibling parent reply Walter Bright <newshound2 digitalmars.com>  writes:


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.



 Feb 05 2013



 next sibling parent  "Don" <don nospam.com>  writes:


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.



 Feb 05 2013



prev sibling  parent reply "bearophile" <bearophileHUGS lycos.com>  writes:


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



 Feb 06 2013



  parent reply "Daniel Murphy" <yebblies nospamgmail.com>  writes:


"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. 



 Mar 05 2013



  parent  "bearophile" <bearophileHUGS lycos.com>  writes:


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



 Mar 06 2013



prev sibling  parent  "renoX" <renozyx gmail.com>  writes:


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



 Mar 07 2013