Releases: nickbattle/vdmj
4.4.0 LSP/DAP Server Support
This release adds Language Server Protocol (LSP) and Debug Access Protocol (DAP) support to VDMJ so that it can be driven from any of several UI client that supports these protocols. The changes are being developed and tested in parallel with the VDM extension for VS Code, available here.
There is more detail about how to use LSP itself in the README for the LSP sub-project.
When snapshots are available, they will be published below. Note that all jars within the VDM suite now have the same 4.4.0-SNAPSHOT version, though individual files may be released as bugfix builds (the -YYMMDD suffix).
Released as 4.4.0 on 20/11/20.
4.3.0 Annotations
Annotations are introduced in VDMJ version 4.3.0 as a means to allow a specifier to affect the tool’s
behaviour without affecting the meaning of the specification. The idea is similar to the notion of
annotations in Java, which can be used to affect the Java compiler, but do not alter the runtime
behaviour of a program. See AnnotationGuide.pdf for full details.
VDMJ provides some standard annotations, but the intent is that specifiers can create new
annotations and add them to the VDMJ system easily.
Annotations are added to a specification as comments, either block comments or one-line comments.
This is so that other VDM tools will not be affected by the addition of annotations, and emphasises the
idea that annotations do not alter the meaning of a specification.
An annotation must be present at the start of a comment, and has the following default syntax:
‘@’, identifier, [ ‘(‘, expression list, ‘)’ ]
So for example, an operation in a VDM++ class could be annotated as follows:
class A
operations
-- @Override
public add: nat * nat ==> nat
add(a, b) == ...
Or the value of variables can be traced during execution as follows:
functions
add: nat * nat +> nat
add(a, b) ==
/* @Trace(a, b) */ (a + b);
Annotations are always located next to another syntactic category, even if they do not affect the
behaviour or meaning of that construct. In the examples above, the @Override annotation applies to
the definition of the add operation, and the @Trace annotation applies to the expression a+b.
Specific annotations may limit where they can be applied (for example, @Override only makes sense
for operations and functions in VDM++ specifications), but in general annotations can be applied to the
following:
• To classes or modules.
• To definitions within a class or module.
• To expressions within a definition.
• To statements within an operation body.
In each case, the annotation must appear in a comment, by itself, before the construct concerned.
Multiple annotations can be applied to the same construct, and may be interleaved with other textual
comments, but each annotation must appear in its own comment.
Annotations can be used to affect the following aspects of VDMJ's operation:
• The parser (for example) to enable or disable new language features.
• The type checker (for example) to check for overrides or suppress warnings
• The interpreter (for example) to trace the execution path or variables' values
• The PO generator to (for example) skip obligations for an area of specification.
Note that none of these examples affect the meaning of the specification, only the operation of the
tool. Although it would be possible to create an annotation to affect a specification's behaviour, this is
strongly discouraged.
A global flag can be set by an "-annotations" command line argument, or the "set" command. This flag
controls whether the comments in a specification are parsed for annotations. It defaults to false, so
unless the command line switch or set command is used, no annotation processing will be performed.
If the set command is used from within VDMJ, the specification must be reloaded to parse the
comments:
> set
Preconditions are enabled
Postconditions are enabled
Invariants are enabled
Dynamic type checks are enabled
Pre/post/inv exceptions are disabled
Measure checks are enabled
Annotations are disabled
> set annotations on
Specification must now be re-parsed (reload)
> reload
> ...
VDMJ includes some standard annotations. They are provided in a separate jar file which needs to be
on the classpath when VDMJ is started. If the jar is not on the classpath, annotations will be silently
ignored. The standard annotations perform the following processing:
• @Override is like the Java annotation of the same name, used in VDM++ functions and operations
• @Trace is used to print variable values during execution
• @NoPOG is used to suppress PO generation for a section of the specification
• @Printf is equivalent to IO'printf, except it can be used in functions as well as operations
• @OnFail is the same as @Printf, but it only produces output if the (boolean) expression after it fails
• @Warning is used to suppress specific warning messages
Users are encouraged to write their own annotations. Full details on how to do this are in the AnnotationGuide.pdf.
A new command line option, -strict has been added to this release, which highlights (with warnings) where a specification is taking advantage of lenient parsing rules. VDMJ does not precisely follow the rules in the grammar in some places - for example, the grammar insists that any module imports appear before exports, but the VDMJ parser will allow them in either order. This causes problems when specifications are ported to other tools, which may follow the grammar more strictly (eg. VDMTools, though that is also lenient in places). Using the -strict option highlights potential problem areas. The new warnings are as follows:
5022, "Strict: expecting semi-colon between exports"
5023, "Strict: expecting semi-colon between imports"
5024, "Strict: order should be imports then exports"
5025, "Strict: expecting 'exports all' clause"
5026, "Strict: order should be inv, eq, ord"
5027, "Strict: order should be inv, init"
5028, "Strict: expecting semi-colon between traces"
5029, "Strict: unexpected trailing semi-colon"
It is sensible to use the -strict flag for all new specifications. The warnings that it currently raises will be converted to errors in a subsequent release (though with a -lenient flag to be backward compatible).
4.3.0 Build 190217, Initial release
4.3.0 Build 190306, Added -strict flag and parser warnings
4.3.0 Build 190309, Corrected a bug with trace expansion
4.3.0 Build 190314, Fixed type bind expansion with invariants and annotation expression parsing
4.3.0 Build 190318, Fixed type checking errors for operation return values
4.3.0 Build 190319, Fixed error with mixed sets of ordered and non-ordered types
4.3.0 Build 190320, Improved type checking for polymorphic types
4.3.0 Build 190619, Fix annotated expression parsing to bind tightly, added @OnFail to annotation2
4.3.0 Build 190704, Fix warning in multiple binds of the same name
4.3.0 Build 190919, Fix PO for non-nil ordered comparison expressions
4.3.0 Build 190927, Fix expression annotation parsing of applicators
4.3.0 Build 191001, Fix bug with type imports not matching exports
4.3.0 Build 191015, Fix bug regarding taking nat values of 0 state variables
4.3.0 Build 191110, Fix bug with recursive record types and change POM to Java 1.7
4.3.0 Build 191117, Fix bug with specification statement parsing
4.3.0 Build 191128, Fix bug with high precision literals (-P build only)
4.3.0 Build 191130, Added better stack overflow handling
4.3.0 Build 191206, Improved annotation parser error detection
4.3.0 Build 191212, Correctly identify reserved prefixes (inv_, pre_ etc) as errors
4.3.0 Build 191216, Add warning for complex polymorphic type usage
4.3.0 Build 191217, Corrected some precision settings for HP library functions
4.3.0 Build 191218, Added #ifndef processing
4.3.0 Build 191223, Added PO generation for mutually recursive functions
4.3.0 Build 200103, Correction to mutual recursion detection/POs for VDM++
4.3.0 Build 200106, Improved exit detection and recursive loop efficiency
4.3.0 Build 200107, Correct seq comprehensions to allow type binds
4.3.0 Build 200315, Add defence to "eq" function for nil values
4.3.0 Build 200401, Small changes to support LSP/DAP server
4.3.0 Build 200426, Added @Warning annotation and update Guide
4.3.0 Build 200504, Small fixes for LSP
4.3.0 Build 200505, Fix for stop/quit actions while debugging.
4.3.0 Build 200512, Some LSP fixes.
4.3.0 Build 200515, Moved @OnFail to annotations, fixed IO library, add commands to LSP
4.3.0 Build 200516, Added set and quit commands
4.3.0 Build 200604, Enable breakpoints during initialization, including via LSP
4.3.0 Build 200605, Added init command to LSP
4.3.0 Build 200610, Fixed a bug with recursive @T types
4.3.0 Build 200611, Updated annotations jars
4.3.0 Build 200618, Added "script" command and updated breakpoint handling and User Guide
4.3.0 Build 200711, Tidy visitor framework and add section to Design Spec
4.3.0 Build 200804, Complete tidy of visitor framework.
4.3.0 Build 200810, Convert getAllValues and instantiate method to visitors.
4.3.0 Build 200813, Fixed bug #27, error in RecordValue's compareTo.
4.3.0 Build 200828, Fixed bug #26, stack overflow with recursive type resolutions.
4.3.0 Build 200907, Fixed bug #28, issuing warnings for op calls in let statements.
4.3.0 Build 201004, Fixed bug #29, warning for function value comparisons.
4.3.0 Build 201008, Added vdmj.mappingpath for annotations and added source jar generation to POM.
4.3.0 Build 201023, Correct PO bug for return statements with no expression argument.
4.3.0 Build 201109, Final release of 4.3.0 - moved all jars to 4.3.0(-P)
(Only the last 5 build jars will be retained)
4.2.0 Measure Expressions
This release contain the changes for RM42, which makes changes to measure clauses. This is also the first release that contains no new Fujitsu IPR.
Measure clauses can now contain a simple expression, using the same parameter variables as the main function, very much like a precondition. Such expressions also cause a function to be created, called measure_f (similar to the creation of pre_f). This function will have the same parameters as the main function, but return a nat or nat tuple, depending on the type of the measure expression.
For example, a measure can now be written as follows:
sum: seq of nat -> nat
sum(s) ==
if s = [] then 0 else hd s + sum(tl s)
-- measure m; -- measure can be a function
measure len s; -- or the expression can now be added inline
m: seq of nat -> nat
m(s) ==
len s;
If you use an inline measure, a function is created:
> env
sum = (seq of (nat) -> nat)
m = (seq of (nat) -> nat)
measure_sum = (seq of (nat) +> nat)
> p measure_sum([1,2,3])
= 3
Executed in 0.016 secs.
> p sum([1,2,3])
= 6
Executed in 0.007 secs.
If you have a complex recursive function that you have not yet written a measure for, or that cannot sensibly have a measure defined, you can suppress the warning by defining a measure as "is not yet specified":
sum: seq of nat -> nat
sum(s) ==
if s = [] then 0 else hd s + sum(tl s)
measure is not yet specified; -- suppress warning about missing measure
4.2.0 Build 180125, Initial release
4.2.0 Build 180126, Correction for type check of subtractions
4.2.0 Build 180317, Fix for lambda values with polymorphic types
4.2.0 Build 180405, Correction for ext rd/wr name/scope lookups
4.2.0 Build 180608, Small correct to POs with old variable identifiers
4.2.0 Build 180705, Experimental annotations feature (see the -annotations jar)
4.2.0 Build 180721, Added extra -verbose output and optimized initialization
4.2.0 Build 181106, Corrected narrow_ execution and reserved word detection
4.2.0 Build 181110, Absorb ContextExceptions during union value conversions
4.2.0 Build 181114, Correct VDMJC Manifest to use the right main class.
Fujitsu's VDMJ
This tag was created to mark the point at which vdmj and FJ-VDMJ diverge. Changes in vdmj after this point are not Fujitsu's IPR. The extent of Fujitsu's IPR is captured in a separate FJ-VDMJ repository for convenience.
4.1.0 Type Ordering and Equality Release
This release implements RM#39, which adds ordering and equality clauses to type definitions. See overturetool/language#39. The change also adds new proof obligations to guarantee strict ordering. For example:
types
S = seq of char
ord a < b == len a < len b -- Ordered by length
eq a = b == len a = len b; -- Equality by length
values
V = let s : set of S = { "nine", "four hundred", "twenty", "six", "three", "sixteen" }
in [ x | x in set s ];
> p V
= ["six", "nine", "three", "twenty", "sixteen", "four hundred"]
Executed in 0.012 secs.
>
> p ord_S("very long", "short")
= false
Executed in 0.004 secs.
>
> p ord_S("short", "very long")
= true
Executed in 0.011 secs.
>
> p eq_S("abc", "def")
= true
Executed in 0.004 secs.
>
> p eq_S("a", "abc")
= false
Executed in 0.003 secs.
>
> pog
Generated 2 proof obligations:
Proof Obligation 1: (Unproved)
S: equivalence relation obligation in 'DEFAULT' (test.vdm) at line 4:8
(forall x:S & eq_S(x, x)) and
(forall x, y:S & eq_S(x, y) => eq_S(y, x)) and
(forall x, y, z:S & eq_S(x, y) and eq_S(y, z) => eq_S(x, z))
Proof Obligation 2: (Unproved)
S: strict order obligation in 'DEFAULT' (test.vdm) at line 3:9
(forall x:S & not ord_S(x, x)) and
(forall x, y, z:S & ord_S(x, y) and ord_S(y, z) => ord_S(x, z))
>
In addition, new checks have been added to the type checker to identify cyclic dependencies between initializers. In previous releases, these would only be identified when the specification was initialized, typically resulting in "unknown name" errors. Most of these errors are now identified during type checking, though complex cases still may get through. Some care has been taken not to produce false positive errors, but if cyclic checking does produce spurious errors, it can be suppressed by setting the Java property "skip.cyclic.check".
Error 3355: Cyclic dependency detected for A`F in 'A' (test.vpp) at line 3:5
Cycle: [A`F, A`f1(nat1), A`f2(nat), A`F]
There is also a new command line option, -verbose, which causes more information about VDMJ processes to be displayed:
Parsed 1 module in 0.086 secs. No syntax errors
Loaded ast-tc.mappings in 0.185 secs
Mapped 66 nodes with ast-tc.mappings in 0.005 secs
Type checked 1 module in 0.011 secs. No type errors
Loaded tc-in.mappings in 0.113 secs
Mapped 120 nodes with tc-in.mappings in 0.003 secs
Initialized 1 module in 0.133 secs.
Interpreter started
>
4.1.0 Build 170707, Add equality and ordering, plus cyclic dependency checking
4.1.0 Build 170710, Bug fixes for inter-module ordered type usage, and ordered value initializers
4.1.0 Build 170712, Some bug fixes for cyclic dependency checking
4.1.0 Build 170724, Bug fix for cyclic dependency checking via renamed imports
4.1.0 Build 170726, Updated docs package for 4.1.0
4.1.0 Build 170803, Improved debugger stepping for func/op returns
4.1.0 Build 170809, Fixed trace debugging problem
4.1.0 Build 170830, Better reporting of import/export type mismatches
4.1.0 Build 170919, Added ValueFactory for native Java methods
(Note that unchanged jar files can be retrieved from earlier releases).
4.0.0 Re-structure Release
This release does not add any new functionality, but it has a large scale restructuring of the internals of VDMJ.
Version 3 and earlier of VDMJ have a monolithic structure, where the code for each type of analysis on a node type (for example, type checking, execution and PO generation) is included in the single AST node of that type. Version 4 onwards splits the functionality of the different analyses into separate classes. Before an analysis is performed, the system generates a new tree of objects specifically for that analysis (once only). This means we can keep new analyses independent of existing code and the AST, but without using visitors, which can become cumbersome for very large ASTs.
4.0.0 Build 161219, Alpha release for testing.
4.0.0 Build 170105, Correction for international charsets
4.0.0 Build 170113, Performance tweak for union/pattern processing
4.0.0 Build 170215, Correction to function instantiation argument processing
4.0.0 Build 170308, Improved support for multi-threaded debugging
4.0.0 Build 170420, Added VDMJC client and DBGP protocol handling
4.0.0 Build 170604, Fixed a pure op bug with class invariants
4.0.0 Build 170704, Added some cyclic dependency checking to the type checker
3.2.0 Set1 and sequence binds
This release includes new functionality for RMs 35 and 36, introducing the "set1" type, and "in seq" sequence binds.
3.2.0 Build 160721, Release of version 3.2.0
3.2.0 Build 160914, Improvement to typechecking of traces.
3.2.0 Build 160921, Correction to function value assignments.
3.2.0 Build 161011, Correction to compose function cloning.
3.2.0 Build 161214, Check for duplicate access keywords in parser.
3.1.1 New Traces Release
This release makes a significant improvement to the way combinatorial tests are expanded from VDM trace definitions, though externally the syntax and semantics of traces themselves have not changed.
The previous 3.0 release expands both trace expressions and all the test sequences themselves before starting to execute the tests. The new 3.1 release expands the trace expressions as before, but the test sequences are created iteratively. This means that the Java heap consumption is drastically reduced, which means that far larger traces can be expanded. For example, it is now easily possible to produce the full expansion of the XO (noughts and crosses) model and execute the tests (over 362,000 of them), even with a 32-bit JRE.
There are also corrections to prevent memory leaks that could occur as tests were expanded and executed. So now, if the trace will expand - ie. if the tests start executing - then it is very likely that the entire test suite will execute without running out of heap.
The iterative nature of the test expansion does have some consequences for shaped pattern reduction, however. Since the tests are not now all expanded before the tests start, it does not know how many different shapes of test exist. The filtering must preserve at least one test of every shape, so it does this by always allowing the first test of a new shape to run. Subsequent tests of the same shape may or may not run, depending on the degree of reduction. The 3.0.1 release was able to examine all of the tests before filtering by shape, so it could select them more randomly. But this seems like a small price to pay for being able to run far larger traces.
If you ask for a specific test number to be executed or debugged, the iterative expansion has to produce (but not execute!) all of the tests prior to the one requested. This is slower than the previous 3.0 release, which expanded all of the tests first and could go directly to the one requested. But of course it was slower to expand all of the tests at the start, so this is not a significant difference.
There are some very minor changes to the trace output. For example:
Generated 150 tests, reduced to 2, in 0.021 secs.
Test 61 = op(7)
Result = [(), PASSED]
Test 149 = op(17)
Result = [(), PASSED]
Excluded 148 tests
Executed in 0.116 secs.
All tests passed
Firstly, it shows both the number of tests generated (the total) as well as the size of the reduced set, and the time taken to expand the tests. Secondly, the tests are numbered as they would appear in a full run (in 3.0, the reduced tests were renumbered from 1). And lastly, the number of excluded tests is now listed at the bottom (this includes any that are stem filtered as well as reduced).
It is also now possible to execute a contiguous range of tests, rather than just one or everything. So the runtrace command has the following syntax:
runtrace <name> [start_test [end_test]]
All the tests between start_test and end_test (inclusive) are executed. Just giving start_test runs one test; giving an end_test of "end" runs all the tests from start to the end of the expansion.
It is also possible to run all of the traces in a named module/class or all traces with the following command:
runalltraces [<name>]
3.1.1 Build 151222, released
3.1.1 Build 151229, performance improvements to trace iterators
3.1.1 Build 151230, added savetrace command and updated documentation
3.1.1 Build 160101, added seedtrace command
3.1.1 Build 160106, fixed record value comparison, bug #6
3.1.1 Build 160112, fixed static instance variable type checks, bug #7
3.1.1 Build 160120, fixed problem with inheritance and overloading, bug #8
3.1.1 Build 160122, fixed problem with abstract class detection, bug #9
3.1.1 Build 160126, fixed problem with class union type checking, bug #10
3.1.1 Build 160201, fixed problem with union pattern matching, bug #11
3.1.1 Build 160203, fixed problem with ValueListenerLists growth, bug #12
3.1.1 Build 160211, fixed second problem related to bug #9
3.1.1 Build 160221, fixed problem with variable name shaped reduction
3.1.1 Build 160225, fixed problem with POs of record unions, bug #13
3.1.1 Build 160303, fixed problem with type check of records, bug #14
3.1.1 Build 160304, fixed more general problem with multi-type checking, bug #15
3.1.1 Build 160317, fixed problem with sequence comprehensions, bug #16
3.1.1 Build 160320, more performance improvements to trace iterators
3.1.1 Build 160324, improvement in function instantiation checks, bug #17
3.1.1 Build 160404, detect use of type parameter variables, bug #18
3.1.1 Build 160408, added runtrace ranges.
3.1.1 Build 160409, experimental assertVDM addition to VDMJUnit
3.1.1 Build 160410, improvement to trace syntax error reporting
3.1.1 Build 160411, added message parameter to assertVDM methods
3.1.1 Build 160412, bring VDMJC and VDMJUnit versions to 3.1.1 in line with VDMJ
3.1.1 Build 160415, some corrections to check of exports, imports and measures with type parameters.
3.1.1 Build 160425, correct arithmetic operations for very large values.
3.1.1 Build 160426, fix problem with measures that use UpdatableValues
3.1.1 Build 160511, fix a problem with UpdatableValue re-use
3.1.1 Build 160519, add trace expansion time to runtrace command
3.1.1 Build 160626, fix some problems with polymorphic function type checking
3.1.1 Build 160603, fixed some type checking errors with module exports
3.1.1 Build 160628, added "runalltraces" command for convenience
3.1.1 Build 160705, fixed problem with struct exports, fixes #19
3.0.1 Bug Fix Release
3.0.1 Pure Operations Release
This is the first release to be made via GitHub. It contains draft type-checking and runtime changes for the RM#27 "pure operations" change.