You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
VDM uses 1-relative sequence indexes, but it is a common mistake for people to write seq(0) when they mean seq(1). This should give an error in the type checker; currently the type checking is clean and it fails at runtime. So for example:
values
S = [1,2,3,4];
T = S(0);
That produces no TC errors, but at runtime (initialization here) you get "Error 4058: Value 0 is not a nat1".
The text was updated successfully, but these errors were encountered:
Parsed 1 module in 0.103 secs. No syntax errors
Error 3056: Sequence application argument must > 0 in 'DEFAULT' (test.vdm) at line 3:9
Type checked 1 module in 0.146 secs. Found 1 type error
Bye
VDM uses 1-relative sequence indexes, but it is a common mistake for people to write seq(0) when they mean seq(1). This should give an error in the type checker; currently the type checking is clean and it fails at runtime. So for example:
That produces no TC errors, but at runtime (initialization here) you get "Error 4058: Value 0 is not a nat1".
The text was updated successfully, but these errors were encountered: