Nick Battle

I've updated VDMCheck in anticipation of the backport changes for 2.0.4. This was mostly straightforward, since the checks from the 3.0 schema for the new XML files could be re-used....

See https://github.com/jonaskrask/vdm-vscode/issues/62 We need to separate the condition from the logged trace value and do multiple checks.

Measures for inline function definitions don't work

1

Consider the following: ``` f: nat -> nat f(x) == let g: nat -> nat g(a) == if a = 0 then 0 else a + g(a-1) pre a >...

The following produces a stack overflow: ``` types T = R; R = T; Parsed 1 module in 0.054 secs. No syntax errors java.lang.StackOverflowError Error 3050: Type 'T' is infinite...

Consider the following: ``` f[@T]: @T * @T -> nat f(a, b) == a + b pre is_real(a) and is_real(b); ``` This is type clean, and allows a pair of...

Checking for alias variables and variability

10

FMI Standard issue 2.0.1 included a clarification paragraph to explain the rules regarding the variability setting of collections of aliased variables. VDMCheck was enhanced to make this new check, and...

Allow nested block comments in parser

8

This was recently raised on VDMJ (via VDM VSCode). It is quite useful to correctly parse nested `/* ... */` style block comments because it means you can comment out...

Correctly colour nested comments in VDM editor

1

This change is linked to issue #774, enabling nested comments. If #774 is accepted, the editor ought to change to correctly colour-code a nested comment. Without such a change, the...

Map domain and range restrictions are over-constrained

1

The set passed to `` operators can be of an arbitrary type. The operator does not have to succeed in limiting the map - it may be that no entries...

Removed hard limit on module initialization

2

This is an issue to reflect the changes, with some amendments, in Simon Fraser's PR #772. I will merge this into ncb/development, which will subsequently be picked up by development...