Type invariant violation incorrectly reported for the state type

[peterwvj]

When I run Entry`op() for the small specification below

module Entry

definitions

state St of
 x : nat
 init s == s = mk_St(0)
 inv s == s.x = 0
end

operations

op : () ==> nat
op () ==
let locSt = mk_St(1)
in
  return locSt.x;

end Entry

..I get the following error:

> p Entry`op()
Error 4079: Type invariant violated by mk_St arguments in 'Entry' (Test.vdmsl) at line 15:13
Stopped in 'Entry' (Test.vdmsl) at line 15:13
15:  let locSt = mk_St(1)
[MainThread-8]>

So the error is produced when I create a local record value of the record type used to define the state. When I read the LRM it says that "The invariant invpred is a boolean expression denoting a property which must hold for the state ident at all times". But it seems like the interpreter treats the invariant in the specification as an invariant over the type 'St' (rather than over the state component).

It's the same for both VDMJ and Overture. VDMTools, on the other hand, does not report the error. Personally I prefer the VDMTools behaviour.

[nickbattle]

I think we should check this with PGL to see if there is any intention of the "Sigma" record type that we're missing if we change this, but yes, on the face of it this may well be a bug.

If it's causing problems, you should be able to fix it by commenting out line 325 of DefinitionTypeResolver.java:

// rtype.setInvDef(node.getInvdef());

A few quick tests suggest that this has the effect we want - the invariant still applies to the state, but the record type as such does not have an invariant.

[peterwvj]

Thanks for looking into this. I'll check with PGL to get his input on this.

[pglvdm]

Well I can certainly understand the confusion here. Personally I had to lok at the ISO VDM-SL standard to find out what was correct here (see http://www.nicoplat.com/sites/default/files/tr-isovdmsl.pdf). In section 8.1.3 at the page called 222 you will see that the transformation from the Outer Abstract Syntax (similar to the Overture AST) to the Core Abstract Syntax. It turns out that in essence the invariant on the state is transformed into into a record type definition with that invariant. Thus as far as I can judge VDMTools is wrong here and Overture and VDMJ is right (according to the ISO standard).

[peterwvj]

Thanks, Peter.

Well, that's interesting and a bit unexpected, I think. Shame on me for reporting it as a bug then :)

I read the part about state transformation and I understand it the same way as you do - at least I think. So effectively the state invariant works like a type invariant on the type of the state.

Any thoughts about this, Nick? Do you understand it differently?

[nickbattle]

I very vaguely remember discussing this with Peter a long time ago when I was implementing it. I remember coming up with a list of six or seven points about how exactly these state records were created and what their type behaviour was. VDMJ was the resulting implementation, so I guess we did discuss this. I'll see if I can find that email at work tomorrow.

If you think of a state definition as similar to a "compose" record definition (the syntax is very similar), then it seems natural to me that the record type carries the invariant. The drawback (from memory) is that this causes problems with the state invariant function - inv_Sigma: Sigma +> bool - because you cannot construct an invalid Sigma record to pass! This is the same with inv_R functions for normal record types. But this is a well known problem (the LB tried to solve it years ago, but none of the solutions was ideal and we left things as they were!).

[peterwvj]

Hi Nick. Yes I see your problem. Just curious though. What would be the problem(s) if the inv_Sigma function was updated to take the fields as arguments instead? inv_Sigma: FieldType1 * .. FieldTypeN +> bool. Basically to avoid constructing the record before checking it.

[nickbattle]

I would have to wade through the mail trail from the LB to answer that. Several subtleties cropped up, some to do with semantic problems and some tool problems. I can share the mail if you wish (50 or so), but the important point is that we have the discussion captured somewhere!

[peterwvj]

Hi Nick. No that's okay - it was just to check if there were any obvious problems that I was not aware of.

[peterwvj]

I think we can close this issue for now..