On software quality and engineering

[Doug.Palmer at csiro.au]

> Another point is that if you have the specification in that formal
> language, then you effectively /have/ the code - if the formal
> language is sufficient to describe the system completely, then it
> should be equivalent to the code for the system. Equivalent meaning
> automatically translatable to the code (and hence to the final
> executable). 

It depends on how the specification is "worded" in the formal language. The
specification languages that I'm (mildly) familiar with are formal
specifications of outcomes, not processes. So you might have a function
specification which is something like:

sqrt: a R -> b R, a >=0, b >=0 : abs(b * b - a) < b * 10e-6

That's good, in the sense that it clearly states what's expected of a square
root function. But you still have to pick an algorithm (bisection,
Newton-Rapheson, ... ?) to actually implement it. Or use Prolog and have it
guess results until it finds a correct one.[*]

There's also the whole issue of specifying non-functional requirements, the
"ilities": availability, integrity, maintainability, tracability,
performance and so on.

> My suspicion is that no matter what kind of tools or languages or
> whatever you might try to apply to the problem, there's just no way
> to turn a complex task into a simple task, or even to reduce the
> complexity by anything approaching an order of magnitude. 

I don't think that that's really the aim of formal specifications. 

One (not necessarily the) aim is to describe, in a _different_ language to
the implementation language, the expected results. As a consequence, any
tension between the implementation and the specification can be identified
and traced; possibly resulting in a change to the specifications as well as
the program. There's a little bit of that mentality in any statically typed
language, where you have to declare the types in a sub-language different to
the use sub-language. There's also a bit of that approach in systems which
develop, in isolation, two programs to the same spec. so that any
disagreements between the two can be used to identify trouble.

Another aim is to allow coverage proofs, so that you can show that the
program domain really is covered by the spec. without any curious holes in
the domain space that people will find out about later in bizarre and
embarrasing curcumstances. It's not 100% foolproof, of course, there's a
long history of faulty mathematic proofs, to begin with.

> So it'll
> never be noticably easier to make provably correct software systems
> . . . The real gains would likely lie in coming up with processes
> that made it practical to approach that level, without being
> prohibitively expensive.

Extreme Programming seems to have a significant foothold. There's a
considerable amount of effort involved in producing all those test cases. I
wonder what would happen if that effort was expended, instead, on formal
specifications which allow the automatic generation of test cases? (Probably
a disaster, I suspect, most programmers that I know of -- including myself
-- are not mathematically adept enough to handle the level of abstraction
required.)

[*] There's a lovely sort program at the start of Foundations of Logic
Programming that "works" by generating permutations of the input until it
finds a sorted one.