* Meaning of “contractual” according to Ada
@ 2013-03-06 18:22 Yannick Duchêne (Hibou57)
2013-03-06 22:35 ` Robert A Duff
0 siblings, 1 reply; 5+ messages in thread
From: Yannick Duchêne (Hibou57) @ 2013-03-06 18:22 UTC (permalink / raw)
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
^ permalink raw reply [flat|nested] 5+ messages in thread
* Re: Meaning of “contractual” according to Ada
2013-03-06 18:22 Meaning of “contractual” according to Ada Yannick Duchêne (Hibou57)
@ 2013-03-06 22:35 ` Robert A Duff
2013-03-07 1:20 ` Yannick Duchêne (Hibou57)
0 siblings, 1 reply; 5+ messages in thread
From: Robert A Duff @ 2013-03-06 22:35 UTC (permalink / raw)
"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
^ permalink raw reply [flat|nested] 5+ messages in thread
* Re: Meaning of “contractual” according to Ada
2013-03-06 22:35 ` Robert A Duff
@ 2013-03-07 1:20 ` Yannick Duchêne (Hibou57)
2013-03-07 2:57 ` Meaning of "contractual" " Randy Brukardt
2013-03-07 9:27 ` Meaning of “contractual” " Dmitry A. Kazakov
0 siblings, 2 replies; 5+ messages in thread
From: Yannick Duchêne (Hibou57) @ 2013-03-07 1:20 UTC (permalink / raw)
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
^ permalink raw reply [flat|nested] 5+ messages in thread
* Re: Meaning of "contractual" according to Ada
2013-03-07 1:20 ` Yannick Duchêne (Hibou57)
@ 2013-03-07 2:57 ` Randy Brukardt
2013-03-07 9:27 ` Meaning of “contractual” " Dmitry A. Kazakov
1 sibling, 0 replies; 5+ messages in thread
From: Randy Brukardt @ 2013-03-07 2:57 UTC (permalink / raw)
[-- 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
^ permalink raw reply [flat|nested] 5+ messages in thread
* Re: Meaning of “contractual” according to Ada
2013-03-07 1:20 ` Yannick Duchêne (Hibou57)
2013-03-07 2:57 ` Meaning of "contractual" " Randy Brukardt
@ 2013-03-07 9:27 ` Dmitry A. Kazakov
1 sibling, 0 replies; 5+ messages in thread
From: Dmitry A. Kazakov @ 2013-03-07 9:27 UTC (permalink / raw)
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
^ permalink raw reply [flat|nested] 5+ messages in thread
end of thread, other threads:[~2013-03-07 9:27 UTC | newest]
Thread overview: 5+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2013-03-06 18:22 Meaning of “contractual” according to Ada Yannick Duchêne (Hibou57)
2013-03-06 22:35 ` Robert A Duff
2013-03-07 1:20 ` Yannick Duchêne (Hibou57)
2013-03-07 2:57 ` Meaning of "contractual" " Randy Brukardt
2013-03-07 9:27 ` Meaning of “contractual” " Dmitry A. Kazakov
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox