[28093] in Perl-Users-Digest
Perl-Users Digest, Issue: 9457 Volume: 10
daemon@ATHENA.MIT.EDU (Perl-Users Digest)
Wed Jul 12 14:15:14 2006
Date: Wed, 12 Jul 2006 11:15:08 -0700 (PDT)
From: Perl-Users Digest <Perl-Users-Request@ruby.OCE.ORST.EDU>
To: Perl-Users@ruby.OCE.ORST.EDU (Perl-Users Digest)
Perl-Users Digest Wed, 12 Jul 2006 Volume: 10 Number: 9457
Today's topics:
Re: What is a type error? <marshall.spight@gmail.com>
Re: What is a type error? <marshall.spight@gmail.com>
Re: What is a type error? <dnew@san.rr.com>
Re: What is a type error? <jo@durchholz.org>
Re: What is a type error? <jo@durchholz.org>
Digest Administrivia (Last modified: 6 Apr 01) (Perl-Users-Digest Admin)
----------------------------------------------------------------------
Date: 12 Jul 2006 09:24:10 -0700
From: "Marshall" <marshall.spight@gmail.com>
Subject: Re: What is a type error?
Message-Id: <1152721450.433219.269270@s13g2000cwa.googlegroups.com>
Joachim Durchholz wrote:
> Darren New schrieb:
> > As far as I understand it, Eiffel compilers don't even make use of
> > postconditions to optimize code or eliminate run-time checks (like null
> > pointer testing).
>
> That's correct.
>
> I think a large part of the reasons why this isn't done is that Eiffel's
> semantics is (a) too complicated (it's an imperative language after
> all), and (b) not formalized, which makes it difficult to assess what
> optimizations are safe and what aren't.
I can see the lack of a formal model being an issue, but is the
imperative bit really all that much of an obstacle? How hard
is it really to deal with assignment? Or does the issue have
more to do with pointers, aliasing, etc.?
Marshall
------------------------------
Date: 12 Jul 2006 09:38:29 -0700
From: "Marshall" <marshall.spight@gmail.com>
Subject: Re: What is a type error?
Message-Id: <1152722309.801960.18090@s13g2000cwa.googlegroups.com>
Joachim Durchholz wrote:
> Marshall schrieb:
>
> > I can certainly see how DbC would be useful without subtyping.
> > But would there still be a reason to separate preconditions
> > from postconditions? I've never been clear on the point
> > of differentiating them (beyond the fact that one's covariant
> > and the other is contravariant.)
>
> There is indeed.
> The rules about covariance and contravariance are just consequences of
> the notion of having a subtype (albeit important ones when it comes to
> designing concrete interfaces).
>
> For example, if a precondition fails, something is wrong about the
> things that the subroutine assumes about its environment, so it
> shouldn't have been called. This means the error is in the caller, not
> in the subroutine that carries the precondition.
>
> The less important consequence is that this should be reflected in the
> error messages.
>
> The more important consequences apply when integrating software.
> If you have a well-tested library, it makes sense to switch off
> postcondition checking for the library routines, but not their
> precondition checking.
> This applies not just for run-time checking: Ideally, with compile-time
> inference, all postconditions can be inferred from the function's
> preconditions and their code. The results of that inference can easily
> be stored in the precompiled libraries.
> Preconditions, on the other hand, can only be verified by checking all
> places where the functions are called.
Interesting!
So, what exactly separates a precondition from a postcondition
from an invariant? I have always imagined that one writes
assertions on parameters and return values, and those
assertions that only reference parameters were preconditions
and those which also referenced return values were postconditions.
Wouldn't that be easy enough to determine automatically?
And what's an invariant anyway?
Marshall
------------------------------
Date: Wed, 12 Jul 2006 17:38:18 GMT
From: Darren New <dnew@san.rr.com>
Subject: Re: What is a type error?
Message-Id: <esatg.14243$MF6.2444@tornado.socal.rr.com>
Marshall wrote:
> So, what exactly separates a precondition from a postcondition
> from an invariant?
A precondition applies to a routine/method/function and states the
conditions under which a function might be called. For example, a
precondition on "stack.pop" might be "not stack.empty", and
"socket.read" might have a precondition of "socket.is_open", and
"socket.open_a_new_connection" might have a precondition of
"socket.is_closed".
A postcondition applies to a routine/method/function and states (at
least part of) what that routine guarantees to be true when it returns,
assuming it is called with true preconditions. So "not stack.empty"
would be a postcondition of "stack.push". If your postconditions are
complete, they tell you what the routine does.
An invariant is something that applies to an entire object instance, any
time after the constructor has completed and no routine within that
instance is running (i.e., you're not in the middle of a call). There
should probably be something in there about destructors, too. So an
invariant might be "stack.is_empty == (stack.size == 0)" or perhaps
"socket.is_open implies (socket.buffer != null)" or some such.
The first problem with many of these sorts of things are that in
practice, there are lots of postconditions that are difficult to express
in any machine-readable way. The postcondition of "socket.read" is that
the buffer passed as the first argument has valid data in the first "n"
bytes, where "n" is the return value from "socket.read", unless
"socket.read" returned -1. What does "valid" mean there? It has to
match the bytes sent by some other process, possibly on another machine,
disregarding the bytes already read.
You can see how this can be hard to formalize in any particularly useful
way, unless you wind up modelling the whole universe, which is what most
of the really formalized network description techniques do.
Plus, of course, without having preconditions and postconditions for OS
calls, it's difficult to do much formally with that sort of thing.
You can imagine all sorts of I/O that would be difficult to describe,
even for things that are all in memory: what would be the postcondition
for "screen.draw_polygon"? Any set of postconditions on that routine
that don't mention that a polygon is now visible on the screen would be
difficult to take seriously.
There are also problems with the complexity of things. Imagine a
chess-playing game trying to describe the "generate moves" routine.
Precondition: An input board with a valid configuration of chess pieces.
Postcondition: An array of boards with possible next moves for the
selected team. Heck, if you could write those as assertions, you
wouldn't need the code.
--
Darren New / San Diego, CA, USA (PST)
This octopus isn't tasty. Too many
tentacles, not enough chops.
------------------------------
Date: Wed, 12 Jul 2006 19:52:43 +0200
From: Joachim Durchholz <jo@durchholz.org>
To: Marshall <marshall.spight@gmail.com>
Subject: Re: What is a type error?
Message-Id: <44B536EB.6020308@durchholz.org>
Marshall schrieb:
> I can see the lack of a formal model being an issue, but is the
> imperative bit really all that much of an obstacle? How hard
> is it really to deal with assignment? Or does the issue have
> more to do with pointers, aliasing, etc.?
Actually aliasing is *the* hard issue.
Just one data point: C compiler designers spend substantial effort to
determine which data structures cannot have aliasing to be able to apply
optimizations.
This can bite even with runtime assertion checking.
For example, ordinarily one would think that if there's only a fixed set
of routines that may modify some data structure A, checking the
invariants of that structure need only be done at the exit of these
routines.
Now assume that A has a reference to structure B, and that the
invariants involve B in some way. (E.g. A.count = A->B.count.)
There's still no problem with that - until you have a routine that
exports a reference to B, which gets accessed from elsewhere, say via C.
Now if I do
C->B.count = 27
I will most likely break A's invariant. If that assignment is in some
code that's far away from the code for A, debugging can become
exceedingly hard: the inconsistency (i.e. A violating its invariant) can
live for the entire runtime of the program.
So that innocent optimization "don't check all the program's invariants
after every assignment" immediately breaks with assignment (unless you
do some aliasing analysis).
In an OO language, it's even more difficult to establish that some data
structure cannot be aliased: even if the code for A doesn't hand out a
reference to B, there's no guarantee that some subclass of A doesn't.
I.e. the aliasing analysis has to be repeated whenever there's a new
subclass, which may happen at link time when you'd ordinarily don't want
to do any serious semantic analysis anymore.
There's another way around getting destroyed invariants reported at the
time the breakage occurs: lock any data field that goes into an
invariant (or a postcondition, too). The rationale behind this is that
from the perspective of assertions, an alias walks, smells and quacks
just like concurrent access, so locking would be the appropriate answer.
The problem here is that this means that updates can induce *very*
expensive machinery - imagine an invariant that says "A->balance is the
sum of all the transaction->amount fields in the transaction list of A",
it would cause all these ->amount fields to be locked as soon as a
transaction list is hooked up with the amount. OTOH one could argue that
such a locking simply makes cost in terms of debugging time visible as
runtime overhead, which isn't entirely a Bad Thing.
There are all other kinds of things that break in the presence of
aliasing; this is just the one that I happen to know best :-)
Without mutation, such breakage cannot occur. Invariants are just the
common postconditions of all the routines that may construct a structure
of a given type.
Regards,
Jo
------------------------------
Date: Wed, 12 Jul 2006 19:59:40 +0200
From: Joachim Durchholz <jo@durchholz.org>
Subject: Re: What is a type error?
Message-Id: <e93djg$9tl$1@online.de>
Marshall schrieb:
> So, what exactly separates a precondition from a postcondition
> from an invariant? I have always imagined that one writes
> assertions on parameters and return values, and those
> assertions that only reference parameters were preconditions
> and those which also referenced return values were postconditions.
> Wouldn't that be easy enough to determine automatically?
Sure.
Actually this can be done in an even simpler fashion; e.g. in Eiffel, it
is (forgive me if I got the details wrong, it's been several years since
I last coded in it):
foo (params): result_type is
require
-- list of assertions; these become preconditions
do
-- subroutine body
ensure
-- list of assertions; these become postconditions
end
> And what's an invariant anyway?
In general, it's a postcondition to all routines that create or modify a
data structure of a given type.
Eiffel does an additional check at routine entry, but that's just a
last-ditch line of defense against invariant destruction via aliases,
not a conceptual thing. Keep aliases under control via modes (i.e.
"unaliasable" marks on local data to prevent aliases from leaving the
scope of the data structure), or via locking, or simply by disallowing
destructive updates, and you don't need the checks at routine entry anymore.
Regards,
Jo
------------------------------
Date: 6 Apr 2001 21:33:47 GMT (Last modified)
From: Perl-Users-Request@ruby.oce.orst.edu (Perl-Users-Digest Admin)
Subject: Digest Administrivia (Last modified: 6 Apr 01)
Message-Id: <null>
Administrivia:
#The Perl-Users Digest is a retransmission of the USENET newsgroup
#comp.lang.perl.misc. For subscription or unsubscription requests, send
#the single line:
#
# subscribe perl-users
#or:
# unsubscribe perl-users
#
#to almanac@ruby.oce.orst.edu.
NOTE: due to the current flood of worm email banging on ruby, the smtp
server on ruby has been shut off until further notice.
To submit articles to comp.lang.perl.announce, send your article to
clpa@perl.com.
#To request back copies (available for a week or so), send your request
#to almanac@ruby.oce.orst.edu with the command "send perl-users x.y",
#where x is the volume number and y is the issue number.
#For other requests pertaining to the digest, send mail to
#perl-users-request@ruby.oce.orst.edu. Do not waste your time or mine
#sending perl questions to the -request address, I don't have time to
#answer them even if I did know the answer.
------------------------------
End of Perl-Users Digest V10 Issue 9457
***************************************
