Meaning of “contractual” according to Ada

Meaning of “contractual” according to Ada

[Yannick Duchêne (Hibou57)]

Because naming and wording matters, especially with Ada :-P , I have this  
question.

http://www.ada-auth.org/standards/12rat/html/Rat12-2-5.html
Says:
> These are not really contractual in the sense thatpreconditions,  
> postconditions and invariants arecontractual but are more akin to  
> constraints.

What's not contractual with subtype predicates? And so what does  
“contractual” means exactly for Ada's definition authors?


-- 
“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

Re: Meaning of “contractual” according to Ada

[Robert A Duff]

"Yannick DuchÔøΩne (Hibou57)" <yannick_duchene@yahoo.fr> writes:

> Because naming and wording matters, especially with Ada :-P , I have
> this  question.
>
> http://www.ada-auth.org/standards/12rat/html/Rat12-2-5.html
> Says:
>> These are not really contractual in the sense thatpreconditions,
>> postconditions and invariants arecontractual but are more akin to
>> constraints.
>
> What's not contractual with subtype predicates? And so what does
> ÔøΩcontractualÔøΩ means exactly for Ada's definition authors?

There's no Ada-specific meaning for "contractual".  You are quoting
the Rationale, not the RM.  ;-)

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.

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.  In fact,
if I could turn back the clock, I'd get rid of constraints,
and just use predicates.  And I'd call them "invariants".

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.

- Bob

Re: Meaning of “contractual” according to Ada

[Yannick Duchêne (Hibou57)]

Le Wed, 06 Mar 2013 23:35:54 +0100, Robert A Duff  
<bobduff@shell01.theworld.com> a écrit:

> "Yannick Duchêne (Hibou57)" <yannick_duchene@yahoo.fr> writes:
>
>> Because naming and wording matters, especially with Ada :-P , I have
>> this  question.
>>
>> http://www.ada-auth.org/standards/12rat/html/Rat12-2-5.html
>> Says:
>>> These are not really contractual in the sense thatpreconditions,
>>> postconditions and invariants arecontractual but are more akin to
>>> constraints.
>>
>> What's not contractual with subtype predicates? And so what does
>> “contractual” means exactly for Ada's definition authors?
>
> There's no Ada-specific meaning for "contractual".  You are quoting
> the Rationale, not the RM.  ;-)

Yes, I knew, I was just plain wrong referring to “Ada's definition  
authors” ;-)

> 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?

> 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

Re: Meaning of "contractual" according to Ada

[Randy Brukardt]

[-- 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 

Re: Meaning of “contractual” according to Ada

[Dmitry A. Kazakov]

On Thu, 07 Mar 2013 02:20:46 +0100, Yannick Duch�ne (Hibou57) wrote:

> Or may be constraints are just more general than contracts?

The reverse. Constraint is a specific type of contract which involves 1)
two related types, and 2) one type is a specialization of another.

Contract is much looser thing, not necessarily put on a type, e.g.
contracts of subprograms or modules.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de