Ada.Strings.Bounded
in [ADA]
|
From: Dmitry A. Kazakov on 15 Apr 2008 11:23 On Tue, 15 Apr 2008 07:20:15 -0700 (PDT), Eric Hughes wrote: > Perhaps you could explain what you want universal_integer to be. Merely the type of a static numeric expression. Well, it isn't, a counterexample is: A'Length (ARM 3.6.2) Universal_Integer is not necessarily Root_Integer, but somewhere close to the root of Root_Integer'Class. > If you can show me a Ada definition that can store a > universal_integer, only then will I believe you that it's the kind of > type that's just like an ordinary Ada type. type T is abstract private; Can you store T? -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de
From: Georg Bauhaus on 15 Apr 2008 16:33 Eric Hughes wrote: > 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. Thanks for the title. I see that some methods are actually heading in this direction. Hopefully, the basic idea that data and timing must be formally correct, too, finds its way into education.
From: Eric Hughes on 15 Apr 2008 22:46 On Tue, 15 Apr 2008 06:56:57 -0700 (PDT), Eric Hughes wrote: > I assert that that Ada as currently defined has no bound on the size > of numbers within universal_integer. On Apr 15, 8:58 am, "Dmitry A. Kazakov" <mail...(a)dmitry-kazakov.de> wrote: > It specifies the lower bound and leaves the upper bound up to the vendor. > Which by no means imply that there were no upper bound. That's an upper bound for a compiler, not for "Ada as currently defined". Please check my language carefully. > Moreover, > because the number of all instances of all existed, existing and future Ada > compilers is obviously finite, there also exists the upper bound of > universal_integer as a whole. "All compilers that were, all that are, and all that will ever be"-- these are not part of the Ada language definition. My assertion stands. I would still like to know what you think universal_integer actually is. Eric
From: Eric Hughes on 15 Apr 2008 22:51 On Tue, 15 Apr 2008 07:20:15 -0700 (PDT), Eric Hughes wrote: > Perhaps you could explain what you want universal_integer to be. On Apr 15, 9:23 am, "Dmitry A. Kazakov" <mail...(a)dmitry-kazakov.de> wrote: > Merely the type of a static numeric expression. Well, it isn't, a > counterexample is: > > A'Length (ARM 3.6.2) The fact that lengths are limited does not mean that their values cannot sit within a type whose values are not. The set of possible values of lengths for a certain compiler are a subset of the values of universal_integer. > Universal_Integer is not necessarily Root_Integer, but somewhere close to > the root of Root_Integer'Class. "Somewhere close" is not a definition. Please be more specific. > > If you can show me a Ada definition that can store a > > universal_integer, only then will I believe you that it's the kind of > > type that's just like an ordinary Ada type. > > type T is abstract private; > > Can you store T? By ordinary type, I mean the kind that's assignable, not abstract, not an interface, something you can declare a variable of. Eric
From: Eric Hughes on 15 Apr 2008 23:11
Eric Hughes wrote: > 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. On Apr 15, 2:33 pm, Georg Bauhaus <rm.tsoh.plus- bug.bauh...(a)maps.futureapps.de> wrote: > Thanks for the title. I see that some methods are actually > heading in this direction. Hopefully, the basic idea that > data and timing must be formally correct, too, finds its way > into education. You're welcome. That essay is collected in the book _Essays in Computing Science_. The title of that essay might well have been titled "Proof of correctness of compiler output", but Hoare doesn't go into compilation issues as such in enough depth to justify such a title. You'd have a program annotated with some properties and their proof, a compiler that converted the proof to one in its execution model, and proof- carrying object code as its output. Even if the proof annotations of the program were empty (as today), you can still infer some basic semantics from expressions and statements by themselves and generate checkable proof. I suspect that discipline would get rid of a lot of code generation defects. Eric |