[Issue 6857] Precondition contract checks should be statically bound.

[d-bugmail at puremagic.com]

http://d.puremagic.com/issues/show_bug.cgi?id=6857



--- Comment #85 from Andrei Alexandrescu <andrei at metalanguage.com> 2012-09-05 07:26:07 PDT ---
I've had the opportunity to discuss the matter with Bertrand Meyer himself and
with a graduate student of his. Bertrand didn't have a defined answer offhand,
but opined that the static contract should be evaluated. His book says the same
.

Julian Tschannen (who allowed me to share his name here) wrote me the
following:

=========
1. Eiffel ECMA standard ([1], Rule 8.23.26) says, that the contract of
the dynamic type is checked, i.e. "pre_A OR ELSE pre_B"
(combined precondition, [1], Rule 8.10.5).

2. The Eiffel runtime does actually that, first checks the
precondition of the parent class A, and then the precondition
of the subclass B.

My take on the issue:
Dynamically it runs of course without a problem. If you would have a
static checker (e.g. the AutoProof tool that I am developing), the
code would be rejected due to the static check. Since we strive to get
a language that is statically checked and fully verified, it would
probably make more sense to just check the precondition of the static
type and not take the dynamic type into account for precondition
checks, since the client code works just with the given example and is
not correct for all possible arguments.
Or to be more precise, you could take all the static information into
account, but only the static information. It would for example be
possible that the client code has some precondition that would make
sure that the code is statically correct, even if the call - when
looked at in isolation - is statically not correct.
=========

So we currently do what the Eiffel standard and compiler do, but not what would
probably be the most sensible thing. In my opinion we should do the right thing
and check the contract statically.

-- 
Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email
------- You are receiving this mail because: -------