karl@grebyn.com (Karl Nyberg) (11/26/88)
[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 <haven!CLI.COM!mksmith>
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