On Sun, 18 Oct 2009 03:44:39 -0400, Rainer Deyke rain...@eldwood.com
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
On 2009-10-20 08:16:01 -0400, Steven Schveighoffer
schvei...@yahoo.com 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
On Tue, 20 Oct 2009 08:36:14 -0400, Michel Fortin
michel.for...@michelf.com wrote:
On 2009-10-20 08:16:01 -0400, Steven Schveighoffer
schvei...@yahoo.com said:
Incidentally, shouldn't all access to the object in the in contract be
const by default anyways?
Hum, access to everything
On 2009-10-20 11:44:00 -0400, Steven Schveighoffer
schvei...@yahoo.com said:
On Tue, 20 Oct 2009 08:36:14 -0400, Michel Fortin
michel.for...@michelf.com wrote:
On 2009-10-20 08:16:01 -0400, Steven Schveighoffer
schvei...@yahoo.com said:
Incidentally, shouldn't all access to the object
On Tue, 20 Oct 2009 11:57:05 -0400, Michel Fortin
michel.for...@michelf.com wrote:
On 2009-10-20 11:44:00 -0400, Steven Schveighoffer
schvei...@yahoo.com said:
On Tue, 20 Oct 2009 08:36:14 -0400, Michel Fortin
michel.for...@michelf.com wrote:
On 2009-10-20 08:16:01 -0400, Steven
On 2009-10-20 12:04:20 -0400, Steven Schveighoffer
schvei...@yahoo.com said:
On Tue, 20 Oct 2009 11:57:05 -0400, Michel Fortin
michel.for...@michelf.com wrote:
On 2009-10-20 11:44:00 -0400, Steven Schveighoffer
schvei...@yahoo.com said:
On Tue, 20 Oct 2009 08:36:14 -0400, Michel Fortin
On Tue, 20 Oct 2009 13:13:07 -0400, Michel Fortin
michel.for...@michelf.com 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
Steven Schveighoffer wrote:
On Tue, 20 Oct 2009 13:13:07 -0400, Michel Fortin
michel.for...@michelf.com 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
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'
Andrei Alexandrescu wrote:
Lutger wrote:
snip
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
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
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.
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.
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.
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
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
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
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
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,
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
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(); // --
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
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.
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
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
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
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
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
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
On Sat, 17 Oct 2009 00:22:54 +0400, Andrei Alexandrescu
seewebsiteforem...@erdani.org 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
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
seewebsiteforem...@erdani.org wrote:
Jason House wrote:
if fun or gun is impure, then they should not be callable by the
contracts. Because of that, order
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())
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 ..
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
seewebsiteforem...@erdani.org wrote:
Jason House wrote:
if fun or gun is
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
seewebsiteforem...@erdani.org wrote:
Jason House wrote:
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
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
seewebsiteforem...@erdani.org wrote:
Jason House wrote:
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
seewebsiteforem...@erdani.org wrote:
Jason
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.
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
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:
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 ==
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.
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
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) {
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 {
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
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
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 {
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
50 matches
Mail list logo
