Ada.Strings.Bounded
in [ADA]
|
From: Georg Bauhaus on 14 Apr 2008 14:13 Eric Hughes wrote: > 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. It might be worth noting that this kind of "correctness" specifically precludes factors that are essential to typical Ada programming: for a program to solve a problem correctly, use of time and storage must stay within specified bounds, too. Is there a definition of "correctness" that includes more than the necessary, static, computer agnostic precondition of "left side of equation equals right side of equation" no matter when and how?
From: Dmitry A. Kazakov on 14 Apr 2008 14:36 On Mon, 14 Apr 2008 08:25:41 -0700 (PDT), Eric Hughes wrote: > On Apr 14, 2:00 am, "Dmitry A. Kazakov" <mail...(a)dmitry-kazakov.de> > wrote: >> 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. Certainly, but I don't see why should we care about an non-implemented type. Well, an application dealing with mathematical objects might be interesting in modeling N, but it is not the language concern. The same way as Ada does not care about types of organic molecules... -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de
From: Dmitry A. Kazakov on 14 Apr 2008 14:52 On Mon, 14 Apr 2008 08:50:21 -0700 (PDT), Eric Hughes wrote: > 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. I think it is wrong to consider N and universal_integer equivalent. >>> 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. It is not a subset of R. Subseting is not a sufficient condition for a successful modeling. Actually it is the opposite, a perfect subset cannot be a good model. The best models of R aren't even close to subsets. For example intervals with rational bounds. >> 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. It makes life a lot easier. Otherwise you will need to introduce encodings, have to define the underlying bit patterns, and will never be able to abstract implementations. >>> -- 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. > > ??? Programs are DFA (except hardware interrupts etc). -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de
From: Eric Hughes on 14 Apr 2008 21:35 On Apr 14, 12:13 pm, Georg Bauhaus <rm.tsoh.plus- bug.bauh...(a)maps.futureapps.de> wrote: > It might be worth noting that this kind of "correctness" > specifically precludes factors that are essential to typical > Ada programming: for a program to solve a problem correctly, > use of time and storage must stay within specified bounds, too. > > Is there a definition of "correctness" that includes more than > the necessary, static, computer agnostic precondition > of "left side of equation equals right side of equation" no > matter when and how? Yes. To me, the quickest way of getting at the essence of such conditions is to start trying to write them down. You need symbols for that. You need a function symbol for, say, the time something takes and another for the space something takes. You need units of time and units of space for the results. You need literal expressions for durations of time and amounts of space to write down bounds. All these are analytical symbols that need not be part of the language they are analyzing. The traditional method of correctness uses only the symbols of a programming language combined with those of predicate calculus. Simply from lack of expressibility, this traditional method cannot directly address issues of time and space. You need to obtain those symbols from somewhere, and this pretty much means constructing an execution model that provides a place to root those symbols. Execution models, however, are properties of the target processor and execution environment, and thus outside of and, really, independent of the abstractions of high-level languages. So, to ground this in Ada, should there be a Ada-wide execution model? Probably not. Might there be someday a way of expressing an execution model in Ada? I would hope so. One of the consequences of this is that, in general, you can't prove performance predicates about a program by itself, but only together with an execution model. Admittedly most execution models are similar, but it would be a error of categories to assert a universal one. (I don't mean to say that a canonical one might not be useful.) There's a whole area of practical experience to gather about the similarities of such proof prior to standardization, and I wouldn't rush in quickly. Finally, in order for this to work, you have to be able to connect execution of the high-level program with execution of a program of equivalent effect in the execution model. This is where that Hoare paper that I mentioned a while back, "Proof of correctness of data representations" comes in. It describes exactly how this works. Eric
From: Eric Hughes on 14 Apr 2008 21:39
On Apr 14, 12:36 pm, "Dmitry A. Kazakov" <mail...(a)dmitry-kazakov.de> wrote: > Certainly, but I don't see why should we care about an non-implemented > type. Because they make better tools of thought. Assuming a prospective "- oid" morphism, universal types provide one half of a type description. Representation issues, such as number of bits in an integer, become an orthogonal issue. Separation of concerns is something Ada got right uniquely among programming languages, but there remain other kinds of concerns yet to separate. Eric |