Alex Rønne Petersen:

> So what if, for whatever reason, the invariant needs to track and maintain some state in order to catch some kind of ugly bug?

This is legitimate practical need. I know two or more ways to solve that problem, one of them is to implement the prestate (old). That's probably the largest hole in the D implementation of contract programming, and I have felt its need several times.

Another solution (that doesn't replace the need for the prestate!) is ghost fields, that are class instance/struct fields usable only inside contracts and that vanish in release mode:
http://d.puremagic.com/issues/show_bug.cgi?id=5027

Bye,
bearophile

On 03-08-2012 22:17, Davidson Corry wrote:
> On 8/3/2012 12:40 PM, bearophile wrote:
>> H. S. Teoh:
>>
>>> IMO, if you need to be changing stuff inside invariants, then you're
>>> using it wrong. Invariants are intended to verify program logic, not
>>> to do things like altering object state. The point is to be able to
>>> compile with invariant code turned off, and still have the program
>>> work exactly as before.
>>
>> I agree, modifying the state of the struct/class instance is not the job
>> of contracts and invariants. D contract programming is already not tidy,
>> so better to not make it even more messy.
>>
>> In a perfect world invariants and contracts should be pure too!
>
> Absolutely. Invariant clauses (and contract clauses generally) must not
> have side effects, lest the class behavior change depending upon whether
> or not they are compiled into the build. Assigning a value within the
> invariant clause is definitely a side effect.

Of course... it was an example to demonstrate the current situation. It was by no means meant to be a sensible piece of code.

>
> It is the job of the *constructor* to establish the invariant state,
> not of the invariant clause (which only *verifies* it).

Yes, but sometimes it's useful to track and maintain state in an invariant in order to debug certain bugs that only manifest in systems programming languages like D. Unlike languages like C#, we can get e.g. memory corruption in D.

I find that in practice, enforcing const in invariants has not helped me in any way. It has forced me to fix countless errors upon a DMD upgrade, none of which indicated actual problems. That's what I got out of that. The likelihood of an invariant visibly altering program semantics due to side-effects is so low it's not worth the huge breakage IMO.

Further, I had to insert casts that cast away constness in some cases because the standard library just isn't const-friendly enough. We need to get our priorities straight.

>
> The compiler *should* be catching a side effect in the invariant clause,
> if it can do so statically.
>

Not if it breaks my 30.000 lines source base where not even a single one of the errors caught actual bugs. I refer to this as "waste of time".

-- 
Alex Rønne Petersen
alex@lycus.org
http://lycus.org

On 03-08-2012 22:40, bearophile wrote:
> Alex Rønne Petersen:
>
>> So what if, for whatever reason, the invariant needs to track and
>> maintain some state in order to catch some kind of ugly bug?
>
> This is legitimate practical need. I know two or more ways to solve that
> problem, one of them is to implement the prestate (old). That's probably
> the largest hole in the D implementation of contract programming, and I
> have felt its need several times.
>
> Another solution (that doesn't replace the need for the prestate!) is
> ghost fields, that are class instance/struct fields usable only inside
> contracts and that vanish in release mode:
> http://d.puremagic.com/issues/show_bug.cgi?id=5027
>
> Bye,
> bearophile

I've used prestate in Spec#/Sing# and can definitely vouch for its usefulness.

-- 
Alex Rønne Petersen
alex@lycus.org
http://lycus.org

On 03-08-2012 22:32, Davidson Corry wrote:
> On 8/3/2012 1:14 PM, Paulo Pinto wrote:
>> Personally I feel D's contracts are still a bit off of what Eiffel,
>    .NET and Ada 2012 offer.
>
> On 8/3/2012 1:01 PM, Alex Rønne Petersen wrote:
>> So what if, for whatever reason, the invariant needs to track and
>> maintain some state in order to catch some kind of ugly bug?
>>
>> I agree that ideally an invariant should not ever need to change state.
>> But I think in some cases it can be a useful debugging tool.
>
> The "track and maintain some state" bit usually means capturing some
> state at entry to the class (via a public method), so that the invariant
> can at exit from the class compare the new, possibly modified, state
> to the previous one.
>
> This is the purpose of Eiffel's 'old' construct, which D does not have.
> (Yet.) (One hopes.) (And it would be nice to be able to capture an old
> *expression* and not just an old variable.)
>
> 'old' is used more often with postconditions than with invariants, but
> it can be useful in both.
>
>> But even ignoring that, making invariants const at this point in time is
>> just not practical. We seem to be doing things in the completely wrong
>> order. The library should be made const-friendly and *then* invariants
>> could be made const (not that I want them to be anyway).
>
> Certainly the libraries should be made as const-correct as possible. But
> it's not like we are forced to do only the one or the other (except for
> the insufficient supply of Walters, perhaps...). IMO, invariants should
> "be made const" (i.e. statically check for side effects) as discussed
> elsewhere. In fact, I believe that having more rigorous contract checks
> could *help* improve library code, by making it harder for loose code
> to get into the library.

The problem here is that making invariants const *now* means that using them in conjunction with Phobos code becomes next to impossible. Casting away const will become common practice, and that ain't exactly the way we want to go. :/

-- 
Alex Rønne Petersen
alex@lycus.org
http://lycus.org

On Friday, 3 August 2012 at 20:48:29 UTC, Alex Rønne Petersen wrote:
> The problem here is that making invariants const *now* means that using them in conjunction with Phobos code becomes next to impossible. Casting away const will become common practice, and that ain't exactly the way we want to go. :/

 Doesn't 'const' only qualify for the object's (this) code? If that's the case, you could have a global object inside a debug statement, then put those inside the invariants so you get your output (say, in a text file), while keeping it const. Having no side effects is pure, meaning global state would be unreachable (and debug already bypasses pure, but not safe).

Am Fri, 03 Aug 2012 22:40:02 +0200
schrieb "bearophile" <bearophileHUGS@lycos.com>:

> Another solution (that doesn't replace the need for the prestate!) is ghost fields, that are class instance/struct fields usable only inside contracts and that vanish in release mode: http://d.puremagic.com/issues/show_bug.cgi?id=5027
> 
> Bye,
> bearophile

While reading this thread I had the same idea. But the user must be 100% aware, that structs change size in release mode. This can be a real problem for data exchange with libraries using the same struct, in memory mapped files or in files.
Just imagine you stored some structured data in a file using the pointer and size of such a struct in release mode. Then you debug the program and you don't realize why the file cannot be loaded any more.
If it weren't for the systems programming language part (.sizeof, &...), it could be a nice proposal.

-- 
Marco

On Friday, August 03, 2012 12:36:41 H. S. Teoh wrote:
> IMO, if you need to be changing stuff inside invariants, then you're using it wrong. Invariants are intended to verify program logic, not to do things like altering object state. The point is to be able to compile with invariant code turned off, and still have the program work exactly as before.

I think that it's more of a problem of not being able to call non-const functions and the like. I'd definitely be against mutating anything in an invariant, but if your type doesn't work with const very well (and the recent debate about Object and const highlights how that can be a big issue), then forcing stuff like invariants and contracts to be const is problematic.

- Jonathan M Davis

It's worth pointing out the obvious, i.e. that as long as 'const' is physical const instead of logical const (which is always), invariants and contracts can't be const, because that would restrict them from calling methods that are logically but not physically const.

So I think they probably shouldn't be const.

On Saturday, 4 August 2012 at 06:53:16 UTC, Mehrdad wrote:
> It's worth pointing out the obvious, I.e. that as long as 'const' is physical const instead of logical const (which is always), invariants and contracts can't be const, because that would restrict them from calling methods that are logically but not physically const.
>
> So I think they probably shouldn't be const.

 As mentioned before, doesn't 'const' _only_ apply to the current (this) object and not anything else? Besides the contracts can't have lasting side effects that would change logical execution. How would changing the current object in an invariant be correct in release code?

 I'm not sure if the contracts should have many (or any) restrictions, but at the same time if you remove the contracts, nothing in the code should change the execution; Example: using writeln in an invariant should not change the current object/structure in any form, or anything it is part of. Although not writeln is not 'pure', const shouldn't prevent you from using it (pure or @safe declarations may withhold you).

On Saturday, August 04, 2012 09:06:19 Era Scarecrow wrote:
>   As mentioned before, doesn't 'const' _only_ apply to the current
> (this) object and not anything else? Besides the contracts can't
> have lasting side effects that would change logical execution.
> How would changing the current object in an invariant be correct
> in release code?

The problem is that if the this pointer/reference is const, then you can't call any member functions which aren't const, and you can't call any non-const functions on any member variables, because _they're_ const, because the this pointer/reference is const. And there are plenty of types out there which _can't_ have many of their member functions be const and do what they need to do, because D's const is both physical and transitive (unlike C++'s const). So, it's quite easy to get into a situation, where you can't call much of any functions at all if the this pointer/reference is const even though calling the non-const functions wouldn't actually mutate anything.

- Jonathan M Davis