Operation POs are missing let binds

[peterwvj]

There seems to be a general problem with POs generated from operations. Consider the operation:

op : () ==> nat
op () ==
 let r = 0
 in
   return 1/r;

Which gives you the PO: (r <> 0). The problem problem is that r is a undefined value in the context of the PO. What the PO should do is to introduce a binding for r, i.e. let r : int = 0 in ....

Whereas if you generate POs for the function:

f : () -> nat
f () ==
 let r = 0
 in
   1/r;

You get: let r:nat = 0 in (r <> 0) which is correct.

Also for f you get the type compatibility PO is_(let r:nat = 0 in (1 / r), nat) whereas the type compatibility PO for op is also missing the let bind.

[peterwvj]

I have looked a bit more into this. Since functions are working and operations are not I tried to compare the caseALetStm and caseALetDefExp cases in the PogParamStmVisitor and the PogParamExpVisitor, respectively, as I was expecting them to be similar.

The bodies of the two case methods are indeed very similar but there is one important difference. The caseALetDefExp method pushes a POLetDefContex and passes along the ALetDefExp node (question.push(new POLetDefContext(node))). However, on the equivalent line the caseALetStm pushes a POScopeContext (question.push(new POScopeContext());) but it does not pass the let statement with the definitions. Also, the POLetDefContex only works for ALetDefExp (and not the statement).

So maybe this is only a matter of creating and using a PO context for the let statement.

@Override
public IProofObligationList caseALetStm(ALetStm node,
        IPOContextStack question) throws AnalysisException
{
        ...
        question.push(new POScopeContext()); // Probably should be question.push(new POSomeLetDefContex(node))
        obligations.addAll(node.getStatement().apply(mainVisitor, question));
        question.pop();

        return obligations;
       ....
}

[ldcouto]

Is there any difference between let statements and expressions?

(other than the obvious of one working for statements and the other for exps)

[peterwvj]

Are you thinking of whether it is possible to update the POLetDefContext to work with both let expressions and let statements?

If you look into the POLetDefContext class you will see that it really only uses the local definitions of the let expression. So maybe the POLetDefContext class could be updated to only take the local definitions as arguments (instead of the entire let construct) and then the POLetDefContext might also work for the let statement.

[nickbattle]

I think the main difference is that let statements exist in a non-functional context and so the evaluation of the variable values can involve operation calls - "let x = op(123) in ...". Since those calls can arbitrarily muck about with state (which the body of the definition may reference), it is difficult to write a PO for the body that adequately reflects the constraints under which the PO holds, if it reasons about state values (at least not without reproducing the body of the "op(123)" call in the PO, which could get ulgy... !!).

This is the same basic reason why VDMJ (and I think, VDMTools) do not attempt to give much context for POs within statement/operation contexts. They just say "The sequence index must be within range" rather than trying to say "For all arg values, when defining this value, the sequence index must be within range".

We'd need to check with PGL, but I'm sure he and I discussed this many years ago. It may be that we need to limit what some state oriented statement POs produce?

[ldcouto]

Right, I see the point. We may not need two contexts. We can use the let exp context for introducing the variables and the op call context (see below) to handle any op calls. I assume all expressions in the rhs of the let are evaluated before the in?

Regarding op calls and what they may do to the state, the way we tackled that in COMPASS was with post-conditions. Whenever you call an operation, its post-condition is conjoined to the context. Of course, this assumes users are writing adequate POs for their operations, but that's how it goes.