* 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