Re: Communicating between in and out contracts
Steven Schveighoffer wrote: On Tue, 20 Oct 2009 13:13:07 -0400, Michel Fortin wrote: So what we need is semi-pure functions that can see all the globals as const data, or in other terms having no side effect but which can be affected by their environment. Another function qualifier, isn't it great! :-) Yeah, I meant which functions to allow among the functions types we already have. To introduce another function type *just to allow contracts to call them* is insanity. Note that there already is a gcc extension for this kind of function in C/C++: __attribute__((const)) Jerome -- mailto:jeber...@free.fr http://jeberger.free.fr Jabber: jeber...@jabber.fr signature.asc Description: OpenPGP digital signature
Re: Communicating between in and out contracts
On Tue, 20 Oct 2009 13:13:07 -0400, Michel Fortin wrote: So what we need is semi-pure functions that can see all the globals as const data, or in other terms having no side effect but which can be affected by their environment. Another function qualifier, isn't it great! :-) Yeah, I meant which functions to allow among the functions types we already have. To introduce another function type *just to allow contracts to call them* is insanity. -Steve
Re: Communicating between in and out contracts
On 2009-10-20 12:04:20 -0400, "Steven Schveighoffer"
said:
On Tue, 20 Oct 2009 11:57:05 -0400, Michel Fortin
wrote:
On 2009-10-20 11:44:00 -0400, "Steven Schveighoffer"
said:
On Tue, 20 Oct 2009 08:36:14 -0400, Michel Fortin
wrote:
On 2009-10-20 08:16:01 -0400, "Steven Schveighoffer"
said:
Incidentally, shouldn't all access to the object in the in contract be
const by default anyways?
Hum, access to everything (including global variables, arguments),
not just the object, should be const in a contract. That might be
harder to implement though.
Yeah, you are probably right. Of course, a const function can still
alter global state, but if you strictly disallowed altering global
state, we are left with only pure functions (and I think that's a
little harsh).
Not exactly. Pure functions can't even read global state (so their
result can't depend on anything but their arguments), but it makes
perfect sense to read global state in a contract. What you really need
is to have a const view of the global state. And this could apply to
all asserts too.
Yes, but what I'm talking about is "what functions can you call while
in a contract." Access to data should be const as you say. But if
you follow that logic to the most strict interpretation, the only
"safe" functions to allow are pure functions.
i.e.:
int x;
class C
{
void foo()
in
{
x = 5; // I agree this should be an error
bar(); // ok?
}
{}
void bar() const
{
x = 5;
}
}
When you try to write to x yes it's an error. But if you were reading x
it should not be an error. Basically inside the contract a global like
x should be seen as const(int) just like the object should be seen as
const(C).
Pure functions are somewhat alike, but are more restrictive since you
can only access immutable globals. So what we need is semi-pure
functions that can see all the globals as const data, or in other terms
having no side effect but which can be affected by their environment.
Another function qualifier, isn't it great! :-)
--
Michel Fortin
michel.for...@michelf.com
http://michelf.com/
Re: Communicating between in and out contracts
On Tue, 20 Oct 2009 11:57:05 -0400, Michel Fortin
wrote:
On 2009-10-20 11:44:00 -0400, "Steven Schveighoffer"
said:
On Tue, 20 Oct 2009 08:36:14 -0400, Michel Fortin
wrote:
On 2009-10-20 08:16:01 -0400, "Steven Schveighoffer"
said:
Incidentally, shouldn't all access to the object in the in contract
be const by default anyways?
Hum, access to everything (including global variables, arguments),
not just the object, should be const in a contract. That might be
harder to implement though.
Yeah, you are probably right. Of course, a const function can still
alter global state, but if you strictly disallowed altering global
state, we are left with only pure functions (and I think that's a
little harsh).
Not exactly. Pure functions can't even read global state (so their
result can't depend on anything but their arguments), but it makes
perfect sense to read global state in a contract. What you really need
is to have a const view of the global state. And this could apply to all
asserts too.
Yes, but what I'm talking about is "what functions can you call while in a
contract." Access to data should be const as you say. But if you follow
that logic to the most strict interpretation, the only "safe" functions to
allow are pure functions.
i.e.:
int x;
class C
{
void foo()
in
{
x = 5; // I agree this should be an error
bar(); // ok?
}
{}
void bar() const
{
x = 5;
}
}
-Steve
Re: Communicating between in and out contracts
On 2009-10-20 11:44:00 -0400, "Steven Schveighoffer" said: On Tue, 20 Oct 2009 08:36:14 -0400, Michel Fortin wrote: On 2009-10-20 08:16:01 -0400, "Steven Schveighoffer" said: Incidentally, shouldn't all access to the object in the in contract be const by default anyways? Hum, access to everything (including global variables, arguments), not just the object, should be const in a contract. That might be harder to implement though. Yeah, you are probably right. Of course, a const function can still alter global state, but if you strictly disallowed altering global state, we are left with only pure functions (and I think that's a little harsh). Not exactly. Pure functions can't even read global state (so their result can't depend on anything but their arguments), but it makes perfect sense to read global state in a contract. What you really need is to have a const view of the global state. And this could apply to all asserts too. -- Michel Fortin michel.for...@michelf.com http://michelf.com/
Re: Communicating between in and out contracts
On Tue, 20 Oct 2009 08:36:14 -0400, Michel Fortin wrote: On 2009-10-20 08:16:01 -0400, "Steven Schveighoffer" said: Incidentally, shouldn't all access to the object in the in contract be const by default anyways? Hum, access to everything (including global variables, arguments), not just the object, should be const in a contract. That might be harder to implement though. Yeah, you are probably right. Of course, a const function can still alter global state, but if you strictly disallowed altering global state, we are left with only pure functions (and I think that's a little harsh). -Steve
Re: Communicating between in and out contracts
On 2009-10-20 08:16:01 -0400, "Steven Schveighoffer" said: Incidentally, shouldn't all access to the object in the in contract be const by default anyways? Hum, access to everything (including global variables, arguments), not just the object, should be const in a contract. That might be harder to implement though. -- Michel Fortin michel.for...@michelf.com http://michelf.com/
Re: Communicating between in and out contracts
On Sun, 18 Oct 2009 03:44:39 -0400, Rainer Deyke wrote: Andrei Alexandrescu wrote: Rainer Deyke wrote: The expression may mutate stuff. It shouldn't. It's an error if it does, just like it's an error for an assertion or post/precondition to have any side effects. It would be nice if the compiler could catch this error, but failing that, 'old' expressions are still no worse than assertions in this respect. I'm coming into this a little late, but what Rainer is saying makes sense to me. Would it help to force any access to the object to be treated as if the object is const? i.e.: old(this.x) would be interpreted as: (cast(const(typeof(this))this).x and cached in the input contract section. It seems straightforward that Rainer's solution eliminates the boilerplate code of caching values available in the in contract, and if you force const access, prevents calling functions which might mutate the state of the object. But it uses the correct contract -- this object is not mutable for this call only. I agree pure is too restrictive, because then the object must be immutable, no? Incidentally, shouldn't all access to the object in the in contract be const by default anyways? -Steve
Re: Communicating between in and out contracts
Andrei Alexandrescu wrote: > Rainer Deyke wrote: > The expression may mutate stuff. It shouldn't. It's an error if it does, just like it's an error for an assertion or post/precondition to have any side effects. It would be nice if the compiler could catch this error, but failing that, 'old' expressions are still no worse than assertions in this respect. > If you know about Eiffel's old, I'd appreciate if you explained how it > works. I am arguing exactly because I don't know. My understanding is > that neither of us currently knows how it works, so I don't think it's > ok to refer me to Eiffel. My suggestion to ask the Eiffel community directly was meant seriously. -- Rainer Deyke - rain...@eldwood.com
Re: Communicating between in and out contracts
Rainer Deyke wrote: Andrei Alexandrescu wrote: It is if x is an _arbitrarily complex_ expression, and if that expression is part of a _complex control flow_. The language definition would have to decide exactly where complex is too complex in the expression or the control flow. That complicates the language. Also, by necessity the feature will be limited and will not give people enough freedom. It's lose-lose. The complexity of the expression is irrelevant, since the expression is simply moved to the beginning of the function as a unit. The expression may mutate stuff. Complex expressions are just simple expressions applied recursively. The compiler already knows how to deal with complex expressions. Heh, that's not what I was worried about. It's mutation and dependencies. Control flow is also irrelevant because it is simply ignored. The AST transformation sees this: blah blah old(x) blah old(y) blah ..and turns it into this: blah blah cached_value_0 blah cached_value_1 blah Yes, this means that the expressions 'x' and 'y' cannot use any local variables from the postcondition block. If you want to cache values in the precondition block for use in the postcondition block, you can't wait until you reach the postcondition block before deciding what to cache. This limitation exists whether the caching is manual or automated. If you insist on arguing about this, please direct your complaints to the Eiffel community and tell *them* how the language feature they've been using for years is broken. If there really is something wrong with Eiffel-style 'old' expressions, I'm sure the Eiffel community would know about it. If you know about Eiffel's old, I'd appreciate if you explained how it works. I am arguing exactly because I don't know. My understanding is that neither of us currently knows how it works, so I don't think it's ok to refer me to Eiffel. Andrei
Re: Communicating between in and out contracts
Andrei Alexandrescu wrote: > It is if x is an _arbitrarily complex_ expression, and if that > expression is part of a _complex control flow_. The language definition > would have to decide exactly where complex is too complex in the > expression or the control flow. That complicates the language. Also, by > necessity the feature will be limited and will not give people enough > freedom. It's lose-lose. The complexity of the expression is irrelevant, since the expression is simply moved to the beginning of the function as a unit. Complex expressions are just simple expressions applied recursively. The compiler already knows how to deal with complex expressions. Control flow is also irrelevant because it is simply ignored. The AST transformation sees this: blah blah old(x) blah old(y) blah ..and turns it into this: blah blah cached_value_0 blah cached_value_1 blah Yes, this means that the expressions 'x' and 'y' cannot use any local variables from the postcondition block. If you want to cache values in the precondition block for use in the postcondition block, you can't wait until you reach the postcondition block before deciding what to cache. This limitation exists whether the caching is manual or automated. If you insist on arguing about this, please direct your complaints to the Eiffel community and tell *them* how the language feature they've been using for years is broken. If there really is something wrong with Eiffel-style 'old' expressions, I'm sure the Eiffel community would know about it. -- Rainer Deyke - rain...@eldwood.com
Re: Communicating between in and out contracts
Rainer Deyke wrote:
Andrei Alexandrescu wrote:
If x is a complex expression and part of a complex control flow, it
becomes highly difficult what it means "at the beginning of the
function". It also becomes difficult to find a way to distinguish good
cases from bad cases without being overly conservative.
It looks like a more or less straightforward AST transformation to me.
in {
} body {
F();
} out {
G(old(x));
}
=>
{
auto old_x = x;
try {
F();
} finally {
G(old_x);
}
}
Repeat for each instance of 'old', in order of appearance. OK, it's not
entirely trivial, but it's not prohibitively difficult either.
It is if x is an _arbitrarily complex_ expression, and if that
expression is part of a _complex control flow_. The language definition
would have to decide exactly where complex is too complex in the
expression or the control flow. That complicates the language. Also, by
necessity the feature will be limited and will not give people enough
freedom. It's lose-lose.
Andrei
Re: Communicating between in and out contracts
Rainer Deyke wrote:
> {
>auto old_x = x;
>try {
> F();
>} finally {
> G(old_x);
>}
> }
Not 'finally', unless postconditions are checked when the function
terminates with an exception. This is closer to correct:
{
auto old_x = x;
// Preconditions go here.
F(); // <-- function body
G(old_x); // <-- postcondition
}
--
Rainer Deyke - rain...@eldwood.com
Re: Communicating between in and out contracts
Andrei Alexandrescu wrote:
> If x is a complex expression and part of a complex control flow, it
> becomes highly difficult what it means "at the beginning of the
> function". It also becomes difficult to find a way to distinguish good
> cases from bad cases without being overly conservative.
It looks like a more or less straightforward AST transformation to me.
in {
} body {
F();
} out {
G(old(x));
}
=>
{
auto old_x = x;
try {
F();
} finally {
G(old_x);
}
}
Repeat for each instance of 'old', in order of appearance. OK, it's not
entirely trivial, but it's not prohibitively difficult either.
--
Rainer Deyke - rain...@eldwood.com
Re: Communicating between in and out contracts
Rainer Deyke wrote: Andrei Alexandrescu wrote: Rainer Deyke wrote: Copying the object would be completely broken, so I'm sure that that's *not* how Eiffel does it. "It denotes the value the expression had on routine entry." In other words, the expression is evaluated once, on routine entry, and the result is cached for use in the postcondition. What if the expression is conditioned by the new state of the object? Not allowed. Since 'old(x)' is the value of 'x' evaluated at the beginning of the function, it must be possible to evaluate 'x' at the beginning of the function. Either rewrite the assertion or drop it. I have a feeling that this will only rarely be an issue. If x is a complex expression and part of a complex control flow, it becomes highly difficult what it means "at the beginning of the function". It also becomes difficult to find a way to distinguish good cases from bad cases without being overly conservative. I have no idea how Eiffel pulls it off. Andrei
Re: Communicating between in and out contracts
Andrei Alexandrescu wrote: > Rainer Deyke wrote: >> Copying the object would be completely broken, so I'm sure that that's >> *not* how Eiffel does it. "It denotes the value the expression had on >> routine entry." In other words, the expression is evaluated once, on >> routine entry, and the result is cached for use in the postcondition. > > What if the expression is conditioned by the new state of the object? Not allowed. Since 'old(x)' is the value of 'x' evaluated at the beginning of the function, it must be possible to evaluate 'x' at the beginning of the function. Either rewrite the assertion or drop it. I have a feeling that this will only rarely be an issue. -- Rainer Deyke - rain...@eldwood.com
Re: Communicating between in and out contracts
Leandro Lucarella wrote:
> Rainer Deyke, el 17 de octubre a las 14:24 me escribiste:
>> There is no "the object".
> There is an object if you have this:
>
> void f(SomeObjectWithLotsOfReferences obj) out {
> assert(old(obj).some_check());
> }
If 'obj' is a reference type and the reference itself wasn't modified,
then 'old(obj)' is the same as 'obj'. Objects are only copied if you
explicitly copy them. 'old(x)' means "the cached value of evaluating
'x' at the beginning of the routine". No more, no less.
--
Rainer Deyke - rain...@eldwood.com
Re: Communicating between in and out contracts
Rainer Deyke wrote: Andrei Alexandrescu wrote: Rainer Deyke wrote: Also, from the Eiffel docs (http://archive.eiffel.com/doc/online/eiffel50/intro/language/invitation-07.html): The notation 'old expression' is only valid in a routine postcondition. It denotes the value the expression had on routine entry. It seems that Eiffel had 'old' semantics that I've proposed all along. Great. Others brought it up too, inspired from Eiffel. Any significant problems with this approach would have been discovered by the Eiffel community by now. There is no problem if a copy of the object is made upon entry in the procedure. That's what I think Eiffel does. I was hoping to avoid that by allowing the "out" contract to see the definitions in the "in" contract. Copying the object would be completely broken, so I'm sure that that's *not* how Eiffel does it. "It denotes the value the expression had on routine entry." In other words, the expression is evaluated once, on routine entry, and the result is cached for use in the postcondition. What if the expression is conditioned by the new state of the object? Andrei
Re: Communicating between in and out contracts
Rainer Deyke, el 17 de octubre a las 14:24 me escribiste:
> Christopher Wright wrote:
> > Rainer Deyke wrote:
> >> It seems that Eiffel had 'old' semantics that I've proposed all along.
> >> Any significant problems with this approach would have been discovered
> >> by the Eiffel community by now.
> >
> > It requires duplicating the object. If the object is mutable, this
> > requires duplicating it and recursively duplicating everything it
> > references. If the object is immutable, this is free.
>
> There is no "the object".
>
> void f(string fname) out {
> file_size(fname) >= old(file_size(fname));
> }
There is an object if you have this:
void f(SomeObjectWithLotsOfReferences obj) out {
assert(old(obj).some_check());
}
But I don't see why the only option is too recursively copy the entire
object. You can do a shallow copy too. It's a little more error prone
since the programmer need to ensure that all needed "old" references are
kept, but it's realistic. And you have the exact same problem with the
ugly-nasty-oh-please-don't-do-it-like-that associative array of variant
approach too =)
So, if you *really* think that this "old stuff" is needed for contracts,
I prefer the old() approach than the ugly-nasty-...-that associative array
of variant =P
--
Leandro Lucarella (AKA luca) http://llucax.com.ar/
--
GPG Key: 5F5A8D05 (F8CD F9A7 BF00 5431 4145 104C 949E BFB6 5F5A 8D05)
--
Me encanta el éxito; por eso prefiero el estado de progreso constante,
con la meta al frente y no atrás.
-- Ricardo Vaporeso. Punta del Este, Enero de 1918.
Re: Communicating between in and out contracts
Christopher Wright wrote:
> Rainer Deyke wrote:
>> It seems that Eiffel had 'old' semantics that I've proposed all along.
>> Any significant problems with this approach would have been discovered
>> by the Eiffel community by now.
>
> It requires duplicating the object. If the object is mutable, this
> requires duplicating it and recursively duplicating everything it
> references. If the object is immutable, this is free.
There is no "the object".
void f(string fname) out {
file_size(fname) >= old(file_size(fname));
}
--
Rainer Deyke - rain...@eldwood.com
Re: Communicating between in and out contracts
Andrei Alexandrescu wrote: > Rainer Deyke wrote: >> Also, from the Eiffel docs >> (http://archive.eiffel.com/doc/online/eiffel50/intro/language/invitation-07.html): >> >> The notation 'old expression' is only valid in a routine >> postcondition. It denotes the value the expression had on routine entry. >> >> It seems that Eiffel had 'old' semantics that I've proposed all along. > > Great. Others brought it up too, inspired from Eiffel. > >> Any significant problems with this approach would have been discovered >> by the Eiffel community by now. > > There is no problem if a copy of the object is made upon entry in the > procedure. That's what I think Eiffel does. I was hoping to avoid that > by allowing the "out" contract to see the definitions in the "in" contract. Copying the object would be completely broken, so I'm sure that that's *not* how Eiffel does it. "It denotes the value the expression had on routine entry." In other words, the expression is evaluated once, on routine entry, and the result is cached for use in the postcondition. -- Rainer Deyke - rain...@eldwood.com
Re: Communicating between in and out contracts
Rainer Deyke wrote: Rainer Deyke wrote: Andrei Alexandrescu wrote: I honestly believe the whole "old" thing can't be made to work. Shall we move on to other possibilities instead of expending every effort on making this bear dance? It definitely /can/ be made to work, for some value of "work". It sacrifices the natural order of evaluation to gain a concise and intuitive syntax. I don't think it should be dismissed out of hand. Also, from the Eiffel docs (http://archive.eiffel.com/doc/online/eiffel50/intro/language/invitation-07.html): The notation 'old expression' is only valid in a routine postcondition. It denotes the value the expression had on routine entry. It seems that Eiffel had 'old' semantics that I've proposed all along. Great. Others brought it up too, inspired from Eiffel. Any significant problems with this approach would have been discovered by the Eiffel community by now. There is no problem if a copy of the object is made upon entry in the procedure. That's what I think Eiffel does. I was hoping to avoid that by allowing the "out" contract to see the definitions in the "in" contract. Andrei
Re: Communicating between in and out contracts
Rainer Deyke wrote: Rainer Deyke wrote: Andrei Alexandrescu wrote: I honestly believe the whole "old" thing can't be made to work. Shall we move on to other possibilities instead of expending every effort on making this bear dance? It definitely /can/ be made to work, for some value of "work". It sacrifices the natural order of evaluation to gain a concise and intuitive syntax. I don't think it should be dismissed out of hand. Also, from the Eiffel docs (http://archive.eiffel.com/doc/online/eiffel50/intro/language/invitation-07.html): The notation 'old expression' is only valid in a routine postcondition. It denotes the value the expression had on routine entry. It seems that Eiffel had 'old' semantics that I've proposed all along. Any significant problems with this approach would have been discovered by the Eiffel community by now. It requires duplicating the object. If the object is mutable, this requires duplicating it and recursively duplicating everything it references. If the object is immutable, this is free.
Re: Communicating between in and out contracts
Rainer Deyke wrote: > Andrei Alexandrescu wrote: >> I honestly believe the whole "old" thing can't be made to work. Shall we >> move on to other possibilities instead of expending every effort on >> making this bear dance? > > It definitely /can/ be made to work, for some value of "work". It > sacrifices the natural order of evaluation to gain a concise and > intuitive syntax. I don't think it should be dismissed out of hand. Also, from the Eiffel docs (http://archive.eiffel.com/doc/online/eiffel50/intro/language/invitation-07.html): The notation 'old expression' is only valid in a routine postcondition. It denotes the value the expression had on routine entry. It seems that Eiffel had 'old' semantics that I've proposed all along. Any significant problems with this approach would have been discovered by the Eiffel community by now. -- Rainer Deyke - rain...@eldwood.com
Re: Communicating between in and out contracts
Andrei Alexandrescu wrote: > Lutger wrote: > >> What is the benefit of variants here? Maybe I'm missing something, it >> just seems a little verbose and lose out on the type system (IDE support >> and such). Wouldn't it also tie the variant type to the language or is >> that not a problem? > > The nice thing there is that you have a single type to be a generic bag > for any types. > > Andrei How? I mean that is a property of variants in general. Pre- and postconditions are written next to each other. I don't see anything generic about them, what am I missing? Let me rephrase that: if I have to write '*storage["oldSize"].peek!(int) == ...' in the out contract as opposed to just 'oldSize == ...', how would that be a win?
Re: Communicating between in and out contracts
Andrei Alexandrescu wrote: > Rats, I meant assert(old.gun(i * i)). That's what compounds the > difficulty of the example. That wouldn't be allowed. More specifically 'old(gun(i * i))' wouldn't be allowed. 'old(this).gun(i * i)' would be allowed, but probably wouldn't do what you want it to do. 'old(this.clone()).gun(i * i)' would be allowed and would work, assuming that the 'clone' method is defined and has the right semantics. The general rule is that for any 'old(expr)', 'expr' only has access to variables that are accessible in the 'in' block. Preferably const access. > I honestly believe the whole "old" thing can't be made to work. Shall we > move on to other possibilities instead of expending every effort on > making this bear dance? It definitely /can/ be made to work, for some value of "work". It sacrifices the natural order of evaluation to gain a concise and intuitive syntax. I don't think it should be dismissed out of hand. -- Rainer Deyke - rain...@eldwood.com
Re: Communicating between in and out contracts
Lutger wrote:
Denis Koroskin wrote:
On Sat, 17 Oct 2009 00:54:51 +0400, Denis Koroskin <2kor...@gmail.com>
wrote:
On Sat, 17 Oct 2009 00:28:55 +0400, Denis Koroskin <2kor...@gmail.com>
wrote:
On Sat, 17 Oct 2009 00:22:54 +0400, Andrei Alexandrescu
wrote:
Jason House wrote:
if fun or gun is impure, then they should not be callable by the
contracts. Because of that, order is irrelevant.
1. Restricting calls to pure functions is sensible, but was deemed too
restrictive.
2. Even so, there's difficulty on what to cache. The amount cached may
depend on both the old and new object (in my example it only depends
on the old object).
3. There's too much hidden work and too much smarts involved. I just
don't think that's a feasible solution with what we know and have
right now.
Andrei
When not just let users one variable of type Variant per contract to
store whatever they want?
I mean, not a Variant, but a Dynamic* object so that the following would
be possible:
void push(T)(T val)
in(storage)
{
storage.oldSize = this.size; // store
//storage.anyDynamicProperty = anyDynamicValue; in general case
}
out(storage)
{
assert(storage.oldSize + 1 == this.size); // access
}
body
{
// impl
}
*do you recall the Dynamic class discussion (a class that allows any
arbitrary methods and properties access, similar to JavaScript objects
or dynamic objects in C#)
On second thought Dynamic objects need run-time reflection that D
currently lacks.
Alternatively users may be given a Variant[string] assoc.array as a
poor-man's replacement for a full-fledged Dynamic object:
void push(T)(T val)
in(storage)
{
storage["oldSize"] = this.size();
}
out(storage)
{
assert(*storage["oldSize"].peek!(int) == this.size - 1);
}
body
{
// impl
}
The contracts userdata would be stored in a stack alongside with monitor,
classinfo etc for classes, and past the data fields for structs.
What is the benefit of variants here? Maybe I'm missing something, it just
seems a little verbose and lose out on the type system (IDE support and
such). Wouldn't it also tie the variant type to the language or is that not
a problem?
The nice thing there is that you have a single type to be a generic bag
for any types.
Andrei
Re: Communicating between in and out contracts
Denis Koroskin wrote:
> On Sat, 17 Oct 2009 00:54:51 +0400, Denis Koroskin <2kor...@gmail.com>
> wrote:
>
>> On Sat, 17 Oct 2009 00:28:55 +0400, Denis Koroskin <2kor...@gmail.com>
>> wrote:
>>
>>> On Sat, 17 Oct 2009 00:22:54 +0400, Andrei Alexandrescu
>>> wrote:
>>>
Jason House wrote:
> if fun or gun is impure, then they should not be callable by the
> contracts. Because of that, order is irrelevant.
1. Restricting calls to pure functions is sensible, but was deemed too
restrictive.
2. Even so, there's difficulty on what to cache. The amount cached may
depend on both the old and new object (in my example it only depends
on the old object).
3. There's too much hidden work and too much smarts involved. I just
don't think that's a feasible solution with what we know and have
right now.
Andrei
>>>
>>> When not just let users one variable of type Variant per contract to
>>> store whatever they want?
>>
>> I mean, not a Variant, but a Dynamic* object so that the following would
>> be possible:
>>
>> void push(T)(T val)
>> in(storage)
>> {
>> storage.oldSize = this.size; // store
>> //storage.anyDynamicProperty = anyDynamicValue; in general case
>> }
>> out(storage)
>> {
>> assert(storage.oldSize + 1 == this.size); // access
>> }
>> body
>> {
>> // impl
>> }
>>
>> *do you recall the Dynamic class discussion (a class that allows any
>> arbitrary methods and properties access, similar to JavaScript objects
>> or dynamic objects in C#)
>
> On second thought Dynamic objects need run-time reflection that D
> currently lacks.
>
> Alternatively users may be given a Variant[string] assoc.array as a
> poor-man's replacement for a full-fledged Dynamic object:
>
> void push(T)(T val)
> in(storage)
> {
> storage["oldSize"] = this.size();
> }
> out(storage)
> {
> assert(*storage["oldSize"].peek!(int) == this.size - 1);
> }
> body
> {
> // impl
> }
>
> The contracts userdata would be stored in a stack alongside with monitor,
> classinfo etc for classes, and past the data fields for structs.
What is the benefit of variants here? Maybe I'm missing something, it just
seems a little verbose and lose out on the type system (IDE support and
such). Wouldn't it also tie the variant type to the language or is that not
a problem?
Re: Communicating between in and out contracts
Andrei Alexandrescu Wrote:
> Jason House wrote:
> > if fun or gun is impure, then they should not be callable by the
> > contracts. Because of that, order is irrelevant.
>
> 1. Restricting calls to pure functions is sensible, but was deemed too
> restrictive.
I don't know about others, but my use of contracts have always been pure. If my
contracts violate that, then they're serving some other purpose and probably
should not be a contract in the first place.
> 2. Even so, there's difficulty on what to cache. The amount cached may
> depend on both the old and new object (in my example it only depends on
> the old object).
>
> 3. There's too much hidden work and too much smarts involved. I just
> don't think that's a feasible solution with what we know and have right now.
You never asked if it was too much work for Walter ;)
Honestly, I think it may be simple enough to allow static (immutable) variable
declarations within the in contract to be seen in the out contract. Maybe it
isn't done with the static keyword.
in{
keep oldLength = length;
...
}
out{
assert(oldLength == length + 1;
}
Re: Communicating between in and out contracts
Denis Koroskin wrote:
On Sat, 17 Oct 2009 00:54:51 +0400, Denis Koroskin <2kor...@gmail.com>
wrote:
On Sat, 17 Oct 2009 00:28:55 +0400, Denis Koroskin <2kor...@gmail.com>
wrote:
On Sat, 17 Oct 2009 00:22:54 +0400, Andrei Alexandrescu
wrote:
Jason House wrote:
if fun or gun is impure, then they should not be callable by the
contracts. Because of that, order is irrelevant.
1. Restricting calls to pure functions is sensible, but was deemed
too restrictive.
2. Even so, there's difficulty on what to cache. The amount cached
may depend on both the old and new object (in my example it only
depends on the old object).
3. There's too much hidden work and too much smarts involved. I just
don't think that's a feasible solution with what we know and have
right now.
Andrei
When not just let users one variable of type Variant per contract to
store whatever they want?
I mean, not a Variant, but a Dynamic* object so that the following
would be possible:
void push(T)(T val)
in(storage)
{
storage.oldSize = this.size; // store
//storage.anyDynamicProperty = anyDynamicValue; in general case
}
out(storage)
{
assert(storage.oldSize + 1 == this.size); // access
}
body
{
// impl
}
*do you recall the Dynamic class discussion (a class that allows any
arbitrary methods and properties access, similar to JavaScript objects
or dynamic objects in C#)
On second thought Dynamic objects need run-time reflection that D
currently lacks.
Alternatively users may be given a Variant[string] assoc.array as a
poor-man's replacement for a full-fledged Dynamic object:
void push(T)(T val)
in(storage)
{
storage["oldSize"] = this.size();
}
out(storage)
{
assert(*storage["oldSize"].peek!(int) == this.size - 1);
}
body
{
// impl
}
The contracts userdata would be stored in a stack alongside with
monitor, classinfo etc for classes, and past the data fields for structs.
I like this solution.
Andrei
Re: Communicating between in and out contracts
On Sat, 17 Oct 2009 00:54:51 +0400, Denis Koroskin <2kor...@gmail.com>
wrote:
On Sat, 17 Oct 2009 00:28:55 +0400, Denis Koroskin <2kor...@gmail.com>
wrote:
On Sat, 17 Oct 2009 00:22:54 +0400, Andrei Alexandrescu
wrote:
Jason House wrote:
if fun or gun is impure, then they should not be callable by the
contracts. Because of that, order is irrelevant.
1. Restricting calls to pure functions is sensible, but was deemed too
restrictive.
2. Even so, there's difficulty on what to cache. The amount cached may
depend on both the old and new object (in my example it only depends
on the old object).
3. There's too much hidden work and too much smarts involved. I just
don't think that's a feasible solution with what we know and have
right now.
Andrei
When not just let users one variable of type Variant per contract to
store whatever they want?
I mean, not a Variant, but a Dynamic* object so that the following would
be possible:
void push(T)(T val)
in(storage)
{
storage.oldSize = this.size; // store
//storage.anyDynamicProperty = anyDynamicValue; in general case
}
out(storage)
{
assert(storage.oldSize + 1 == this.size); // access
}
body
{
// impl
}
*do you recall the Dynamic class discussion (a class that allows any
arbitrary methods and properties access, similar to JavaScript objects
or dynamic objects in C#)
On second thought Dynamic objects need run-time reflection that D
currently lacks.
Alternatively users may be given a Variant[string] assoc.array as a
poor-man's replacement for a full-fledged Dynamic object:
void push(T)(T val)
in(storage)
{
storage["oldSize"] = this.size();
}
out(storage)
{
assert(*storage["oldSize"].peek!(int) == this.size - 1);
}
body
{
// impl
}
The contracts userdata would be stored in a stack alongside with monitor,
classinfo etc for classes, and past the data fields for structs.
Re: Communicating between in and out contracts
Rainer Deyke wrote:
Andrei Alexandrescu wrote:
class A {
int fun() { ... }
int gun(int) { ... }
int foo()
in {
}
out(result) {
if (old.fun())
assert(old.gun(5));
else
assert(old.fun() + old.gun(6));
foreach (i; 1 .. old.fun())
assert(gun(i * i));
}
...
}
Now please tell what's cached and in what order.
The following are cached, in this order:
fun()
gun(5)
gun(6)
Old values are calculated in the order in which they appear in the
function, but only once each.
Rats, I meant assert(old.gun(i * i)). That's what compounds the
difficulty of the example.
However, I strongly prefer the following syntax:
class A {
int fun() { ... }
int gun(int) { ... }
int foo()
in {
}
out(result) {
if (old(fun()))
assert(old(gun(5)));
else
assert(old(fun()) + old(gun(6)));
foreach (i; 1 .. old(fun()))
assert(gun(i * i));
}
...
}
This lets you distinguish between the following cases:
old(f().g())
old(f()).g()
It also lets you cache non-members:
old(arg);
old(global_var);
For example:
void increment_global_counter() out {
global_counter = old(global_counter) + 1;
}
I honestly believe the whole "old" thing can't be made to work. Shall we
move on to other possibilities instead of expending every effort on
making this bear dance?
Andrei
Re: Communicating between in and out contracts
On Sat, 17 Oct 2009 00:28:55 +0400, Denis Koroskin <2kor...@gmail.com>
wrote:
On Sat, 17 Oct 2009 00:22:54 +0400, Andrei Alexandrescu
wrote:
Jason House wrote:
if fun or gun is impure, then they should not be callable by the
contracts. Because of that, order is irrelevant.
1. Restricting calls to pure functions is sensible, but was deemed too
restrictive.
2. Even so, there's difficulty on what to cache. The amount cached may
depend on both the old and new object (in my example it only depends on
the old object).
3. There's too much hidden work and too much smarts involved. I just
don't think that's a feasible solution with what we know and have right
now.
Andrei
When not just let users one variable of type Variant per contract to
store whatever they want?
I mean, not a Variant, but a Dynamic* object so that the following would
be possible:
void push(T)(T val)
in(storage)
{
storage.oldSize = this.size; // store
//storage.anyDynamicProperty = anyDynamicValue; in general case
}
out(storage)
{
assert(storage.oldSize + 1 == this.size); // access
}
body
{
// impl
}
*do you recall the Dynamic class discussion (a class that allows any
arbitrary methods and properties access, similar to JavaScript objects or
dynamic objects in C#)
Re: Communicating between in and out contracts
Andrei Alexandrescu wrote:
> class A {
> int fun() { ... }
> int gun(int) { ... }
>
> int foo()
> in {
> }
> out(result) {
> if (old.fun())
>assert(old.gun(5));
> else
>assert(old.fun() + old.gun(6));
> foreach (i; 1 .. old.fun())
>assert(gun(i * i));
> }
> ...
> }
>
> Now please tell what's cached and in what order.
The following are cached, in this order:
fun()
gun(5)
gun(6)
Old values are calculated in the order in which they appear in the
function, but only once each.
However, I strongly prefer the following syntax:
class A {
int fun() { ... }
int gun(int) { ... }
int foo()
in {
}
out(result) {
if (old(fun()))
assert(old(gun(5)));
else
assert(old(fun()) + old(gun(6)));
foreach (i; 1 .. old(fun()))
assert(gun(i * i));
}
...
}
This lets you distinguish between the following cases:
old(f().g())
old(f()).g()
It also lets you cache non-members:
old(arg);
old(global_var);
For example:
void increment_global_counter() out {
global_counter = old(global_counter) + 1;
}
--
Rainer Deyke - rain...@eldwood.com
Re: Communicating between in and out contracts
On Sat, 17 Oct 2009 00:22:54 +0400, Andrei Alexandrescu wrote: Jason House wrote: if fun or gun is impure, then they should not be callable by the contracts. Because of that, order is irrelevant. 1. Restricting calls to pure functions is sensible, but was deemed too restrictive. 2. Even so, there's difficulty on what to cache. The amount cached may depend on both the old and new object (in my example it only depends on the old object). 3. There's too much hidden work and too much smarts involved. I just don't think that's a feasible solution with what we know and have right now. Andrei When not just let users one variable of type Variant per contract to store whatever they want?
Re: Communicating between in and out contracts
Jason House wrote: if fun or gun is impure, then they should not be callable by the contracts. Because of that, order is irrelevant. 1. Restricting calls to pure functions is sensible, but was deemed too restrictive. 2. Even so, there's difficulty on what to cache. The amount cached may depend on both the old and new object (in my example it only depends on the old object). 3. There's too much hidden work and too much smarts involved. I just don't think that's a feasible solution with what we know and have right now. Andrei
Re: Communicating between in and out contracts
Andrei Alexandrescu Wrote:
> Walter Bright wrote:
> > Rainer Deyke wrote:
> >> Andrei Alexandrescu wrote:
> >>> Eiffel offers the "old" keyword that refers to the old object in a
> >>> postcondition. But it seems quite wasteful to clone the object just to
> >>> have a contract look at a little portion of the old object.
> >>
> >> You don't need to clone the whole object. You just need to cache the
> >> properties that are used with 'old'.
> >
> > That's a good idea.
>
> Should work, but it has more than a few subtleties. Consider:
>
> class A {
> int fun() { ... }
> int gun(int) { ... }
>
> int foo()
> in {
> }
> out(result) {
> if (old.fun())
> assert(old.gun(5));
> else
> assert(old.fun() + old.gun(6));
> foreach (i; 1 .. old.fun())
> assert(gun(i * i));
> }
> ...
> }
>
> Now please tell what's cached and in what order.
>
>
> Andrei
if fun or gun is impure, then they should not be callable by the contracts.
Because of that, order is irrelevant.
Re: Communicating between in and out contracts
Walter Bright wrote:
Rainer Deyke wrote:
Andrei Alexandrescu wrote:
Eiffel offers the "old" keyword that refers to the old object in a
postcondition. But it seems quite wasteful to clone the object just to
have a contract look at a little portion of the old object.
You don't need to clone the whole object. You just need to cache the
properties that are used with 'old'.
That's a good idea.
Should work, but it has more than a few subtleties. Consider:
class A {
int fun() { ... }
int gun(int) { ... }
int foo()
in {
}
out(result) {
if (old.fun())
assert(old.gun(5));
else
assert(old.fun() + old.gun(6));
foreach (i; 1 .. old.fun())
assert(gun(i * i));
}
...
}
Now please tell what's cached and in what order.
Andrei
Re: Communicating between in and out contracts
Walter Bright: > Rainer Deyke: > > You don't need to clone the whole object. You just need to cache the > > properties that are used with 'old'. > > That's a good idea. Once in a time I want to improve Walter's mood. This is a list of the top 25 requests for improvements to the Java language (some of them are about 10 years old, so people like me that complain that Walter isn't implementing their ideas have to compare the situation with the Sun engineers that sometimes look like molass): http://bugs.sun.com/bugdatabase/top25_rfes.do The top request, with 592 votes, submitted originally 23-APR-2001, asks for "Support For 'Design by Contract', beyond "a simple assertion facility"". I don't know if D programmers like to use such contracts often, but it seems several Java programmers wants them (even if in Java there are already ways to write unit tests that are far better&more flexible than D ones!). Bye, bearophile
Re: Communicating between in and out contracts
Rainer Deyke wrote: Andrei Alexandrescu wrote: Eiffel offers the "old" keyword that refers to the old object in a postcondition. But it seems quite wasteful to clone the object just to have a contract look at a little portion of the old object. You don't need to clone the whole object. You just need to cache the properties that are used with 'old'. That's a good idea.
Re: Communicating between in and out contracts
Kagamin wrote:
Andrei Alexandrescu Wrote:
void push(T value);
in {
auto oldLength = length();
}
out {
assert(value == top());
assert(length == oldLength + 1);
}
Walter tried to implement that but it turned out to be very difficult
implementation-wise.
What is the problem? Syntactical, semantical or ABI-related?
This. What does it mean "implementation-wise"?
Re: Communicating between in and out contracts
Andrei Alexandrescu wrote:
>void push(T value);
>in {
> auto oldLength = length();
>}
>out {
> assert(value == top());
> assert(length == oldLength + 1);
>}
Another keyword abuse:
void push(T value);
in {
auto in.oldLength = length();
}
out {
assert(value == top());
assert(length == in.oldLength + 1);
}
Re: Communicating between in and out contracts
Chris Nicholson-Sauls Wrote:
> How hard would it be to do something like this: collect any local variables
> declared in
> the precondition into a structure, and make that structure transparently
> available to the
> postcondition. So your push case above gets rewritten to something like this:
>
> __magic_tmp = {
> typeof( length() ) oldLength;
> }
> in {
> __magic_tmp.oldLength = length();
> }
> out {
> assert(value == top());
> assert(length == __magic_tmp.oldLength + 1);
> }
We have so many nifty keywords in D, I can't stand against abusing them
(contracts already do it).
void push(T value);
shared {
typeof(length()) oldLength;
}
in {
oldLength = length();
}
out {
assert(value == top());
assert(length == oldLength + 1);
}
Re: Communicating between in and out contracts
Andrei Alexandrescu Wrote:
> void push(T value);
> in {
>auto oldLength = length();
> }
> out {
>assert(value == top());
>assert(length == oldLength + 1);
> }
>
> Walter tried to implement that but it turned out to be very difficult
> implementation-wise.
What is the problem? Syntactical, semantical or ABI-related?
Re: Communicating between in and out contracts
Andrei Alexandrescu wrote:
> Eiffel offers the "old" keyword that refers to the old object in a
> postcondition. But it seems quite wasteful to clone the object just to
> have a contract look at a little portion of the old object.
You don't need to clone the whole object. You just need to cache the
properties that are used with 'old'. In other words, this functionality:
>void push(T value);
>in {
> auto oldLength = length();
>}
>out {
> assert(value == top());
> assert(length == oldLength + 1);
>}
...can be expressed with this syntax:
void push(T value);
out {
assert(value == top());
assert(length == old length + 1);
}
The syntax with 'old' is more concise, easier to read, and does the same
thing. What's wrong with it (other than adding yet another keyword to
the language)?
--
Rainer Deyke - rain...@eldwood.com
Re: Communicating between in and out contracts
Andrei Alexandrescu wrote:
> Lutger wrote:
>> Between sharing the whole object and sharing scope lies specifying
>> exactly what to share, I'd think.
>>
>> Here is one possible syntax, like regular function calls. Parameter types
>> can possibly be inferred and omitted:
>>
>> void push(T value);
>> in {
>>out(length());
>> }
>> out(size_t oldLength) {
>>assert(value == top());
>>assert(length == oldLength + 1);
>> }
>
>
> I think this could work. One of Walter's ideas was to pass the entire
> old object as an argument to out. Passing handpicked data is more work
> for the user but faster.
>
> Perhaps this would simplify things a bit:
>
> void push(T value);
> in {
> auto oldLength = length;
> }
> out(oldLength) {
> assert(value == top());
> assert(length == oldLength + 1);
> }
>
> Whatever parameters you pass to out they'd be matched by name with stuff
> defined in the "in" contract. That poses a problem because until now
> out(whatever) automatically passed the result to the out contract under
> the name "whatever".
>
>
> Andrei
Right, I forgot about that, you do need that return variable or have to
invent a magic name. Jeremie's proposal doesn't have that problem, taking
the reverse route of letting in{} define which variabeles are to be passed
to the out function.
So either would work:
in{
auto oldLength = length;
out(oldLength);
}
or:
in{
out auto oldLength = length;
}
Whatever syntax is chosen, it doesn't strike me as cumbersome to handpick
variables considering what you get from it. Also, some conditions may depend
on calculated values, in those cases it may even be more straightforward
than checking an old copy of the object.
Re: Communicating between in and out contracts
Lutger wrote:
Between sharing the whole object and sharing scope lies specifying exactly
what to share, I'd think.
Here is one possible syntax, like regular function calls. Parameter types
can possibly be inferred and omitted:
void push(T value);
in {
out(length());
}
out(size_t oldLength) {
assert(value == top());
assert(length == oldLength + 1);
}
I like this, but I wouldnt make a regular function call:
void push(T value)
in {
out auto oldLength = length();
}
out {
assert(value == top());
assert(length() == oldLength + 1);
}
body {
...
}
If you declare variables as 'out' in a precondition, they are hidden
from the body and visible in the post condition.
The implementation of this is as easy as pushing oldLength on the stack
in the precondition and poping it in the postcondition.
Jeremie
Re: Communicating between in and out contracts
Lutger wrote:
Between sharing the whole object and sharing scope lies specifying exactly
what to share, I'd think.
Here is one possible syntax, like regular function calls. Parameter types
can possibly be inferred and omitted:
void push(T value);
in {
out(length());
}
out(size_t oldLength) {
assert(value == top());
assert(length == oldLength + 1);
}
I think this could work. One of Walter's ideas was to pass the entire
old object as an argument to out. Passing handpicked data is more work
for the user but faster.
Perhaps this would simplify things a bit:
void push(T value);
in {
auto oldLength = length;
}
out(oldLength) {
assert(value == top());
assert(length == oldLength + 1);
}
Whatever parameters you pass to out they'd be matched by name with stuff
defined in the "in" contract. That poses a problem because until now
out(whatever) automatically passed the result to the out contract under
the name "whatever".
Andrei
Re: Communicating between in and out contracts
Andrei Alexandrescu wrote:
Consider a Stack interface:
interface Stack(T) {
bool empty();
ref T top();
void push(T value);
void pop();
size_t length();
}
Let's attach contracts to the interface:
interface Stack(T) {
bool empty();
ref T top()
in {
assert(!empty());
}
void push(T value);
out {
assert(value == top());
}
void pop()
in {
assert(!empty());
}
size_t length()
out(result) {
assert((result == 0) == empty());
}
}
So far so good. The problem is now that it's impossible to express the
contract "the length after push() is the length before plus 1."
Eiffel offers the "old" keyword that refers to the old object in a
postcondition. But it seems quite wasteful to clone the object just to
have a contract look at a little portion of the old object.
I was thinking of having the two contracts share the same scope. In that
case we can write:
void push(T value);
in {
auto oldLength = length();
}
out {
assert(value == top());
assert(length == oldLength + 1);
}
Walter tried to implement that but it turned out to be very difficult
implementation-wise. We tossed around a couple of other ideas, without
making much progress. In particular inlining the contract bodies looks
more attractive than it really is. If you have any suggestion, please
share.
Thanks,
Andrei
How hard would it be to do something like this: collect any local variables declared in
the precondition into a structure, and make that structure transparently available to the
postcondition. So your push case above gets rewritten to something like this:
__magic_tmp = {
typeof( length() ) oldLength;
}
in {
__magic_tmp.oldLength = length();
}
out {
assert(value == top());
assert(length == __magic_tmp.oldLength + 1);
}
Honestly Lutger's idea of passing the data like parameters might be better, I'm just
somehow uneasy about the look of "out(foo,bar)".
-- Chris Nicholson-Sauls
Re: Communicating between in and out contracts
Between sharing the whole object and sharing scope lies specifying exactly
what to share, I'd think.
Here is one possible syntax, like regular function calls. Parameter types
can possibly be inferred and omitted:
void push(T value);
in {
out(length());
}
out(size_t oldLength) {
assert(value == top());
assert(length == oldLength + 1);
}
Communicating between in and out contracts
Consider a Stack interface:
interface Stack(T) {
bool empty();
ref T top();
void push(T value);
void pop();
size_t length();
}
Let's attach contracts to the interface:
interface Stack(T) {
bool empty();
ref T top()
in {
assert(!empty());
}
void push(T value);
out {
assert(value == top());
}
void pop()
in {
assert(!empty());
}
size_t length()
out(result) {
assert((result == 0) == empty());
}
}
So far so good. The problem is now that it's impossible to express the
contract "the length after push() is the length before plus 1."
Eiffel offers the "old" keyword that refers to the old object in a
postcondition. But it seems quite wasteful to clone the object just to
have a contract look at a little portion of the old object.
I was thinking of having the two contracts share the same scope. In that
case we can write:
void push(T value);
in {
auto oldLength = length();
}
out {
assert(value == top());
assert(length == oldLength + 1);
}
Walter tried to implement that but it turned out to be very difficult
implementation-wise. We tossed around a couple of other ideas, without
making much progress. In particular inlining the contract bodies looks
more attractive than it really is. If you have any suggestion, please share.
Thanks,
Andrei
