Type check gives warning for state component if a frame reference is made

[pglvdm]

For a CML model like:

process Test =
begin

state 
  m : map nat to nat:= {|->}

operations

Op(a: nat) r : nat
frame rd m 
pre a in set dom m
post r = m(a)

@ Skip

end

one gets a warning that the state component "m" is hidden when the "frame" line is present. However, this is wrong since the "m"s both refer to the same state component. Thus this warning should be removed.

[lausdahl]

Can you check this in overture as well i think that this is standard VDM and not CML.

Sent from my iPhone

On 29/05/2014, at 08.54, pglvdm notifications@github.com wrote:

For a CML model like:

process Test = begin

state m : map nat to nat:= {|->}

operations

Op(a: nat) r : nat frame rd m pre a in set dom m post r = m(a)

@ Skip

end one gets a warning that the state component "m" is hidden when the "frame" line is present. However, this is wrong since the "m"s both refer to the same state component. Thus this warning should be removed.

— Reply to this email directly or view it on GitHub.

[pglvdm]

In standard VDM-SL the same model looks like:

state St of 
  m : map nat to nat
init m == m = mk_St({|->})
end

operations

Op(a: nat) r : nat
ext rd m 
pre a in set dom m
post r = m(a)

but here the warning does NOT appear. So this is purely a CML issue.

[lausdahl]

The example should look like this in VDM++ which matched the process in CML:

 class Test 

instance variables
  m : map nat to nat:= {|->}

operations

Op(a: nat) r : nat
ext rd m 
pre a in set dom m
post r = m(a)

end Test

but it also doesn't report the warning.

[lausdahl]

Why are we checking if an ext rd m definition is duplicated against other definitions. Shouldn't it be enough to check that no two clauses refer the same state and that the states exists. The current implementation relies on ext rd m being lookup to an assigment definition and not an instance variable definition (which actually is the one that has the name) if the instance definition is found instead (as in COMPASS) a duplicate warning is issued from FlatCheckedEnvironment :

if (def != null && def.getLocation() != n1.getLocation()
                        && def.getNameScope().matches(scope))
{
warning...
}

since the external definition is created with the name of what it resolved to then this actually should create a warning.

[pglvdm]

I agree that it seems that the extra dublication test is not needed.

[lausdahl]

See https://github.com/overturetool/overture/issues/353