Skip to content
Pre-release

@nickbattle nickbattle released this Feb 17, 2019 · 30 commits to master since this release

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

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

Assets 13

@nickbattle nickbattle released this Jan 25, 2018 · 158 commits to master since this release

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.

Assets 14
Pre-release

@nickbattle nickbattle released this Oct 1, 2017 · 201 commits to master since this release

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.

Assets 2

@nickbattle nickbattle released this Jul 7, 2017 · 234 commits to master since this 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).

Assets 13

@nickbattle nickbattle released this Dec 19, 2016 · 343 commits to master since this 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

Assets 13

@nickbattle nickbattle released this Jul 21, 2016 · 356 commits to master since this release

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.

Assets 11

@nickbattle nickbattle released this May 11, 2016 · 447 commits to master since this 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

Assets 19
Pre-release

@nickbattle nickbattle released this Dec 16, 2015 · 475 commits to master since this release

This release is just a rollup of the most recent problems.

  • Problem with set pattern matching #4 (release 3.0.1-12 and -13)
  • Problem matching empty map patterns #5 (release 3.0.1-14)

The updates usually only affect the two "vdmj" jars, rather than vdmjc or vdmjunit.

Assets 9
Nov 27, 2015
Merge remote-tracking branch 'origin/master'
Nov 24, 2015
Fix a problem with set pattern matching, fixes #4
You can’t perform that action at this time.
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.