Scope rules for assignments

[joey-coleman]

The following bug was originally reported on Sourceforge by nick_battle, 2009-06-09 10:18:21:

Title:

Scope rules for assignments

Date:

09/06/09

Raised By:

Nick Battle

Overview:

This is to seek clarification on the rules for the resolution of names on the left hand side of an assignment statement. Currently, VDMTools uses different scope rules for updatable state names compared to read-only names, and this is used by some specifications - notably the POP3 sample model for the VDM++ Book, though VDM-SL is the same.

Background:

VDMTools ignores non-state names in scope when locating the variables on the left of an assignment. For example, you can write "x := x", which can update a state variable "x" (on the left) with a local value "x" (on the right).

Similarly, names on the left of an assignment which are not being updated can see non-state names, so you can write "x(x) := x" which will use the state variable for the left-most "x", and the local variable for everything else.

This applies when updating any kind of state: VDM-SL "state" definitions, as well as local "dcl" defintions and instance variables, though if state names hide other state names, the scope rules are as you would expect.

You can also qualify a variable name with a backtick, such as "A`x := x", which is perhaps clearer, but VDMTools still confuses the scope here, using different rules at type checking compared to runtime (see example attached).

This is used in the POP3 model in some constructors to overcome the common naming problem when initializing instance variables from similarly named constructor parameters:

instance variables

id : seq of char; cmds : seq of POP3Types`ClientCommand; mc : MessageChannel;

public POP3TestSender: seq of char * seq of POP3Types`ClientCommand * MessageChannel ==> POP3TestSender POP3TestSender(id, cmds, mc) == ( id := id; cmds := cmds; mc := mc; );

It also occurs in the "loose.vdm" specification in VDM-SL:

state Sigma of ... fn_m: map ASName to (ASPattern * AS`Expr) ... end

InstallFnDefs: map ASName to ASExplFnDef ==> () InstallFnDefs(fn_m) == fnm := {nm |-> mk(fn_m(nm).pat, fn_m(nm).body) | nm in set dom fn_m};

The leftmost fn_m in the assignment refers to the state; the one within the body refers to the parameter (which is a different type in this case).

And it also occurs in one of the CSK tests, cgip/PP/methods/full/full-01.vpp:

public m1: real * real ==> real * real m1(i,j) == ( Ai := i; Aj := j; return mk_(Ai,Aj) ) pre i < j;

Here the intention to update the instance variable is made clearer using the backtick notation.

VDMJ reproduced this scope functionality (at some cost) in the belief that it was correct, but recent conversations with Peter lead me to suspect that this may simply be a VDMTools bug.

The attached specification produces the same results in VDMTools and VDMJ, apart from the An(An) cases, where VDMTools takes the inner An to be local for type checking, but state at runtime (and so fails). In these cases VDMJ uses the state for the outer An and the local for the inner A`n, both at runtime and for type checking. Both tools give scope hiding warnings in most cases, though VDMTools does not for the simple "n(n) := n" case.

Recommendation

This is a bug. Name resolution should not take account of whether the name is being updated, and so statements like "x := x" should either be legal and do nothing (for state) or be illegal (for non-state).

The backtick syntax is important for superclass member resolution (as in obj.Aop(args)), but ordinarily it should not affect simple name scope lookup (ie. locals in class A are implicitly Aname and can be referred to as such).

Consequently, there is no way of referring to a state variable that is hidden by a local.

Although the POP3 sample model depends on this, it is not used in the published text of the VDM Book, as far as I can see (it is in the online version of the model on the website). I cannot assess the wider impact of changing this, but I would hope that it is minimal - specifications that need to change will give type checking errors if they depend on the functionality.

[joey-coleman]

Comment by nick_battle, 2009-06-09 10:18:21:

Scope example

Files were attached:

• scope.vpp (513 bytes)

[joey-coleman]

Comment by shinsahara, 2009-08-02 10:20:19:

I think that experienced programmers in Real World don't use this style. But, beginners fall into great confusion. So, we have to obey Nick's opinion.

[joey-coleman]

Comment by pglvdm, 2009-08-08 15:13:45:

Well although I think that some programming languages such as Java use principles where the names used in a parameter list are also used on the left-hand-side of assignments inside such operations I also agree with Nick's suggestion to do as Nick suggests.

[joey-coleman]

Comment by nick_battle, 2009-08-10 07:32:20:

Java will let you say things like "this.p = p" - which we would represent as "self.p = p", but that isn't permitted in VDM++ either (I think it's because of the grammar of a "state designator". If you remember, I tried to make VDMJ's assignments use "object designators" on the LHS, but that was objected to for some reason, so I changed them back to state designators).

[joey-coleman]

Comment by ardbeg1958, 2009-09-06 10:31:24:

This is a bug. Surely it affects on my current translation work :)

[joey-coleman]

Comment by nick_battle, 2009-09-07 09:47:45:

Moving to discussion phase after no negative LB comments.

[joey-coleman]

Comment by nick_battle, 2009-11-02 13:19:30:

Changed to Execution, after LB NM on 1st November. This is a bug, and will be fixed in current tool versions.

[joey-coleman]

Comment by nick_battle, 2009-11-19 15:27:02:

Implemented in VDMTools 8.2.1b. Closing issue as completed.

[joey-coleman]

Comment by sunewolff, 2012-09-07 08:34:09.984000:

• vdmtools_implementation: --> Available in 8.2.1b
• vdmj_implementation: --> VDM-SL, VDM++, VICE
• no: --> 2803420

[joey-coleman]

Comment by nick_battle, 2013-06-14 15:26:26.831000:

• assigned_to: Nick Battle
• LRM updated: --> False