OpenJML 0.21.0-alpha-0

Publishing release 0.21.0-alpha-0.

This is an alpha release of OpenJML for Java 21. Though it is still an alpha, it is expected to be an improvement over the most recent Java 17 release, which is no longer actively supported.

OpenJML 0.17.0-alpha-15

Publishing release 0.17.0-alpha-15

Improvements to type annotations for NonNull and Nullable
Corrected bugs in documented behaviors and corresponding tests

OpenJML 0.17.0-alpha-14

Publishing release 0.17.0-alpha-14

Changed type names to backslash version
Fixed some technical debt
-- aligned modifiers with JML -- immutable
-- cleaned up feasibility checking and proof splitting and language variants
-- fixed bugs in naming conflicts

OpenJML 0.17.0-alpha-13

Publishing release 0.17.0-alpha-13

• Progress on revising how frame conditions are handled, especially for recursion
• Implementing helper fields
• Added arithmetic failure modes and --show-summary
• Refactoring internals and fixing miscellaneous bugs

OpenJML 0.17.0-alpha-12

Publishing release 0.17.0-alpha-12.

Initial implementation for reads clauses.
Addition of switch expressions
Fixed exception specs to be nullable
Fixed unchecked warnings
Tutorial and Makefile cleanup
Bug fixes.-- e.g. crash in Flow, problem with length fields
Addition of --arithmetic-failure, --show-summary

OpenJML 0.17.0-alpha-11

Publishing release 0.17.0-alpha-11.

Restored basic RAC to working order. There are still crashes and bugs with model fields and junitNG tests, but all demo cases and most test examples of RAC now work as expected.

OpenJML 0.17.0-alpha-10

Publishing release 0.17.0-alpha-10

• Significant refactoring to fit with OpenJDK symbol entering phase, with better handling of nested classes and model classes and members
• Implementation for recursive model fields
• Updating to double hyphen options
• RAC not (yet) operational

OpenJML 0.17.0-alpha-9

Publishing release 0.17.0-alpha-9

Up to date with openjdk-17-GA
Partial work on locset and dynamic frames
Simple RAC is now working (without model methods, model fields or invariants)

OpenJML 0.16.0-alpha-8

Publishing release 0.16.0-alpha-8
Fixes to inheritance of frame conditions.

OpenJML 0.16.0-alpha-7

Publishing release 0.16.0-alpha-7.
Issue #754.
Initial implementation of RAC.