KeY-2.12.0 (2023-08-18)

Changes

Breaking changes

• The minimum required JDK version is set to 11.
• This release contains breaking changes for the reloading of older proofs:
  • Integers in specifications are now considered as unbounded (i.e. \bigint, math mode specifiers can be used to deviate from the default).
  • The list of rule sets used by the One-Step-Simplifier has changed.
  • JML assertions are handled as a standalone construct and not as a block contract anymore.

Highlights

• Support for floating points

• Support for JML asserts/assumes as standalone construct (instead of transforming into blockcontracts), Support of \old() in JML asserts

• Support for JML math mode specifiers (and changed default semantics to spec_bigint_math)

• Migration to Github

  • Files for Github Actions
  • Add merge_group event to checks
  • Artiweb: #3047, #3097, #3098, #3101, #3102, #3103
  • Upload HTML test report
  • Dependabot

• Proof slicing extension

• Run the Javac compiler when loading Java code

Features

• Enable JavaDL data types in ghost and model fields
• Change SwitchToIf to create a if-else cascade
• More proof script commands: hide and unhide
• Logging via slf4j
• Suggested automation for seqPerm
• More descriptive names for result variables
• Implement some features of the jml assert wishlist
• ChoiceExpr: En-/Disabling taclets/goal templates using boolean expression
• New rules from the sorting case study
• Overflow checking
• Bring INVISMT to KeY; Refactors SolverTypes
• Redux additions

UI/UX Improvements

• Selection history (back + forward button)
• Generic undo button for user actions
• Expand oss nodes
• Allow user to select any installed LaF
• Un-clutter the context menus in the proof tree view
• Close more dialogs on escape press
• Replay progress display
• Improved taclet error reporting
• Immediately resize proof tree font
• Tooltip for the exloration status label
• Update log button, use Desktop.open instead of edit, fix an exception and log format on windows
• Report location on error in constant evaluation
• Report better error for missing model method
• Proof tree view: Multiple small changes for readability
• Disable exploration tree updates when disabled
• Focus first cell in the taclet instantiation dialog on open
• Clipboard: Replace nbsp from html document selection with normal spaces
• Improve naming in recently used files dropdown

🛠 Maintenance/Internal Changes

• Logging

  • Logging cleanup
  • Housekeeping: Logging

• Code formatting with spotless

  • Check formatting with Spotless
  • Formatted rules
  • Set an import order for Java code
  • Apply Spotless to code base: Source code reformatting (no license headers)
  • Spotless: Don't join manually split lines

• Code-Clean-Ups and Refactoring:

  • Replace the hardcoded SolverType classes by .props files
  • Position information overhaul
  • Remove ServiceLoaderUtil
  • Remove last Eclipse files
  • Code cleanup
  • Miscellaneous cleanups (unused classes removed etc.)
  • Removal of the Eclipse Plugins
  • Remove sonarqube from readme
  • Cleanup: Remove extension of CreatingASTVisitor by MergeRuleUtils.CollectLocationVariablesVisitor
  • Some code cleanup
  • Refactor Java formatter used in the sequent view
  • Overhaul of the Configuration
  • Add possibility to check for unsupported properties keys to SettingsConverter and clean up the class
  • Removal of the Proof Collection Parser

• Dependencies

  • Recoder became part of this repo (Version 0.84 incl. KeY extensions)
  • Update dependencies
  • No dependencies as local jar files
  • JUnit 5
  • Update Checkstyle configuration to latest Checkstyle version
  • Externalization of Interaction Logging
  • Prepare build.gradle scripts for Gradle 8.0

• Performance

  • Performance when switching nodes
  • Autopilot Performance: hasModality
  • Performance: pause tree updates while executing "Set All Goals Below to XX"
  • Avoid creating proof obligations in ProofManagementDialog

• Tests

  • JUnit XML files for optional-tests
  • Add documentation for TestTacletEquality and update oracle
  • Restore Information FlowTests
  • Split testRunAllProofs into two tasks
  • Disable proof_references + symbolic_execution

• Misc

  • Small tweaks to proof script engine
  • Reducing the binary filesize by only including the necessary example files
  • Improve smt solver checking on windows
  • Translating DL contracts to JML
  • Read \profile and \settings once
  • Stop the message about java_profile.jfr
  • Suppress logback message before configuration
  • Support for jdiv and jmod in SMT translation via definitions
  • Add gen folder to gitignore
  • Add Task runWithProfiler to execute key.ui with the Java Flight Recoder
  • Load some (old) proofs with wrong/missing instantiations of \assumes in taclet app
  • Specialized version of RuleContext::getText in TextualJMLAssertStatement::getClauseText
  • Multiplication for rule costs

🐛 Bug Fixes

• Bug fixes from the IdentityHashMap case study

• Remove highlighting artifacts in SequentView with Unicode symbols enabled

• Avoid tooltip NPE for incomplete proof nodes

• Always load correct example on double click

• TokenMgrErr in issue dialogs

• Fix exception when parsing unknown source name in BuildingException

• Solve missing plugin in shadowJar by adding mergeServiceFiles()

• Fix Z3 counterexample generation

• Fix three memory leaks

• Keep original PositionInfo in ForToWhileTransformation

• Check for correct polarity when applying taclets

• Add triggers to textual representations of taclets

• Allow declaration of function symbols in custom key file and to use them in JML via \dl

• Fix leftover files that are not formatted properly

• Fix loop in strategy

• Fix PosInProgram

• Fix file filter for .proof.gz files

• Fixed rule "wellFormedStoreObjectEQ"

• Resolve "Taclet leaves a broken tree after failing to apply"

• Fix potential stack overflow in ExplorationStepsList

• Show message of the chained cause of the exception in IssueDialog

• Ensure that the condition of a JML assert statement is always a formula

• Fix widening casts and boxing of extension primitive types like bigint

• Fix construction of Javac issue dialog

• Fix handling of multiline log messages

• Fix javacc deprecation warning

• Fix ProofTreeView NPE

• Fix program element printing in proof saver

• Fix some positions being offset

• Fix type of Long.MIN_VALUE and Long.MAX_VALUE

• Activate Z3 if no other SMT solver is configured

• Register modifier when parsing JML spec

• Fix set statements (allow expressions on lhs, e.g. for array and field access)

• Fix IllegalArgumentException being thrown from IssueDialog

• Insert JML assume and assert statements in the right order

• Make AbbrevMap::getTerm fulfill its contract and prevent a NPE

• A collection for some (straight forward) of the SonarQube reliability bugs

• Remove space from taclet proof save file name

• Resolve "Parsing exception: undeclared variable in an assignable declaration"

• Fix for heap/permissions/threads example

• Repairing JML interpretation of equality on floats and doubles.

• Further bug fixes: #1664, #1658, #1652, #1679, #1681, #1682, #1678, #1685, #1690, #1706, #1709, #1684, #1711, #1707, #1723, #1598, #3035

---

We like to thank our contributors for this release, namely:

Alicia Appelhagen, Richard Bubel, Lukas Grätz, Christian Hein, Arne Keller, Michael Kirsten, Florian Lanzinger, Wolfram Pfeifer, Mike Schwörer, Benjamin Takacs, Samuel Teuber, Mattias Ulbrich, Alexander Weigl, Julian Wiesler