Operation can be dispatching in only one type
in [ADA]
|
From: Georg Bauhaus on 8 Dec 2009 05:33 Dmitry A. Kazakov schrieb: > On Tue, 08 Dec 2009 11:06:54 +0100, Georg Bauhaus wrote: > >> Dmitry A. Kazakov schrieb: >>> In my view pre-/postconditions and >>> invariants should be static, used strictly for program correctness proofs. >>> Subtypes should complement them for dynamic run-time checks (recoverable >>> faults). >> Hm. What would be your subtype based expression for >> >> generic >> type E is private; >> package Stacks is >> >> type Stack is private; >> >> procedure push (Modified_Stack : in out Stack; >> Another : Element) >> with pre => not Full (Modified_Stack), >> post => Size (Modified_Stack'Exit) = Size (Modified_Stack); >> >> procedure pop (Modified_Stack : in out Stack) >> with pre => not Empty (Modified_Stack), >> post => Empty (Modified_Stack); > > None. The above is wrong. You cannot implement this contract (if we deduced > one from the given pre- and postconditions). Proof: > > loop > Push (Stack, X); > end loop; > > q.e.d. > > Therefore the contract of a stack must always contain ideals, e.g. > > 1. exceptions, like Full_Error, Empty_Error; I understand that exceptions are implied by Eiffel style conditions. The Eiffel camp might answer, for example, Lock (Stack); while not Full (Stack) loop Push (Stack, X); end loop; Unlock (Stack); q.e.d. > 2. blocked states, like holding the caller until the stack state is changed > from another task. Would you want this to be possible with Ada, or with SPARK? ;-) > > Pre- and psotconditions are to be used to prove a contract to hold. They > themselves are no contract. In Eiffel, pre post and inv are used to write a contract. The proof obligation rests on the programmer.
From: Dmitry A. Kazakov on 8 Dec 2009 05:49 On Tue, 08 Dec 2009 11:33:25 +0100, Georg Bauhaus wrote: > Dmitry A. Kazakov schrieb: >> On Tue, 08 Dec 2009 11:06:54 +0100, Georg Bauhaus wrote: >> >>> Dmitry A. Kazakov schrieb: >>>> In my view pre-/postconditions and >>>> invariants should be static, used strictly for program correctness proofs. >>>> Subtypes should complement them for dynamic run-time checks (recoverable >>>> faults). >>> Hm. What would be your subtype based expression for >>> >>> generic >>> type E is private; >>> package Stacks is >>> >>> type Stack is private; >>> >>> procedure push (Modified_Stack : in out Stack; >>> Another : Element) >>> with pre => not Full (Modified_Stack), >>> post => Size (Modified_Stack'Exit) = Size (Modified_Stack); >>> >>> procedure pop (Modified_Stack : in out Stack) >>> with pre => not Empty (Modified_Stack), >>> post => Empty (Modified_Stack); >> >> None. The above is wrong. You cannot implement this contract (if we deduced >> one from the given pre- and postconditions). Proof: >> >> loop >> Push (Stack, X); >> end loop; >> >> q.e.d. >> >> Therefore the contract of a stack must always contain ideals, e.g. >> >> 1. exceptions, like Full_Error, Empty_Error; > > I understand that exceptions are implied by Eiffel style > conditions. No, in that case the conditions should be: pre => true post => Size (Modified_Stack'Exit) = Size (Modified_Stack); or Full_Error Actually, the second part is more elaborated, it should also state that the stack was not modified, but you've got the idea. Ideals are postcondition things. >> 2. blocked states, like holding the caller until the stack state is changed >> from another task. > > Would you want this to be possible with Ada, or with SPARK? ;-) In what sense? Of course it is possible to implement in Ada using a protected object or a monitor task. >> Pre- and psotconditions are to be used to prove a contract to hold. They >> themselves are no contract. > > In Eiffel, pre post and inv are used to write a contract. > The proof obligation rests on the programmer. Yes, this is the core of the disagreement. If that rests on the programmer, then *-conditions are THE program. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de
From: Randy Brukardt on 9 Dec 2009 23:09 "Dmitry A. Kazakov" <mailbox(a)dmitry-kazakov.de> wrote in message news:c7bquicl77wg$.1lpuev0db0z46$.dlg(a)40tude.net... > On Tue, 8 Dec 2009 05:30:30 +0100, stefan-lucks(a)see-the.signature wrote: .... >> Isn't that essentially the same as the invariants in Eiffel? > > I see differences. Both Window_Type and Valid_Window_Type are visible. > Eiffel invariant deals with one type. Further the invariant is an > implementation detail normally invisible for the clients. Subtype is a > publicly declared constraint (contract). Right. We're actually considering both. We're almost certainly going to have invariants, on private types only, which are required to be checked only at the boundary of the defining package. (Such invariants can be abused, but they still more predicable than those on visible types.) Such invariants apply to all values of a type. Subtype predicates (for the lack of a better name, they're definitely *not* constraints, read AI05-0153-1 to see why) apply only to a view of a type, and would mainly be checked when a conversion to the subtype is done. (Almost everything interesting in Ada is technically a conversion to a subtype, so that covers the vast majority of interesting cases.) The current thinking is that using a subtype with a predicate in an array index, slice, entry family, and possibly some cases I forgot about would be illegal (or raise Program_Error in a generic body). We don't want to prevent the construction of subtypes like: subtype Odd_Integer is Integer with Predicate => Odd_Integer mod 2 = 1; but we sure don't want them in arrays. I'm not throughly convinced that this is the right approach, but more work needs to be done on the proposal in any case. Randy.
From: Robert A Duff on 10 Dec 2009 19:10 stefan-lucks(a)see-the.signature writes: > On Mon, 7 Dec 2009, Randy Brukardt wrote: > >> "Dmitry A. Kazakov" <mailbox(a)dmitry-kazakov.de> wrote in message > >> > Why not to allow such constraints for subtypes? E.g. >> > >> > subtype Valid_Window_Type is Window_Type when Is_Valid; >> > >> > then simply: >> > >> > procedure Do_Something (Window : Valid_Window_Type; ...) >> >> That's also under consideration, > > Great! Yes, it is great. I am a strong advocate of this feature. But there are a lot of details to work out, and the feature might not make it into the language by 2012. We'll see. > Isn't that essentially the same as the invariants in Eiffel? Yes, it's quite similar. But there are some important differences, such as the fact that in Eiffel, a class is both a type and a module, whereas in Ada, we have types, subtypes, and packages as separate concepts. >> but there are some problems with it. One >> problem is that such types are very confusing in array indexes/slices (do >> the values all participate or just the ones that pass the predicate?) I consider such problems to be side issues. They are solvable, I think. > One way to solve^H^H^H^H^H^H circumvent this problem would be to prohibit > that kind of subtyping for discrete types. In Dmity's example above, > Window_Type is likely to be a record (probably a tagged one). If it is not > a discrete type, you can't use it as an array index. :-) I don't like that "solution" (or "circumvention", if you prefer). ;-) I think one important goal is to be able to have arbitrary subtypes of an enumeration type, in addition to just subranges. I don't much care about arrays indexed by such subtypes. subtype Vowel is Character with Predicate => To_Lower(Vowel) in ('a', 'e', 'i', 'o', 'u'); or something like that. Here, Vowel refers to the current instance of subtype Vowel. I don't particularly want an array indexed by Vowel, but I might want to say: case C is when Vowel => ...; when Consonant => ...; when Punctuation => ...; ... or: procedure P(X : Vowel); or: if X in Vowel ... - Bob
From: Robert A Duff on 15 Dec 2009 18:54
stefan-lucks(a)see-the.signature writes: > On Tue, 1 Dec 2009, Dmitry A. Kazakov wrote: > >> On Tue, 1 Dec 2009 06:45:16 +0100, stefan-lucks(a)see-the.signature wrote: >> >> > On Tue, 1 Dec 2009, Dmitry A. Kazakov wrote: >> > >> >> On Mon, 30 Nov 2009 15:43:21 -0500, Robert A Duff wrote: >> > >> >>> Right. I think they should be equivalent. My solution is to use >> >>> two different symbols for (initial) assignment and (subsequent) >> >>> reassignment. >> >> >> >> But they cannot be, otherwise the semantics of ":=" would depend on the >> >> things done before: >> >> >> >> X : T; >> >> begin >> >> X := F (Y); -- Initialization >> > >> > No, at this point of time, X has been initialised to *some* value, even if >> > the value itself is undefined. So this is just a proper assignment. >> >> You should say that to Bob, because this is exactly my point. Bob, here. Sorry I didn't reply to many messages in this thread -- I don't follow this newsgroup every day. Too much real work to be done. ;-) More like every few months... I'm getting mixed up about arguments regarding semantics, versus arguments regarding terminology. Both are important. > No! > > You just moved to a different topic: > > [...] >> Initialization /= construction does not fit into this picture. > > The issue was > > initialisation /= assignment (*) Right. Ada distinguishes the two. But it uses the same syntax for both, which I think is confusing. Except we use "zee". Or "zed" if you prefer. ;-) Actually the Ada terminology is that "assignment" includes both: "initialization" and "assignment_statement". That's confusing. > and the fact that in Ada both look syntactically the same. You seem to be > the first to mention "construction" at all. > > BTW, I don't think initialisation and construction are actually identical, > even though they have to be performed in close temporal proximity. If > construction fails, this is a Storage_Error. A failed Initialisation is > much more powerful -- it can raise any of your favourite exceptions. ;-) More terminology confusion: Some folks think "construct" and "allocate storage" are synonymous. Other folks think "construct" and "initialize" are synonymous. Maybe in 100 years computer science will have terms everybody can agree on. In the mean time, we have "procedure", "function", "subprogram", "subroutine", "routine", "program", "method", etc. all of which mean more-or-less the same thing. Sigh. > --------- > Footnote: > (*) I prefer to avoid the word "reassignment", which Bob would use. Sigh. Several people have voted against my (clever? too clever?) "assign" vs. "reassign" terminology. I'm still not sure... - Bob |