Assignments to the main record should not be allowed

[peterwvj]

Consider the specification below. Overture/VDMJ maintains two versions of the state - one for the entire state (the record value) and one for the record fields. This causes unexpected behaviour when executing A``op() which returns 0. If you evaluate A``op() in VDMTools it yields 4, which makes sense to some extent.

However, Nick pointed me to an old email conversation where it was once agreed that assignments to the main record should not be allowed (e.g. St := mk_St(4)). Therefore, the specification below should report a type error for the assignment statement.

module A

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

operations

op : () ==> nat
op () ==
(
 St := mk_St(4);
 return x;
);

end A