Precondition visibility.

[nevdelap]

Hi Chuck,

DBC says "members used in preconditions to x must be at least a visible as x", ie visible to and testable by clients so that they can (at least theoretically, if not explicitly) guarantee that they fulfill their contracts, (and in fact know the conditions of the contract).

Currently the compiler doesn't enforce that at compile time.

Just wondering if that's deliberate, or for technical reasons, or that you've got a million other things to do, or...?

Cheers.

class A

    var __lame as int is private

    cue init
        base.init
        __lame = #[something secretly computed inside A]

    def meth
        require
            __lame == 1
        body
            print "hello"

class P

    def main
        a = A()
        a.meth

[nevdelap]

BTW, I basically just ask so that if it was appropriate I could make a ticket just so that it doesn't get overlooked.

[Charles]

Just a million things to do. Thanks for bringing it up. Ticket, please.

[hopscc]

If I understand the point correctly what that will cause is that if you want/need to ascertain private internal state as a prerequisite check to executing a method you
will be unable to do it in a precondition/require clause and will instead have to do it as an assertion early in the method...

While it might not be DBC ( as defined somewhere ) Is that restriction necessary ?

What is being improved by limiting where checks on internal state can be placed ?

I admittedly dont know anything about DBC in action but
I would have thought that an (invisible? assumed) precondition for any contract would always include that the object being acted on was in a valid receptive state to be acted on so
anything that checked/enforced that would be reasonable.

Is this an entangledment in semantic differences between DBC precondition contracts (wrt external consumers) and a more general concept of preconditions (for both the Object being acted on and the message/info about the action to be done) ??

[Charles]

It has to do with the fact that the contracts are considered part of the interface of the method. In fact, they should be showing up in the -doc output (but -doc is not complete).

Of course, in the body/implementation you can always do whatever you want including throwing an exception every time or having an infinite loop. Can't really control that and don't think I would want to.

[hopscc]

OK - so dont call it a contract ( as defined by ?? eiffel ??)
Call it a (general set of ) precondition(s) that you may choose to limit to the (also) externally accessible tests that define an interfacing contract.


i.e it can be a contract ( in the DBC sense) if you want to restrict the conditions to that or it can be a set of any general validating/gating conditions - up to the developer/user.

a cobra-contract that is a super set of the allowable DBC contract.

[Charles]

Sorry, no. The contract being an interface is an integral aspect of being a contract. And what kind of contract would have secret clauses that subscribers to the contract don't know about?

It goes even deeper. Subclassed methods inherit their base classes and therefore the contracts of the base method. Requirements can be weakened (boolean or) and guarantees (ensure) can be strengthened (boolean and).

Read Eiffel tutorials and docs until it clicks. I think they got it right.

The only difference is the treatment of contract failures in Cobra vs. Eiffel, but I'm too tired to go into that right now.

[hopscc]

Thats what I'm saying
Dont force it to be only a (eiffel) Contract , allow it to be that (and/or more if desired ( Contract and internals state precondition verification))

Re the secret clauses question:
As I said , It seems to me that all Contracts have a secret assumption/clauses anyway - that the receiving object is in a valid state and receptive to the request.
not limiting the accessibility allows that to be explicitly specified in the prerequirements clause....

Maybe theres two things here were referencing with the same name
- A contract that the callee wants enforced on both itself and the caller (internal state verification and externally accessable state and caller constraints) and
- A Contract that the callee provides/exposes to its callers (externally accessible state and caller constraints only) as an interfacing gateway.

[Charles]

Thats what I'm saying
Dont force it to be only a (eiffel) Contract , allow it to be that (and/or more if desired ( Contract and internals state precondition verification))

I understand that's what you're saying. I'm saying that it's not an issue of just shifting definitions around. The idea of a secret contract is a bad idea. Your phrase "that the receiving object is in a valid state and receptive to the request" is something that should be pushed to a visible contract.

Allowing a protected member to be referenced in the contract of a public method doesn't provide anything over putting such things in the method implementation--except maybe confusion.

[nevdelap]

Hi hopscc

Conditions that must be valid for the object to be in a valid state during execution are in the invariant, and can be in state invariants and loop invariants, and can be expressed as built in test as assertions in the body, which is executable test and documents the internals of the class - ie: is not part of the interface, is not of concern to the client, because if it fails it is a bug in the class.

If you want some internal state to be a precondition to executing a method it is simple - you have to expose it.

For example, if, for some reason, you have a stack with a limited size and you must only push onto a stack that is not full then you have to expose an isFull property and put in the preconditions not isFull (there are other possibilities that amount to the same thing). It can't just blow up, you can't expect the client to read your implementation, and you can't expect the client to read in the API doco don't push on a full stack and keep track of it themselves.

If the client cannot know what the precondition is then the precondition is not any type of precondition, not just not a DBC precondition, or not an Eiffel precondition.

It's simple - if an assertion in the body, an ensure, or an invariant fails it is the class's fault. If a precondition fails it is the callers fault. Is very clear cut. The finger is pointed where the responsibility lies.

There are plenty of references in Eiffel and in Microsoft Code Contracts on the web, and it is not just arbitrary Eiffel "contract's", it is a very coherent set of principles. Microsoft hasn't invented anything new here, even though they like to pretend they have. But it rocks that their weight is behind it now. It's also cool that Cobra's implementation is much better than Microsoft's "language agnostic" version - IMHO.