🚀 go-pugleaf

Ralph Johnson has claimed that every specification is a program, and this
statement has been challenged by other posters.  Since I take it as an
article of faith myself, I'll try to clarify it.

No specification or program by itself does anything, except take up disk
space.  A program (as we all learned at a tender age) is a sequence of
instructions.  These instructions must be executed by (in cases of interest
to us) a computer.  And the code we see is seldom executed directly; it is
normally processed by a compiler and friends.  Therefore, when we speak
about executing a program, we implicitly acknowledge the existence of large
amounts of hardware, software and cleverness, which make up our program
execution engine.

Specifications are not generally executed, and therefore the market for
specification language engines is thin.  However, in principle, such an
animal is quite possible.  A specification defines the set of acceptable
output states for a given input state.  (I'll certainly accept other
flavours of specification, but similar arguments can be made.)  To
implement the specification, simply enumerate the domain of output states
until one satisfying the postcondition is found.  Or, if you prefer, select
states nondeterministically until satisfaction.  If the specification is
satisfiable, then the specification engine will terminate, albeit in
unbounded time.

Bruce Weide gave a description of a specification which he claims is
unimplementable:

>Suppose you have a component
>that keeps track of a function from some domain type D to some range
>type R (both parameters to the component).  You want to specify a
>boolean-valued operation that returns "true" given f and r iff
>function f maps some value of type D to the specific value r.  This is
>easy to specify in the abstract using an existential quantifier;
>something like:
>
>	there exists d:D such that f(d) = r
>
>Presumably the source code to explain this behavior consists of a
>program to search through all values of type D for one that f maps to
>r.  Two problems here.  First, D may not be finite, in which case this
>is not an algorithm at all because it may not terminate and could
>never return "false".  Second, how do you write this program (except
>in pseudocode or something) without knowing what type D is?

This isn't quite fair, because he's given a specification of a
component or function g without specifying the function f that it
uses.  If f is specified, then we can enumerate through the range
of g ({true, false}) in quite acceptable time.  The specification of f is
executed in the same manner.

The only reason that implementations are somehow more ``concrete'' than
specifications, then, is that we've gone to the trouble of building the
program execution engines.  Specification engines would actually be
easier to build in some ways, because we can be totally uninterested in
performance.

So both specifications and implementations are descriptions of a
computation, which merely differ in undescribed side effects.  Formal
verification is just the process of showing that the two are in fact
equivalent.  The advantage of the implementation is its efficiency.
The advantage of the specification *should* be its clarity.  If the
specification is no clearer than the implementation, then it is of
academic interest at most.

My PhD thesis, by the way (Extremely Real Soon Now) is on the subject of
specification and verification of object languages.  This should make
me the world's greatest booster of component selection by specification
alone.  Well, the work is worth doing so that giants can step on my
shoulders.  However, we're a long way from modular, sound, and complete
object specifications, let alone ones that are easier to read than the
source.  (Those who wish to challenge this statement are invited to do
so by mail.  Note that the claim has four adjectives and a noun that
require precise definitions.)

Probably the main advantage of formal specifications is that they can be
used to prove that if sub-components meet their specifications, their
component sum will too.  But that's a property of an associated proof
system, not the specification language per se.
-- 
John Hogg			hogg@csri.utoronto.ca
Department of Computer Science, University of Toronto