Ada.Strings.Bounded
in [ADA]
|
From: Dmitry A. Kazakov on 14 Apr 2008 05:07 On Sun, 13 Apr 2008 16:20:24 -0700 (PDT), Eric Hughes wrote: > Why > shouldn't you derive from a universal type? Because it's not > implementable! One does not imply another. If you are aiming at Liskov substitutability principle, you should also remember how it is defined. It is in terms of *provable* propositions. Pragmatically, the program is correct even if there exist unreachable states where it could crash. However, LSP does not work anyway. > So I can now outline what the relationship ought to be: > -- The set of values of an implemented type is > a _subset_ of the terms of the universal type. Counterexample: NaN of Float. (The set of values of a derived type is neither subset or superset. It is a different set. There could be mappings defined between these two sets in order to achieve substitutability. Such mappings could be injective, or not) > -- The set of operators on an implemented type > _satisfy_ the axioms of the universal type. This cannot work because any implementation is necessarily a DFA. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de
From: Adam Beneschan on 14 Apr 2008 11:11 On Apr 12, 11:50 am, Eric Hughes <eric....(a)gmail.com> wrote: > On Apr 5, 3:43 am, Pascal Obry <pas...(a)obry.net> wrote: > > > What to do if we have Put_Line defined for String and > > Unbounded_String? Which version gets called? > > I know this answer is a bit heretical, but the answer I'd pick is > "either one". Non-deterministic execution, if you'd like the > technical term. Ooops, I must have stumbled into some other newsgroup---I thought I was in comp.lang.ada. -- Adam
From: Eric Hughes on 14 Apr 2008 11:25 On Apr 14, 2:00 am, "Dmitry A. Kazakov" <mail...(a)dmitry-kazakov.de> wrote: > If we had universal_string, it would have no assignment anyway, because all > universal objects are immutable. Sure, because you can't declare a variable of a universal type. But this critique misses the point, which is about the relationship of types that partially implement a universal type. > There is a difference between types and their constrained subtypes in terms > of substitutability. That's why the language has Constraint_Error defined. > The contracts extended by Constraint_Error aren't violated and everything > is fine. Sure, but again not the point. The relationship between a universal type and an implemented type is NOT the same as that between two implemented types. Eric
From: Eric Hughes on 14 Apr 2008 11:50 On Apr 14, 3:07 am, "Dmitry A. Kazakov" <mail...(a)dmitry-kazakov.de> wrote: > If you are aiming at Liskov substitutability > principle, But I'm not aiming for that. It's related, to be sure, but it's not the same. If you don't acknowledge that a universal type is a different creature than an ordinary type, then you would have to see only preexisting relationships. > > So I can now outline what the relationship ought to be: > > -- The set of values of an implemented type is > > a _subset_ of the terms of the universal type. > > Counterexample: NaN of Float. I take from what you're saying that the ordinary way of bringing floating point arithmetic into a language is not an implementation of universal Real numbers. That's true. We can talk about optimal encodings and less-than-optimal encodings, if you'd like, but I really don't see how the exceptional values of floating point numbers violate the spirit of the rule. NaN, but even more so overflow and underflow, even though they're defined for hardware implementations, could well be forbidden as accessible values from within the language. You clearly couldn't eliminate this kind of type from ordinary use soon, because it's well-embedded in practice and skills. The issue then becomes whether it would be beneficial to also have a Real-implementing type in the pattern I've mentioned. The differences would be small. Since a calculation that results in an exceptional value raises an exception, such a value that would otherwise be assigned is simply not assigned (or even made visible). I think that takes care of all the modification that would be needed. > The set of values of a derived type is neither subset or superset. It is a > different set. If you insist, but this is not derivation. > > -- The set of operators on an implemented type > > _satisfy_ the axioms of the universal type. > > This cannot work because any implementation is necessarily a DFA. ??? Eric
From: Eric Hughes on 14 Apr 2008 12:09
On Apr 14, 9:11 am, Adam Beneschan <a...(a)irvine.com> wrote: > Ooops, I must have stumbled into some other newsgroup---I thought I > was in comp.lang.ada. I did say "heresy". But the whole point of that discussion was to characterize when non-determinism would not break correctness. Eric |