[Prev][Next][Index][Thread]

denotational versus operational semantics

Date: Mon, 30 May 88 20:15:45 +0200 (MET dst)



I want to add something to our discussion (and take up again an
earlier one which we had with Bob Tennent and Frank Oles at POPL).

I can accept the viewpoint which Albert presented: The original semantic
concepts might be vague, and rewrite rules are one possibility to make
them precise.  And I also agree that recursion is a "constructive"
idea (fixed points have never been my favorite semantic concept).  

But I think we must be careful when we speak about the LOGICAL view.
I fear that there are again TWO views
1) Logic is only symbol pushing: We have a (purely syntactic) calculus
for proving properties of programs like partial or total correctness
or equivalence. 
2) Logic is more than that: The axioms and rules of the calculus
should be formal versions of intuitive and simple semantic concepts.

Here is my favorite example to compare these two views: Consider
parameter passing mechanisms in ALGOL-like languages.  From the symbol
pushing point of view, call-by-name is the simplest concept.  This can
be seen in Reynolds' specification logic where call-by-name procedure
calls are simply handled by substitution.  On the other hand one needs
extra (and more sophisticated) axioms to handle procedure calls with
value- or reference-parameters.  But does that mean we should prefer
call-by-name ?  We all know, that procedures with name-parameters can
have "unexpected behavior", e.g.

begin
var i: integer; 
var a: array of integer;
procedure P(x: integer):                           % x name parameter
x := 0; while i>0 do x := x + i; i := i-1 od       % i global variable
end P;
 ...
i := 10;
P(a[i])                       % changes the contents of a[10], ... a[1]
 ...
end

It's not hard to see (or to prove formally), what this program does.
So what's unexpected ?  

The problem is that we want to use procedures as an abstraction
mechanism.  Then we have to SPECIFY the procedure, i.e. to describe
its behavior in general (and not only for a particular call).  In
other words: we must consider the procedure as a FUNCTION of its
parameters.  And that's difficult for call-by-name (try it with the
example !), and much easier for call-by-value or -reference, because
the SEMANTIC concepts 'value' and 'location' are simpler than 'thunk'
(for name parameters).

Of course specification logic has been designed for specifying
procedures (in contrast to earlier Hoare-style calculi), but I fear
that Reynolds' decision to use only thunks for this purpose has made
specification logic unnecessarily complicated.  I think that the
simplicity of the procedure call axiom was misleading in this case and
that the denotational semantics reveals the difficulties which we have
with call-by-name.

Regards

Kurt. 


PS: I hope it's clear that I don't want to criticize specification as
a whole, but only the decision to use call-by-name !