Re: Meaning of "contractual" according to Ada

["Randy Brukardt" <randy@rrsoftware.com>]

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: Type: text/plain, Size: 2926 bytes --]

"Yannick Duch�ne (Hibou57)" <yannick_duchene@yahoo.fr> wrote in message 
news:op.wtjx0wq4ule2fv@cardamome...
Le Wed, 06 Mar 2013 23:35:54 +0100, Robert A Duff
<bobduff@shell01.theworld.com> a �crit:
...
>> If you have a formal parameter of subtype T, then T's predicate
>> forms part of the contract between the procedure body and its
>> callers.  So does T's constraint.  So I'd say predicates and
>> constraints are "contractual" in that sense.
>That's how I understand it too.
>
>> I think what John means is that predicates (like constraints)
>> can be used in cases like "X := Y + 1;" where there's no
>> clear boundary between abstractions, with a contract between
>> those abstractions.  It's just checking that Y+1 obeys the
>> constraints and predicates of X.
>
>> John is right that predicates are like constraints.
>Yes, and constraints are contracts. or not? Or may be constraints are just 
>more general than contracts?

With the previso that I'm interpreting Bob interpreting John, so I might be 
getting something wrong...

Bob is pointing out that "contracts" apply to profiles, as in subprogram 
profiles and generic profiles. The term is usually not used when talking 
about other sorts of things (like assignments and type conversions).

So, while a constraint or a predicate can be used in a contract (and in that 
case forms part of the contract), they also can be used in other contexts 
that aren't usually referred to as contracts. Which makes them broader than 
purely contracts.

Of course, this is all really natural language semantics more than anything 
that really matters. A compiler or analysis tool can use constraints and 
predicates in proofs whether or not they appear in things that are generally 
thought of as contracts.

Finally, I don't think it is smart to read the Rationale too closely. John 
is trying to explain this stuff so that everyone can understand, and 
sometimes it's the case that he doesn't understand it that well himself. 
(The blind leading the blind, if you will.) I've picked up some whoppers in 
the various drafts of the Rationale; those have been fixed, but I often see 
ones that I've missed upon re-reading some part of it (I sent John several 
pages of comments about the recently posted General chapter, which was 
extensively reviewed last fall).

                                                      Randy.


> We've got a bit of a mess:  5 or 6 kinds of constraint, "not null",
> predicates, and invariants, all of which are basically the same
> thing, with differences in minor details.  I'd prefer a language
> design that unified all those things.
Yes, unification of some other stuffs too would be nice :-P That's a job
for Ada's successor in 3045.


-- 
"Syntactic sugar causes cancer of the semi-colons." [1]
"Structured Programming supports the law of the excluded muddle." [1]
[1]: Epigrams on Programming - Alan J. - P. Yale University