Carl (>>), Damian (>):
>> class A {
>> method foo($x) {
>> PRE { $x < 10 }
>> # ...
>> }
>> }
>>
>> class B is A {
>> method foo($a, $b, $c) {
>> PRE { [>] $a, $b, $c }
>> # ...
>> }
>> }
>>
>> When C<B.foo> is called, are both C<PRE> blocks meant to be run?
>
> No. Contractual constraints are only inherited by methods of the
> same signature.
>
> BTW, that example isn't Liskov substitutable, so it really doesn't
> matter what it does under DbC. ;-)
Right. :-) I chose a non-Liskov-substitutable example to highlight how
much trouble we are in. Nowhere does the spec mention that Liskov
substitutability should be taken into account before DbC is
considered. The closest it gets is talking about "all the appropriate
per-method C<PRE> phasers", but it's up to the reader to infer what
those are. In other words, the spec isn't frozen solid there yet.
> Also, it would be much better if such cases issued a warning in Perl 6,
> rather than just silently hiding the inherited method and thereby
> breaking the shared polymorphic interface of the hierarchy.
We just discussed it briefly on #perl6. Signature smartmatching
(checking for signature compatibility) isn't computable in the general
case, due to C<where> clauses and subtypes. Which means that we could
presumably issue warnings for "well-behaved" signatures (a
sufficiently large class), but would have to remain silent for some
exotic ones.
>> A modest proposal: we already have excellent IoC primitives with
>> C<nextsame> et al. Why not let DBC fall out of their use instead of
>> trying to impose it from the outside? This poses no problems at all:
>
> Except for the problem that it doesn't actually implement DbC semantics. ;-)
>
> For example:
>
> class A {
> method foo($x) {
> PRE { $x < 10 }
> my $result = 2 * $x;
> return $result;
> POST { $result > $x }
> }
> }
>
> class B is A {
> method foo($x) {
> PRE { $x < 100 }
> callwith($c % 10);
> return -$c;
> }
> }
>
> In a proper DbC system, calling B::foo would always fail, since A::foo's
> inherited POST requires the method's result be greater than its original
> argument. But under the proposed new semantics, this example succeeds in
> returning a result that violates the inherited contract.
Aye.
I'd just like to point out, perhaps slightly redundantly, that the
above example wouldn't work (and can't work) under the imagined DbC
rules. The intent is clear: we'd like C<POST { $result > $x }> to run
at the end of C<B.foo>, checking that the result returned exceeds the
parameter C<$x>. But C<$result> isn't in C<B.foo>'s lexical scope, and
no matter how much pixie dust we sprinkle on it, it will never equal
the return value of another method. (The variable C<$result> is
suggestively named, but the compiler won't care.)
And opening the door to non-lexical semantics means selling sanity and
analyzability cheap. If C<POST { $result > $x }> is meant to somehow
find C<$result> in the wrong lexical scope, what about C<$x>? Is it
C<A.foo>'s or C<B.foo>'s C<$x>? The more one thinks about these
things, the less one feels an urge to cheat and be clever to get
proper semantics.
> Note that I'm *not* saying that Carl's example isn't demonstrating
> useful behaviour...just that the behaviour it's demonstrating isn't DbC.
Agreed.
> For a start, PRE- and POST- inheritance should only occur when a derived
> method does indeed have the same signature as some base method, and then
> only from that identically signatured method. Secondly, PREs have to be
> inherited disjunctively (i.e. be allowed to weaken), rather than being
> conjunctively accumulated (i.e. being forced to to strengthened).
No argument here. If the spec is already saying these things, it's not
being clear enough about them.
> However, I'd also want the spec to remove all reference to DbC when talking
> about PRE and POST. Or, better still, to state explicitly that PRE and
> POST do *not* have DbC semantics when applied to methods (perhaps even
> using some of the examples above to illustrate why not).
Sounds like a good idea all around.
> And if we are ever to properly supply DbC, then I think we'd also want
> to explicitly reserve--but not spec--the phaser names REQUIRE and ENSURE
> for possible later use (either in-core or via a future 'use contracts'
> pragma or module that some heroic soul may attempt write. ;-)
>
> On the other hand, because DbC "requires" and "ensures" are really
> much more like (inheritable) traits of a method's signature,
> rather than phasers tied to the method's block, it seems likely that
> any eventual DbC mechanism should not use phasers at all. So perhaps
> we ought to reserve the traits 'will require' and 'will ensure' so that the
> eventual DbC mechanism could be specified like so:
>
> class A {
> method foo(Num $x --> Num $result)
> will require { $x < 10 }
> will ensure { $result > $x }
> {
> return 2 * $x;
> }
> }
>
> class B is A {
> method foo(Num $x --> Num)
> will require { $x < 100 }
> {
> return $x+1;
> }
> }
>
> And, yes, this does indeed imply a syntax for optionally naming the
> return value in a signature (which syntax seems to fall out quite
> naturally in any case).
This all sounds exciting and worthwhile, and also more suitable a
place for DbC semantics: that is, not in absolute core, or not in Perl
6.0.0. Don't get me wrong, I'd still very much like to see/use
functionality like this, and definitely want to make room for it. But
it's not a blocker.
// Carl
