OpenJML 21.0.26

Publishing release 21.0.26

• Fixed issue #955
• Corrected default: pure in specs is not allowed by default
• #956 - added linux+arm64 build of OpenJML and Z3. However this build of Z3 has different behavior than on other platforms, so --esc on linux+arm is not yet functional.

OpenJML 21.0.25 + Language Server, Eclipse and VSCode clients

Publishing release 21.0.25

• Fixes issue #953

• Switches to using OSGI versioning (21.0.25 followed by 21.0.25.a followed by 21.0.26) because that is needed by Eclipse plugins; note this is a different ordering than "semantic versioning"

• This version introduces a LSP-compliant Language Server for OpenJML/OpenJDK, along with two IDE clients: an Eclipse plugin and a VSCode extension, providing typical IDE functionality (error markers, navigation, OpenJML actions) for Java+JML programs. This is an alpha release -- improvements in functionality, UX smoothness, scalability to large files and projects (and bug fixes) are in progress. Comments and suggestions from trial users will be appreciated. Documentation is available at openjml.org.

OpenJML 21.0.24

Publishing release 21.0.24

OpenJML 21-0.23

Publishing release 21-0.23

-- further work on warning categories
-- integration of type annotations and JML nullity, particularly for generic types
-- small bug fixes
-- fixed #932
-- unit test cleanup and refactoring

OpenJML 21-0.22

Publishing release 21-0.22

• Changed modelling of String-based classes to use \string instead of a Java char[ ]
• Implemented warning categories
• additional checking and clarification for purity categories; removed --purity-check
• removed error message after --help=warn and --help=infer
• fixed soundness bug in \not_modified
• Enabled RAC checking of completeness and disjointenss
• Added RAC print statement
• refactored tests: updated to 'verify' messages instead of 'warning' messages
• Fix for #933
• Fixes for shift by literals

OpenJML 21-0.21

Publishing release 21-0.21

Fix for #941 (a behavioral regression from V21-0.20)

OpenJML 21-0.20

Publishing release 21-0.20

-- refactoring and improvement to handling of frames, particularly loop_assigns
-- fixes for #726, #763, #769, #815, #890, #932, #934, #935, #937, #938, #940
-- added --infer option and mechanisms for control of specification inference
-- improved heap tracking for switch statements and expressions
-- improvement to nightly test scripts
-- refactoring and improvement of public scripts and of coverage options
-- refactoring and cleanup of testing

OpenJML 21-0.19

Publishing release 21-0.19

Primarily a bug fix release with added tests

• edits and fixes to the tutorial pages on openjml.org
• lots of small bugs
• updated properties-template
• added tests for parsing
• distinguished verify failures from regular warnings in tests
• refactored mock files
• #816
• #904
• #899
• #854
• #883
• gitbug469
• fixed --splits option
• implemented if (z instanceof X x) [if statements only so far]
• Spec: InputStream, ByteArrayInputStream, FileInputStream

OpenJML 21-0.18

Publishing release 21-0.18

A bug-fix release -- the following issues are closed (some did not need code changes)
#903
#902
#895
#894
#888
#876
#860
#780
#777
#776
#766
#756
#747
#746
#738
#725
#724
#719
#617
#616
#547
#546
#449

OpenJML 21-0.17

Publishing release 21-0.17

Fixed #869
Fixed #893
Fixed #894
Fixed #898
Fixed #899
Fixed #901
Fixed --check-asccessible
Allow clauses after clause groups
Removed --stop-at-parse-error
Changed --quiet to be completely silent
Fixed #511
Fixed #752
Fixed #753
Fixed #761
Fixed #762
Fixed #765