From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-0.8 required=5.0 tests=BAYES_00,INVALID_DATE autolearn=no autolearn_force=no version=3.4.4 Path: utzoo!attcan!uunet!husc6!bloom-beacon!apple!bionet!agate!ucbvax!grebyn.com!karl From: karl@grebyn.com (Karl Nyberg) Newsgroups: comp.lang.ada Subject: Unpredictable Ada Message-ID: <8811251708.AA07137@grebyn.com> Date: 25 Nov 88 17:08:25 GMT Sender: daemon@ucbvax.BERKELEY.EDU Organization: Grebyn Corporation List-Id: [Ed - This, like a lot of things lately, seems to have fallen through the info-ada cracks...] >From haven!CLI.COM!mksmith Wed Nov 2 19:29:50 1988 Date: Thu, 27 Oct 88 16:38:12 CDT From: Michael K. Smith To: info-ada-request@ajpo.sei.cmu.edu Subject: Unpredictable Ada I just received a copy of Date: 18 Oct 88 14:17:00 GMT From: inmet!ishmael!inmet!authorplaceholder@bbn.com Subject: Vendor introduces "safe" Ada subset Regarding: >... To achieve Ada integrity, Spark has introduced several restrictions. It ... From a compiler writer's viewpoint, generics, exceptions, and even tasks are just compile-time notions: We know *exactly* how to translate them to simpler language features. .... Mike Ryer Intermetrics and am compelled to respond. I think the Spark stuff is fundamentally motivated by a desire for PREDICTABILITY. Program proof is one way to get this, but it shares many of the same requirements of people who just want their code to run predictably. Predictability is impossible to guarantee with certain Ada constructs because the so-called definition explicitly permits them to be implemented so as to behave in a wide variety of ways. A single Ada compiler yields a perfectly predictable result. It is just that different compilers yield different results. If you want your code to behave in a predictable fashion you can do one of two things. 1. Choose to use a single compiler for which you can determine which of the implementation options have been selected. 2. Write in a subset that will behave predictably. A few examples: 1. There is no way to know what will happen with predefined exceptions. To quote the section on exceptions and optimization [11.6 (5)] Such a reordering is allowed even if it may remove an exception, or introduce a further predefined exception. Its really more bizarre than that, but you get the idea. There is more going on than not knowing what exceptions will actually be raised by a program. When an exception is HANDLED, you in general can't know what the values of various variables are since they depend on order of evaluation and the parameter passing mechanism. Of course any program that depends on particular implementations of these is erroneous, but there is no specified way to detect an erroneous program. The only way to avoid erroneous programs is to avoid constructs that give rise to them. 2. One of the people that I am working with has developed a really nice set of generic packages. On his first try he found one validated Ada compiler that compiled it properly, out of 6 that he tried. He has since convinced one other of the compiler manufacturers to fix their generic implementation so that his package works. 3. Anyone doing real time tasking in Ada knows that they must find out what scheduling algorithm is being supported. Code that runs fine under one compiler won't run at all under another. For a fairly exhaustive list of the compiler variations that need to be considered by anyone concerned with performance or reusability see "Catalogue of Ada Runtime Implementation Dependencies" prepared by the ACM Special Interest Group on Ada, Ada Runtime Environment Working Group. What if my application *needs* more than one thread of control, because of multiple asynchronous interactions with the outside world? You just need to choose a particular compiler whose behavior is predictable. Any proofs you do will need to take into account the implementation choices made by this particular compiler. Porting to a different compiler will be a non-trivial task involving a careful comparison of the implementation choices of both compilers. If the claim is being made that full Ada is inherently unprovable, I'd like to see the proof. Full Ada is not inherently unprovable if you are willing to accept a proof that says a particular program will behave in one of a very large number of ways. This sort of specification, conditioned by the multiplicity of implementation decisions, is not comprehensible or useful. If you want to be able to prove something specific about the input/output behavior of a particular Ada program that uses the constructs that Spark rejects you are out of luck. (Again, assuming you are proving something about Ada, as opposed to Ada as implemented by compiler X.) Just to make my biases clear, I am currently involved in a project to write a formal definition of a subset of Ada in the Boyer Moore logic. The intent is that this subset will be as independent of particular implementation choices as possible. - Michael K. Smith (mksmith@cli.com) Computational Logic Inc. 1717 W 6th, Suite 290 Austin, TX 78703