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!lll-winken!lll-tis!ames!ll-xn!mit-eddie!bbn!inmet!ishmael!inmet!authorplaceholder
From: ryer@inmet.UUCP
Newsgroups: comp.lang.ada
Subject: Re: Vendor introduces "safe" Ada subset
Message-ID: <124000017@inmet>
Date: 18 Oct 88 14:17:00 GMT
References: <6073@june.cs.washington.edu>
Nf-ID: #R:june.cs.washington.edu:-607300:inmet:124000017:000:2344
Nf-From: inmet.UUCP!ryer    Oct 18 10:17:00 1988
List-Id: <comp.lang.ada>


Regarding:

>... To achieve Ada integrity, Spark has introduced several restrictions.  It
>does not allow the use of tasks, exceptions or generic units.  Access types 
>are also omitted, as these are considered unacceptable in real-time safety
>critical applications.  ... Certain features - such as "go to" statements
>and "declare" statements - are totally barred.

>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.  For example the compiler creates new (non-generic)
code for each instantiation of a generic.  It converts tasking constructs into
calls on subprograms which themselves are written in Ada without using tasking.
Ultimately there is a piece of hardware at the bottom that only has gotos and
a handful of datatypes.

I appreciate the *complexity* of doing any kind of program proving in
the presence of generics, separate compilation, tasking, exceptions, and
so on.  What I find irritating is the often repeated premise that one
*must* subset in order to make proving feasible.  If a compiler can translate
generics into non-generic code, why can't a program prover do the same?

What if my application *needs* more than one thread of control, because of
multiple asynchronous interactions with the outside world?  Am I to implement
a full executive in Ada (or assembler) and prove it?  If so, how is this any
easier than proving the implementation of the tasking semantics that happen
to be built into Ada already?

If exceptions are not permitted, I presume that the prover is able to prove
that no exceptions such as numeric error or constraint error can ever occur.
If so, it can *surely* also tell whether a given raise statement is going
to be executed and when (i.e. which handler will be activated).  If I were
on an airplane, I'd rather believe that there was an appropriate handler for
every possible exceptional condition than that someone had mathematically
proven that the *source code* of the flight control software would never
cause an exception.

There is no doubt that Spark is *easier* to prove than Ada.  If the claim
is being made that full Ada is inherently unprovable, I'd like to see
the proof.

Please excuse the flame, which is personal, not corporate.
Mike Ryer
Intermetrics