SPARK gets another fan

SPARK gets another fan

[Mike Silva]

This is from the latest "Embedded Muse 90", an e-newsletter put out by
Jack Ganssle (he gives permission for noncommercial redistribution):

Book Review � High Integrity Software
-------------------------------------
"High Integrity Software" � the title alone got me interested in this
book
by John Barnes. Subtitled "The SPARK Approach to Safety and Security",
the
book is a description of the SPARK programming language's syntax and
rationale.
 
The very first page quoted C. A. R. Hoare's famous and profound
statement:
"There are two ways of constructing a software design. One way is to
make
it so simple that there are obviously no deficiencies. And the other
way is
to make it so complicated that there are no obvious deficiencies."
This
meme has always rung true, and is one measure I use when looking at
the
quality of code. It's the basis of the SPARK philosophy.
 
What is SPARK? It's a language, a subset of Ada that will run on any
Ada
compiler, with extensions that automated tools can analyze to prove
the
correctness of programs. As the author says in this Preface, "I would
like
my programs to work without spending ages debugging the wretched
things."
SPARK is designed to minimize debugging time (which averages 50% of a 
project's duration in most cases).
 
SPARK relies on Ada's idea of programming by contract, which separates
the
ability to describe a software interface (the contract) from its 
implementation (the code). This permits each to be compiled and
analyzed
separately.
 
It specifically attempts to insure the program is correct as built, in
contrast to modern Agile methods which stress cranking a lot of code
fast
and then making it work via testing. Though Agility is appealing in
some
areas, I believe that, especially for safety critical system, focus on
careful design and implementation beats a code-centric view hands
down.
 
SPARK mandates adding numerous instrumentation constructs to the code
for
the sake of analysis. An example from the book:
 
Procedure Add(X: In Integer);
--#global in out Total;
--#post Total=Total~ + X;
--#pre X > 0;
 
The procedure definition statement is pure Ada, but the following
three
statements SPARK-specific tags. The first tells the analysis tool that
the
only global used is Total, and that it's both an input and output
variable.
The next tag tells the tool how the procedure will use and modify
Total.
Finally a precondition is specified for the passed argument X.
 
Wow! Sounds like a TON of work! Not only do we have to write all of
the
normal code, we're also constructing an almost parallel
pseudo-execution
stream for the analysis tool. But isn't this what we do (much more
crudely)
when building unit tests? In effect we're putting the system
specification
into the code, in a clear manner that the tool can use to
automatically
check against the code. What a powerful and interesting idea!
 
And it's similar to some approaches we already use, like strong typing
and
function prototyping (though God knows C mandates nothing and
encourages
any level of software anarchy).
 
There's no dynamic memory usage in SPARK � not that malloc() is
inherently
evil, but because use of those sorts of constructs can't be
automatically
analyzed. SPARK's philosophy is one of provable correctness. Again�
WOW!
 
SPARK isn't perfect, of course. It's possible for a code terrorist to
cheat
the language, defining, for instance, that all globals are used
everywhere
as in and out parameters. A good program of code inspections would
serve as
a valuable deterrent to lazy abuse. And it is very wordy; in some
cases the
excess of instrumentation seems to make the software less readable.
Yet
SPARK is still concise compared to, say, the specifications document.
Where
C allows a starkness that makes code incomprehensible, SPARK lies in a
domain between absolute computerese and some level of embedded
specification.
 
The book has some flaws � it assumes the reader knows Ada, or can at
least
stumble through the language. That's not a valid assumption anymore.
And
I'd like to see real life examples of SPARK's successes, though
there's
more info on that at http://www.sparkada.com/.
 
I found myself making hundreds of comments and annotations in the
book,
underlining powerful points and turning down corners of pages I wanted
to
reread and think about more deeply.
 
A great deal of the book covers SPARK's syntax and the use of the
automated
analysis tools. If you're not planning to actually use the language
your
eyes may glaze over in these chapters. But Part 1 of the tome, the
first 80
pages which describes the philosophy and fundamentals of the language
and
the tools, is breathtaking. I'd love to see Mr. Barnes publish just
this
section as a manifesto of sorts, a document for advocates of great
software
to rally around. For I fear the real issue facing software development
today is a focus on code uber alles, versus creating provably correct
code
from the outset.
 
High Integrity Software, The SPARK Approach to Safety and Security, by
John
Barnes. Published by Addison-Wesley, ISBN: 0321136160.

Re: SPARK gets another fan

[Vinzent 'Gadget' Hoefler]

Mike Silva wrote:

>This is from the latest "Embedded Muse 90", an e-newsletter put out by
>Jack Ganssle (he gives permission for noncommercial redistribution):

Yeah. SPARK seems to reach some audience. Yesterday Rod mentioned that
the current edition of John's "High Integrity Software" sold better
than the first one. Whatever this means when expressed in numbers - it
can't be too bad. :)


Vinzent.

Re: SPARK gets another fan

[Jeffrey Carter]

Vinzent 'Gadget' Hoefler wrote:

> Yeah. SPARK seems to reach some audience. Yesterday Rod mentioned that
> the current edition of John's "High Integrity Software" sold better
> than the first one. Whatever this means when expressed in numbers - it
> can't be too bad. :)

I wish I could get a job where people are at least concerned enough 
about software quality to actually have and use a design and 
implementation method, much less the discipline of something like SPARK. 
I'm tired of US defense contracts where quality is a bad thing, because 
creating bad software takes longer, and that translates into more 
profits for the contractor.

-- 
Jeff Carter
"C++ is like giving an AK-47 to a monk, shooting him
full of crack and letting him loose in a mall and
expecting him to balance your checking account
'when he has the time.'"
Drew Olbrich
52