[Prev][Next][Index][Thread]
specification logic and call by name
Kurt: A few comments on your note.
1. The use of deferred evaluation of parameters ("call by name")
does not require that "only thunks" (state-dependent expression
meanings) be used. I agree with Reynolds on the former, but agree
with you that it can be convenient to have "pure" value-denoting
identifiers. This can be done by introducing a new class of
phrase types, say val[t], for each data type t, with
[[val[t]]] = [[t]] lifted, and then [[exp[t]]] = S -> [[val[t]]],
where S is the set of states (or, more generally, the states
functor). Then value phrases are state-independent, and so
are not "expression-like". For example, a swapping procedure
could be specified in specification logic as follows:
all x,y:var[t]. all x0,y0:val[t]. gv(x) & gv(y) & y#x =>
{x=x0 and y=y0} swap(x,y) {x=y0 and y=x0}
which avoids a lot of distracting non-interference assumptions
about x0 and y0 (compare with the Craft of Programming, page 240).
But such value phrases would still be called-by-name in the sense
of deferred evaluation. Conceivably, location-denoting phrase
types could be added in the same fashion, with a coercion from
locations to variables, but I'm not convinced that the low-level
concept of location has any advantages.
2. You suggest that call by name is easy to reason about yet has
"unexpected behaviour". Depends on what kind of behaviour one
expects! I think the behaviour seems unexpected primarily to
programmers who are more familiar with FORTRAN and PASCAL
than with ALGOL 60. With the well-known example swap(i, a[i]),
the formula obtained by simple substitution of the actual
parameters for x and y in the specification above immediately
warns the programmer not to expect the post-condition a[x0]=x0
(unless x0=y0). Providing both expression AND value phrase types
should help to clarify the difference between them.
3. You suggest that it must be possible to specify the behaviour of
procedures "in general". But how general? Nobody is surprised when
the specification of a command has a non-trivial pre-condition
(on the state), so why shouldn't a specification have non-trivial
assumptions (on free identifiers)? For example, the specification
of swap above has three assumptions on x and y; but then the
behaviour of swap(x,y) is unspecified for actual parameters that
fail to meet those requirements. A "complete" specification would
indeed be much more complicated, but uselessly so, since the programmer
is probably not interested in the behaviour of the procedure under
those conditions. Obviously this approach will not be acceptable to
people who think that the main function of a programming
logic is to provide an opportunity to prove a completeness theorem,
rather than to be useful in developing correct programs.
But I think the use of conditional specifications represents a
reasonable compromise between ease of reasoning and generality.
Notice that the assumptions in the example are generated more or
less automatically when using the assignment axiom in reasoning
about the body of the procedure.
Regards, Bob Tennent