Precondition visibility.

[Charles]

I agree with Nev's post here.

[hopscc]

OK Last try.

What you are both saying is that the 'requires' clause is a DbC contract/DbC precondition, acts as an interface and therefor must have this restriction/feature for all the reasons and examples given
and is solely and only be used for defining a DbC contract.

What I'm trying to point out (obviously badly) is that if you dont enforce this or dont enforce it strongly, as well as allowing it to be used as a DbC contract (all the fields accessed are as accessible as the member) in all its full and wondrous glory,
it can also be used for another purpose, which is as a general pre-entry checker, internal validity check on an objects state specific to the member call -
If used like this it is not a DbC contract/interface/... but a gating constraint for entering the method/validating the instance/.... ( just like a set of asserts)
Some or many of these item checks may well have contract constrained accessibility (checking arg values/ranges) but many will not.
Either use does not preclude the other.

and

This is a natural thing to do it seems both for people unfamiliar with dBC as implemented/described elsewhere as well as folks who are coming up to speed and/or totally familiar with the full gamut of its
range, capabilities and features.

The reason I say that with a fair degree of confidence is that if I look at the existing cobra compiler source there is a small but significant set of require clauses used in exactly that manner,
single or a few checks that validate internal non externally exposed state, checking values of internal non public fields on public methods.
This doesnt seem unreasonable to me (obviously) and presumably wasnt to the original writer.

It comes down to a difference between
"The requires clause is a DbC precondition (or DbC Contract)"
vs
"The requires clause may be used to provide a Dbc precondition/Contract or for validating args on internal less visible state prior to member entry"

The other thing I wanted to say was that while you can do the same thing with invariants ( that are invariant over the whole instance or method body(?) - not necessarily exactly what may be desired) and by asserts at the start of the method/member) it doesnt seem natural to do so (same example as above) In that the requires clause seems an obvious place to put all such prior entry checking separate from and not obscuring the early parts of the member implementation code.

which came from this

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.

If a requires clause can be solely and only a contract then yes perhaps, so but I'd suggest that if you change 'contract' above to 'requires clause' it does provide something: A place to put all your pre-entry guards away from implementation code (or declare your contracts) and there is no confusion - It seems the natural thing to do.

I probably should apologise too in that earlier I had been using precondition assuming it meant only 'set of conditions checked prior to something else'
- I hadnt realised that it has a more specific meaning (contract) wrt DbC. that possibly caused some confusion as to what I was saying

Nev thanks for that post explanation re DbC and about the reason for that visibility restriction - so callers can check conditions prior . I dont see that actually happening much but the capability is there.
I like the blame aspect - its obviously the callers fault a contract failed cos they didnt check for permission

[nevdelap]

the reason for that visibility restriction - so callers can check conditions prior . I dont see that actually happening much but the capability is there.

You're right, in practice you don't often do those checks explicitly, you write you code so that it just conforms to the preconditions - and if you mess it up you get swiftly told so - but importantly you do 'know' the preconditions of the methods in full, no grey areas, because they are right there for you, and they are executable, not in some comment or regular API doc.

And I understand what you are saying about wanting to built in test without being restricted - so that you can do loads of it - I love it, and I understand your feeling that the require is a neat place to put that, rather than having asserting at the beginning of the body, but in practice I put assertions all through things, beginning, middle, end. Why?

The thing is 'require' has the specific meaning in contracts of 'requiring something of the caller' and telling them what you require in executable code, rather than non-dbc generated old API docs or something. And this is as opposed to a class 'requiring something of itself' for correct operation, which is what you're getting at, and and is good built in test, but is different from the interface definition aspect, and is therefore not a 'require of the caller'.

And if you ask why I'd put assertions at the end of a method? Why not in the ensure? It's again that ensure is guaranteeing results to the caller, documenting them in the interface in executable form, and them being able to know exactly, no grey areas, what the method guarantees. It's not simply the class testing itself at the end of the method - a valid thing to do, just not in an ensure clause because it's not 'ensure for the caller'.

Think about it this way too - someone could re-implement your class from scratch, knowing the full specification of the interface, and their different implementation could have completely different asserts and a different invariant. Because that's the internal business. But to the caller it would be identical.

[Charles]

I wrote some of those crappy contracts back when I was still learning DbC. I'll be happy to correct them.

[hopscc]

Chuck, I thought you might say that which is to some extent another point.
If you did it while learning, with an incomplete knowledge of fully fledged DbC then it was done because it presumably was the most natural obvious thing to do at that stage of your learning
- its been sufficient for the purpose and gains no advantage ( for current uses) by exposing/rewriting or rearranging cos the rest of the contract utility ( check contract conditions/document contractual interface,/alternative implementation ) hasnt been done/isnt necessary for the purpose being addressed...

Full DbC hasnt exactly taken the programming world by storm and as we are finding there are shades of description, meaning and intended use suggested by existing implementation and doc that are not immediately apparent but may be eventually discovered by a disciplined practitioner by rigorous research and eventual practise. I'd submit thats not happening on a wide scale and one reason (beyond the std one of natural laziness/multiple calls on time on practitioners) is that its perhaps as an excessive effort (both learning the fine points and implementing) for the return and is beyond the current level of 'standard' need .
Things like that restriction both add to that ( both non obvious and non intuitive) and preclude the use for a more natural, obvious use ( for at least folks passing through the early parts of the use-quality-of-programming -constructs learning experience).

asserts/guards are perhaps a devt-101 level concept, fully fledged DbC contracts requirements/ins and outs are more a 305...
Can we make it possible to get (with some satisfaction) past the 101 learning level without getting smacked back.

Nev,
Unfairly I'm taking your first line as confirmation that the restriction is unnecessary - if noone (mostly) checks them then why bother enforcing the restrictionto allow them to be checked
In either case if you mess up you get told and all the conditions are executable, and presented both internal or externally accessible ( and all in one place).

Sure assertions go anywhere but I'm asserting the natural pace to put pre-entry checks/validations/non-dBC-meaning-preconditions is in the require clause when/if/as/because it is not being used for DbC contract.

Youre finely parsing meanings as to the definition of 'require' ( and later 'ensure') wrt where it requires them from, seen only through the definition of a DbC contract which I think I've already addressed when it is NOT being used for a full DbC contract + interfacing.
I point this out cos its obviously far to fine a distinction for most people to take up up early on in familiarising with full DbC (I didnt get that until explained and by example chuck didnt early on either).
For a new language 'require' can have whatever semantics we design/implement

The argument re whats allowable in 'ensure' shadows the discussion here with 'require' and is predicated again on require/ensure being used only and solely for a (canonical eiffel-like ?) DbC construct rather than allowed to be a little less doctrinaire.

The reimplementation point is a perhaps a reasonable one but but spurious I think - At this point I'd live with existing implementations being robustly healthy and as a way of supporting that making it very easy for a writer to add whatever (conditions) they like wherever it requires the least consideration for them to do so...

Enough I think - I've had my say and I think you should both see the point by now.

[hopscc]

Pox - cant help myself, Forgot to say this
Chuck - while they might be crappy contracts they are absolutely excellent pre-entry validation checks

[nevdelap]

These are from Microsoft pages - not Eiffel pages. Microsoft Code Contracts are DBC and if Microsoft aren't reinventing and twisting things just to make them Microsofty there must be good reasons.

All members that are mentioned in preconditions must be at least as accessible as the method itself; otherwise, the precondition might not be understood by all callers of a method.

Visibility - All members mentioned in a contract must be at least as visible as the method in which they appear. For example, a private field cannot be mentioned in a precondition for a public method; clients cannot validate such a contract before they call the method.

Precondition visibility: Preconditions specify the conditions a caller should establish prior to calling a method. Because of this, preconditions must be visible to the caller in the sense that the caller should be able to determine if he/she satisfies the preconditions. Thus, preconditions should not refer to internal state that the caller cannot access. Debug.Assert on the other hand can be used to specify internal consistency. Use Contract.Requires for preconditions so humans and tools can identify the condition as a method contract, rather than an internal consistency check.

The rest can be skipped by anyone not interested in the arguing...

in practice you don't often do those checks explicitly, you write you code so that it just conforms to the preconditions - and if you mess it up you get swiftly told so - but importantly you do 'know' the preconditions of the methods in full, no grey areas, because they are right there for you

if noone (mostly) checks them then why bother enforcing the restrictionto allow them to be checked

1/ You can't "code so that it just conforms to the preconditions" if you don't know what the preconditions are.
2/ For the same reason you bother having nilable and non-nilable types in Cobra. It's better to specify what you want and have the compiler enforce it, than to not know, innocently F-up, and have to figure out why after the fact because things are throwing exceptions at you, that could have easily been avoided.

Why DBC hasn't until recently taken off is that IMHO it forces you to do things right, and most programmers don't want engineering rigor because they are either too lazy, don't understand it, want freedom to sculpt their creations, or think that designing, implementing, and testing things properly takes too long, and many other reasons that make me glad airplanes aren't built like a lot of software is built.

What seems more natural to someone when they are learning something and don't fully understand it and are using it wrong is hardly a guiding principle for implementation.

And if the compiler doesn't make someone do it right when it can, and they don't have time or inclination to learn how to do it right, they will either never do it right or will do it wrong for a long time until finally figuring it out, if they ever do.

All that can be avoided by the compiler doing it right. If you don't think it's right I'm not going to argue, I'd just suggest learning a lot more about it.

If Cobra implemented a better version of DBC then awesome, but if Cobra implemented a broken version of DBC it would seriously hurt it's credibility. For starters if you wanted to redefine what 'require' and 'ensure' mean you'd stop saying that Cobra includes Contracts.