Invariants for methods

[bearophile]

Jens Mueller:

> I see. bearophile even has a bug for this problem
> (http://d.puremagic.com/issues/show_bug.cgi?id=5027)

Issue 5027 is about ghost fields, not about "old", it's a related but separated problem/solution. In the meantime the idea of ghost fields was shot down for not being so important, so probably I will eventually close bug 5027...


> In particular I'm not sure whether bearophile agrees with having the out
> contract seeing the in contract's scope.

I write lot of posts, but I am not much expert yet, so I don't know what the better solution is. Both solutions have upsides and downsides:

The upsides of the "old" solution is that it's simple looking for the user and it's known to other people that already know DbC from C# and Eiffel. But in the "old" the compiler has to find a way to automatically copy a class instance, this is something that all D has avoided. So in the end the "old" approach may be doomed in D.

Seeing the precondition scope in the postcondition seems a good enough solution, it doesn't require new keywords, it does't ask the compiler to have an automatic way to copy class instances. The disadvantage is that it asks the programmer to invent ways to copy class instances every time the programmer wants to use a prestate, this is a lot of work, so I think very often class instances prestate will be not used (values prestate or pointer to values prestate will be used)... Even As another possible downside this solution may lead to DbC code less easy to reason about by automatic proof systems (this is a D DbC risk that I have discussed about some time ago, and it was dismissed) (Example: if you want a 2D matrix prestate you have to copy it in a foreach loop, this makes automatic analysis more and more difficult).


> But if that's a valid solution
> maybe he can add it to his bug report.

If you want to put it in bugzilla it's better to create something specific about DbC prestate, not about ghost fields.

Bye,
bearophile