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

specification logic and call by name


Thanks for your clarifying comments.  I think I haven't done a good
job by mixing
- the denotational/operational discussion,
- my critique in specification logic.
Let's talk only about specification logic now.


1. Using value identifiers	

You are right: We can ADD value identifiers to specification logic,
without throwing away name parameters.  But I don't think that this is
only CONVENIENT (as you expressed it), I consider it as IMPORTANT.


Here is an example:

c is a VALUE identifier and x is a LOCATION identifier (which I
would also like to add; I can't see why location-returning thunks
should be less problematic than value-returning thunks). 

Let the second order procedure P be specified by:
spec(P):   (all c,Q. {x=c} Q {x = c+1} => {x=c} P(Q) {x=c+2})
In words: Whenever the parameter Q increments x by 1, then P(Q)
increments x by 2.   

Let the parameterless procedure Q' be specified by:
spec(Q'):   all c. {x=c and c>5} Q' {x=c+1}
In words: Q' increments x by 1, provided its initial contents is >5.

Now we want to prove 
(*)   (spec(P) & spec(Q')) => all c. ({c>5 and x=c} P(Q') {x=c+2})
In words: It follows from the specifications of P and Q' that P(Q')
increments x by 2, whenever the initial contents of x is >5.

The main steps of the proof are: 
(1)  spec(Q') => (all c. {c>5} => {x=c} Q' {x=c+1})
(2)  spec(P) => (all c. ({c>5} => {x=c} Q' {x=c+1}) 
                           => ({c>5} => {x=c} P(Q') {x=c+2}))
(3)  (spec(P) & spec(Q')) => (all c. {c>5} => {x=c} P(Q') {x=c+2})

We can then use the following axiom (among others) to derive (*) from 
(3):
({r} => {p} St {q}) => {r and p} St {r and q}
        if r is (syntactically) state independent
(Choose c>5 for r.)
This axiom is (classically) valid, because (the state independent
formula) r holds for ALL states (assumption on the LHS) iff it holds
for the initial state of the statement St (assumption on the RHS).

But if we DON'T have value identifiers, then we must use a thunk
identifier u instead of the value identifier c.  I suppose that the
first three steps still work without problems, with some "non
interference" and "good variable" conditions added to the formulas,
in particular with the information P(Q')#(u>5) in formula (3).

But then we need Reynolds' STRONG CONSTANCY axiom:
        St#r & ({r} => {p} St {q}) => {r and p} St {r and q} 
(Choose P(Q') for St, u>5 for r, ...)
This axiom is classically INVALID, because---even for a formula r
which doesn't interfere with St---the assumption that r holds for ALL
states (LHS) is stronger than the assumption that it holds for the
initial state of St (RHS). 


Summary: I suppose that the problematic axioms of specification logic
are only necessary because of the EXCLUSIVE use of state dependent
identifiers instead of (state independent) value or location
identifiers.   


2. Specifying call-by-name procedures

I agree that we do not always need 'general' specifications, as long
as we don't aim for theoretical completeness results.  But it seems to
me that 'reasonable' assumptions on a name parameter u for a procedure
P always guarantee noninterference between P and u.  Hence the
question is, why we should use state dependent parameters at all.

It's not quite clear to me whether we can have deferred evaluation
WITHOUT state dependence in an imperative language ?  I think it's
obviously possible, but is it also reasonable, efficient ?  Are there
languages with such parameters ?  This might be a compromise. 

Regards, Kurt Sieber.