PO wrong if no result for implicit operation

[pglvdm]

For an example such as:

process Test =
begin

state 
  n : nat

operations

Op(a: nat) 
frame rd n : nat
pre a > 42
post n = a

@ Skip

end

one gets a PO:

(forall a:nat & (pre_Op(a) => (exists  & post_Op(a))))

which should be:

(forall a:nat & (pre_Op(a) => post_Op(a)))

[pglvdm]

We,ll coming to think about this I guess that it really should be:

(forall a, n:nat @ (pre_Op(a) => post_Op(a,n)))

And if the frame would have been "wr" instead it should be

(forall a, n:nat @ (pre_Op(a) => post_Op(a,n,n~)))

with the state component argument in a standardised order (same as in the translation of the definition. Thus, maybe one should use the latter in all cases?

[ldcouto]

I think it's actually more complicated than that. I was under the impression that quoting of pre and post conditions of operations is not allowed in CML. Am I incorrect?

[pglvdm]

No you are right that quoting of pre and post conditions are only properly defined for functions as far as I am aware.

[ldcouto]

So instead of post_Op(...) we would print out the entire body of the pre/post yes?

[pglvdm]

Yes

[ldcouto]

Fixed. The reported spec now produces: (forall a:nat, n:nat & ((a > 42) => (exists n1:nat & (n1 = a))))