#185 TC should warn about assignments to variables not in nameset

[Joey Coleman]

The typechecker should issue warnings (not errors!) in cases where a sub-action of a parallel operation that uses namesets might assign to a variable that is not in its corresponding nameset.

This should only be a warning; it's perfectly valid to assign to a variable not in your corresponding nameset, but any changes will be thrown away. This is analogous to shadowed variables in regular VDM.

In the below example, there should be warnings at the interleave construct for AssignOp and AssignAct: AssignOp modifies y and AssignAct modifies x, but neither have those variables in their namesets. The last assignment to z is fine, as the corresponding nameset contains z.

process A = begin
state
  x : int := 0
  y : int := 0
  z : int := 0

operations
  AssignOp : () ==> ()
  AssignOp == y := 1

actions
  AssignAct = x := 1
@
  AssignOp() [|| {} | {} ||] AssignAct [|| {} | {z} ||] z := 1
end

[Kenneth Lausdahl]

I'm not sure what the problem is here. The errors reported are defiantly right:

1: This "AssignOp == y := 1" is not a valid input for the parser. It is missing the "()"
2: When this is fixed then AssignOp is used in a place where only an action is allowed.

The fixed model does not contain any errors or warnings so I'm not sure what error it is that is reported wrong.

process A = begin
state
  x : int := 0
  y : int := 0
  z : int := 0

actions
  AssignAct = x := 1
  AssignOp = y := 1
@
  AssignOp [|| {} | {} ||] AssignAct [|| {} | {z} ||] z := 1
end

Does this then mean that the type checker should have a more strict check that detects the cases mentioned above where warnings should have been generated

[Joey Coleman]

Don't set this to cannot-reproduce --- it is a new feature request. Talk to me about what is required.

Example code above fixed.

[Joey Coleman]

• Description has changed:

Diff:

--- old
+++ new
@@ -18,6 +18,6 @@
 actions
   AssignAct = x := 1
 @
-  AssignOp [|| {} | {} ||] AssignAct [|| {} | {z} ||] z := 1
+  AssignOp() [|| {} | {} ||] AssignAct [|| {} | {z} ||] z := 1
 end
 ~~~~