[Prev][Next][Index][Thread]
denotational versus operational semantics
/* Written 8:04 pm May 30, 1988 by sieber%fb10vax.i@RELAY.CS.NET */
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 ?
...
Kurt.
/* End of text */
I believe that has an easy answer. Call the procedure (\x.P). We can
prove using an equational calculus of assignment programs (see for
example the "Laws of Programming" calculus of Hoare et al. CACM, Aug
87) and a little induction that
P = P' (assuming i >= 0)
where P' is
(x,i) := (i*i, 0)
If we have a Church-Rosser property for our calculus, then the
equality
((\x.P) a[i]) = ((\x.P') a[i])
must hold. Or, put another way, "executing" both the programs should
give the same answer. But, it doesn't. So, we don't have a Church-Rosser
property. (Incidentally, Church-Rosser property holds for a
call-by-value language. But, it doesn't hold for call-by-reference.
So, there is no easy way out). If you are bothered by the use of
induction in proving P = P' (which is not quite operational
reasoning), you can use one of the standard examples without loops
which illustrates the same point.
So, the complexity of call-by-name + assignments can be shown by
purely operational (or deductive) reasoning.
Incidentally, can you give me the reference for Reynolds's
"Specification Logic"?
Uday