October 09, 2010
On Sat, 09 Oct 2010 15:32:26 +0400, Jonathan M Davis <jmdavisProg@gmx.com> wrote:

> On Saturday 09 October 2010 04:23:25 Denis Koroskin wrote:
>> On Sat, 09 Oct 2010 15:06:40 +0400, Jonathan M Davis <jmdavisProg@gmx.com>
>>
>> wrote:
>> > On Saturday 09 October 2010 03:47:52 Denis Koroskin wrote:
>> >> Why not just throw an exception and get a nice stack trace?
>> >
>> > You get a stack trace anyway with an assertion failure. And sure, they
>> > _could_
>> > make it so that the only way to output anything from a contract is to
>> > use an
>> > exception, but not only would that be more of a pain than using
>> > writeln(), but
>> > it would mean that the only time you could output anything would be on
>> > failure.
>> > As it is, you can print something every time that a contract is run.  
>> You
>> > couldn't do that with an exception.
>> >
>> > - Jonathan M Davis
>>
>> I could do the same within a function body.
>>
>> Anyway, I don't see the discussion going anywhere, it's just a matter of
>> preference and I don't really mind yours.
>
> Well, regardless of what we think and what the pros and cons of the situation
> actually are, as I understand it, the whole reason that contracts aren't pure is
> so that you can use writeln() in them for debugging.
>
> - Jonathan M Davis

I don't thinks so, it's rather the feature isn't fully implemented yet.
For example, up until recently you couldn't throw Exceptions from contracts, and was only be able to use asserts. That got changed because it was an easy to violate rule (by calling some other function that throws, e.g. enforce). Why do you think Walter disallowed throwing from contracts (other than asserts) in first place?
October 09, 2010
On Saturday 09 October 2010 04:49:08 Denis Koroskin wrote:
> On Sat, 09 Oct 2010 15:32:26 +0400, Jonathan M Davis <jmdavisProg@gmx.com>
> 
> wrote:
> > On Saturday 09 October 2010 04:23:25 Denis Koroskin wrote:
> >> On Sat, 09 Oct 2010 15:06:40 +0400, Jonathan M Davis <jmdavisProg@gmx.com>
> >> 
> >> wrote:
> >> > On Saturday 09 October 2010 03:47:52 Denis Koroskin wrote:
> >> >> Why not just throw an exception and get a nice stack trace?
> >> > 
> >> > You get a stack trace anyway with an assertion failure. And sure, they
> >> > _could_
> >> > make it so that the only way to output anything from a contract is to
> >> > use an
> >> > exception, but not only would that be more of a pain than using
> >> > writeln(), but
> >> > it would mean that the only time you could output anything would be on
> >> > failure.
> >> > As it is, you can print something every time that a contract is run.
> >> 
> >> You
> >> 
> >> > couldn't do that with an exception.
> >> > 
> >> > - Jonathan M Davis
> >> 
> >> I could do the same within a function body.
> >> 
> >> Anyway, I don't see the discussion going anywhere, it's just a matter of preference and I don't really mind yours.
> > 
> > Well, regardless of what we think and what the pros and cons of the
> > situation
> > actually are, as I understand it, the whole reason that contracts aren't
> > pure is
> > so that you can use writeln() in them for debugging.
> > 
> > - Jonathan M Davis
> 
> I don't thinks so, it's rather the feature isn't fully implemented yet. For example, up until recently you couldn't throw Exceptions from contracts, and was only be able to use asserts. That got changed because it was an easy to violate rule (by calling some other function that throws, e.g. enforce). Why do you think Walter disallowed throwing from contracts (other than asserts) in first place?

IIRC, TDPL specifically says that the reason that contracts aren't pure is so that you can use writeln() for debugging. And as for exceptions, why _would_ you throw them from a contract? Contracts are supposed to contain assertions and whatever code is necessary to set up what's given to them. That's it. Exceptions are used for error handling, which contracts aren't supposed to do.

- Jonathan M Davis
October 09, 2010
Denis Koroskin:

> Why do you think Walter disallowed throwing from contracts (other than asserts) in first place?

Probably because exceptions have no place in contracts. If a contract fails, the program is buggy, and it needs to stop. Contracts need to contain logical expressions that need to true for the contract to pass. And the compiler has to enforce the contracts statically as much as possible.

Thank you for all the answers. I'll add something in bugzilla soon.

Bye,
bearophile
October 09, 2010
Jonathan M Davis:

> What's odder is that the invariant is run after the precondition. That shouldn't be necessary, since any changes to the object would have been verifed after the last time that a public member function was called.

They may contain different tests.

Bye,
bearophile
October 09, 2010
On Saturday 09 October 2010 06:02:52 bearophile wrote:
> Jonathan M Davis:
> > What's odder is that the invariant is run after the
> > precondition. That shouldn't be necessary, since any changes to the
> > object would have been verifed after the last time that a public member
> > function was called.
> 
> They may contain different tests.

True, but assuming that there is no way to access the state of the object except through its public functions, then running the invariant before executing a public function is pointless, because it was already run after the last public function was called, and there's no way that the state of the object could have changed in the interim. However, given that returned references and pointers as well as public member variables would allow you to alter an object outside of its public functions, the object's state could have changed between its last public function call and the new public function call, so that's probably why the invariant is run before the public function is. However, if the state couldn't have changed since the last public function call, the running the invariant before the function call is pointless.

- Jonathan M Davis
October 09, 2010
Jonathan M Davis:

> if the state couldn't have changed since the last public function call, the running the invariant before the function call is pointless.

The post-condition of a method doesn't need to make sure the class is in a correct state, all it has to test is that its output (including the instance state it has modified) is correct.

The invariant instead has to test that the whole class instance is in a meaningful state. So method post-condition and class invariant contain different code and they must be run both, because the post-condition has to test just the class instance state it has changed, and not that such changes are globally coherent with the whole class instance state.

Bye,
bearophile
October 09, 2010
bearophile wrote:
> Jonathan M Davis:
> 
>> if the state couldn't have changed since the last public function call, the running the invariant before the function call is pointless.
> 
> The post-condition of a method doesn't need to make sure the class is in a correct state, all it has to test is that its output (including the instance state it has modified) is correct.
> 
> The invariant instead has to test that the whole class instance is in a meaningful state. So method post-condition and class invariant contain different code and they must be run both, because the post-condition has to test just the class instance state it has changed, and not that such changes are globally coherent with the whole class instance state.
> 
	Jonathan's point is not about running the post-condition and the
invariant. It is about running the invariant twice: both before and
after the function. This is completely independent from any pre- or
post-conditions there may be.

		Jerome
-- 
mailto:jeberger@free.fr
http://jeberger.free.fr
Jabber: jeberger@jabber.fr



October 09, 2010
J. Berger:

> 	Jonathan's point is not about running the post-condition and the
> invariant. It is about running the invariant twice: both before and
> after the function. This is completely independent from any pre- or
> post-conditions there may be.

You are missing something still.

C = a class with Dbc
foo = nonstatic method of C
fooargs = input arguments of foo
r = result of foo
S = state of the class instance foo
fooS = a subset of S, the part of the state influenced by foo
noFoo = S - fooS = part of S not influenced by foo
Inv = C invariant, that tests for coherence of the whole S
prefoo = pre-condition of foo
postfoo = post-condition of foo

Let's say DMD runs things in this order (this is not currently true but I think this is more correct): Inv prefoo foo postfoo Inv

Then:
- The first Inv tests that S is coherent
- prefoo tests that fooargs are correct (and maybe even that fooS is correct)
- postfoo tests that r and fooS are correct
- Inv tests that S is coherent

It's necessary to run Inv before and after foo because postfoo has not tested that the whole S is coherent.

foo is able to modify just fooS, it can't touch noFoo, but you need to run Inv again because inside Inv it may be present a predicate1(fooS, noFoo) that is true according to the relation between fooS and noFoo. So even if noFoo is unchanged, changes to fooS may be enough to invalidate predicate1.

Bye,
bearophile
October 09, 2010
bearophile wrote:
> J. Berger:
> 
>> 	Jonathan's point is not about running the post-condition and the
>> invariant. It is about running the invariant twice: both before and
>> after the function. This is completely independent from any pre- or
>> post-conditions there may be.
> 
> You are missing something still.
> 
	No.

> ... example pseudo-code

	This is more or less what Jonathan said in his last post.

		Jerome
-- 
mailto:jeberger@free.fr
http://jeberger.free.fr
Jabber: jeberger@jabber.fr



October 09, 2010
J. Berger:

> This is more or less what Jonathan said in his last post.

You are right, if the state isn't changed between two method calls, there's no point in calling the invariant two times after the method call and before the next method call.

Bye,
bearophile