Jonathan M Davis:
> Yes, the problem creeps in because public methods are not necessarily the
> only
> way to alter the state of an object. Running the invariant before the
> function
> is run is actually a good catch on Walter's part. I wouldn't have thought of
> it
> precisely because it w
On Saturday 09 October 2010 08:39:30 bearophile wrote:
> 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 nex
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
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 miss
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 c
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
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 (inclu
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 cal
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
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
On Saturday 09 October 2010 04:49:08 Denis Koroskin wrote:
> On Sat, 09 Oct 2010 15:32:26 +0400, Jonathan M Davis
>
> wrote:
> > On Saturday 09 October 2010 04:23:25 Denis Koroskin wrote:
> >> On Sat, 09 Oct 2010 15:06:40 +0400, Jonathan M Davis
> >>
> >>
> >> wrote:
> >> > On Saturday 09 Octob
On Sat, 09 Oct 2010 15:32:26 +0400, Jonathan M Davis
wrote:
On Saturday 09 October 2010 04:23:25 Denis Koroskin wrote:
On Sat, 09 Oct 2010 15:06:40 +0400, Jonathan M Davis
wrote:
> On Saturday 09 October 2010 03:47:52 Denis Koroskin wrote:
>> Why not just throw an exception and get a nic
On Saturday 09 October 2010 04:23:25 Denis Koroskin wrote:
> On Sat, 09 Oct 2010 15:06:40 +0400, Jonathan M Davis
>
> 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 a
On Sat, 09 Oct 2010 15:06:40 +0400, Jonathan M Davis
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 t
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
On Sat, 09 Oct 2010 14:44:41 +0400, Jonathan M Davis
wrote:
On Saturday 09 October 2010 03:25:48 Denis Koroskin wrote:
Well, I meant they are conceptually pure.
Yes, they are conceptually pure, just not actually pure.
But do believe you shouldn't be able to use writeln in code like that.
On Saturday 09 October 2010 03:25:48 Denis Koroskin wrote:
> Well, I meant they are conceptually pure.
Yes, they are conceptually pure, just not actually pure.
> But do believe you shouldn't be able to use writeln in code like that. Why
> would you do it anyway? It's more or less like using asse
On Sat, 09 Oct 2010 14:20:18 +0400, Jonathan M Davis
wrote:
On Saturday 09 October 2010 03:09:30 Denis Koroskin wrote:
Given that pre-, post-conditions and invariants are all pure, it doesn't
really matter in what order they are executed.
In effect yes, but they aren't actually pure. If th
On Saturday 09 October 2010 03:09:30 Denis Koroskin wrote:
> Given that pre-, post-conditions and invariants are all pure, it doesn't
> really matter in what order they are executed.
In effect yes, but they aren't actually pure. If they were, you couldn't use
stuff
like writeln() in them. Howeve
On Sat, 09 Oct 2010 07:16:10 +0400, bearophile
wrote:
This is a simple D2 class that uses Contracts:
import std.c.stdio: printf;
class Car {
int speed = 0;
invariant() {
printf("Car invariant: %d\n", speed);
assert(speed >= 0);
}
this() {
printf("C
On Friday 08 October 2010 20:16:10 bearophile wrote:
> This is a simple D2 class that uses Contracts:
>
>
> import std.c.stdio: printf;
>
> class Car {
> int speed = 0;
>
> invariant() {
> printf("Car invariant: %d\n", speed);
> assert(speed >= 0);
> }
>
> this(
This is a simple D2 class that uses Contracts:
import std.c.stdio: printf;
class Car {
int speed = 0;
invariant() {
printf("Car invariant: %d\n", speed);
assert(speed >= 0);
}
this() {
printf("Car constructor: %d\n", speed);
speed = 0;
}
22 matches
Mail list logo
