Re: Strategies with SPARK which does not support exceptions

["Randy Brukardt" <randy@rrsoftware.com>]

"Claude" <claude.defour@orange.fr> wrote in message 
news:d90f60dd-b74f-4eff-b9d8-803ebb64c9d2@z8g2000yqz.googlegroups.com...
>
>Exceptions are not the best way to process error. (i.e., Not just a
>SPARK topic).

There is an extra "not" in your statement. :-) You must have meant 
"Exceptions are the best way to process error."

Result codes are dangerous, as ignoring of result codes is one of the major 
problems in programming, and the resulting bugs are very, very hard to find. 
(That's because of the difficulty of finding errors of omission.)

Perhaps you are too young to remember, but early versions of Windows (3.0, 
3.1) had a reputation for being unstable and crashing often. But the 
problems were mostly not with Windows but rather with programs that tended 
to ignore the error returns from the Windows API. As such, they tended to 
continue running but using non-existent Windows handles and the like. Given 
the lack of memory protection on 16-bit computers, these errors tended to 
take the entire Windows subsystem with them.

We developed a "middle-level" binding for programming Windows, which used 
exceptions rather than error codes, and programs developed with it tended to 
be much more stable than the commercial programs we were using at the 
time --- probably because even when they failed, they didn't take the entire 
OS with them (just popped up a message box and terminated properly).

I understand the problems with safety-critical systems and the need to test 
to check exceptions, but I believe that the proper solution to those 
problems is on the line of exception contracts and proving exception absence 
when necessary to fufill those contracts. In particular, if a routine is 
declared to not propagate Constraint_Error, then the routine is incorrect if 
it in fact could propagate that exception. (I'm mildly annoyed that we 
didn't have time in Ada 2012 to pursue those sorts of contracts seriously.)

There is no technical reason that tools like SPARK couldn't support 
exceptions if they wanted to do so. Compiler optimizers are a form of proof 
tool, and they have no problem dealing with exceptions. (That's because the 
control flow caused by exceptions is quite limited, and is generally out of 
blocks -- outbound flow has little effect on proofs within a block).

Returning to the dark ages of programming (that is BE - Before Exceptions) 
and reintroducing all of the problems of early C code just because of 
inadequate tools seems like a horrible step backwards to me.

This is exactly why I'm not much interested in SPARK itself: because it 
forces programs back into the style that I originally learned for Fortran IV 
in 1976: no dynamic allocation, no dynamic calls, no exceptions -- no 
interest! I'm interested in what SPARK brings to the table in proof 
capabilities, but I see no reason to give up 3/4rds of Ada to get it. 
(Remember that Ada allocators, Ada O-O dispatching, Ada access-to-subprogram 
calls, are all type-safe and provide plenty of opportunity for reasoning).

                       Randy Brukardt.