Operation can be dispatching in only one type
in [ADA]
|
From: stefan-lucks on 7 Dec 2009 23:30 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! Isn't that essentially the same as the invariants in Eiffel? > 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?) 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. :-) In any case, you definitively would not want to allow that kind of type for array indexes, if only the values which the predicate being true is allowed. How would you efficiently implement something like subtype Primes is Positive when Is_Prime; A: array (Primes (10_000 .. 20_000)) of T; -- 10_001 primality tests B: array (Primes (Start .. Stop)) of T; -- Start-Stop+1 such tests -- possibly at runtime > Another issue is that not all preconditions/postconditions can be written > this way. For one thing, a precondition can depend on multiple parameters at > once. Another issues is that the entry condition and exit conditions may be > different for a parameter. Right. That is precisely why Eiffel distinguishes preconditions, postconditions and invariants -- and supports all the three. -- ------ Stefan Lucks -- Bauhaus-University Weimar -- Germany ------ Stefan dot Lucks at uni minus weimar dot de ------ I love the taste of Cryptanalysis in the morning! ------
From: Dmitry A. Kazakov on 8 Dec 2009 04:12 On Tue, 8 Dec 2009 05:30:30 +0100, stefan-lucks(a)see-the.signature wrote: > 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! > > 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). >> 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?) > > 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. :-) Well, it would be nice not to limit this to only tagged types. > In any case, you definitively would not want to allow that kind of type > for array indexes, if only the values which the predicate being true is > allowed. How would you efficiently implement something like > > subtype Primes is Positive when Is_Prime; > A: array (Primes (10_000 .. 20_000)) of T; -- 10_001 primality tests I assume the above should be: A: array (Primes'Val (10_000) .. Primes'Val (20_000)) of T; > B: array (Primes (Start .. Stop)) of T; -- Start-Stop+1 such tests > -- possibly at runtime And this: B: array (Primes (Start) .. Primes (Stop)) of T; However the rules determining the subtype of the range are not clear. The main problem is that there is no range types and their subtype to clarify the issue: Positive'(1)..Positive'(2) is this positive range or Integer range? Same with above, if ranges fall back to the base type ranges, there will be no problem, but also the semantics of the declarations would change to: A: array (Integer (Primes'Val (10_000)) .. Integer (Primes'Val (20_000))) of T; This is the actual problem to me, not the performance issues. The programmer packing a DVD playback into the subtype constraint should know what he is doing. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de
From: Dmitry A. Kazakov on 8 Dec 2009 04:22 On Mon, 7 Dec 2009 18:19:11 -0600, Randy Brukardt wrote: > "Dmitry A. Kazakov" <mailbox(a)dmitry-kazakov.de> wrote in message > news:1gcigitaii0u0.1psu2vj52e66g$.dlg(a)40tude.net... >> On Fri, 4 Dec 2009 20:45:19 -0600, Randy Brukardt wrote: >> >>> Writing in Ada 2012 as proposed today >>> (and that might change before it gets standardized): >>> >>> procedure Do_Something (Window : Claw.Basic_Window_Type; ...) >>> with Pre => Is_Valid (Window); >> >> 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, 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?) Only ones of the subtype, obviously. But the problem is same as with the index sliding: when two subsets of the index are equivalent, either nominally (when elements are same) or structurally (when the number of elements is same + maybe other conditions). Structural equivalence might appear convenient, but it is always a source of confusion. > are a couple of others as well. > > Another issue is that not all preconditions/postconditions can be written > this way. For one thing, a precondition can depend on multiple parameters at > once. Another issues is that the entry condition and exit conditions may be > different for a parameter. For instance, from Claw: > > procedure Create (Window : Basic_Window_Type; ...) > with Pre => not Is_Valid (Window), > Post => Is_Valid (Window); Mutating [sub]type? That looks like a case for a constructor to me (an old discussion). > So subtypes cannot completely replace pre and post conditions, but they can > be a complement to them. Absolutely. However I consider it differently. 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). -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de
From: Georg Bauhaus on 8 Dec 2009 05:06 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);
From: Dmitry A. Kazakov on 8 Dec 2009 05:23
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; 2. blocked states, like holding the caller until the stack state is changed from another task. Pre- and psotconditions are to be used to prove a contract to hold. They themselves are no contract. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de |