Nightly Release

What's Changed

Other Changes

• Update LICENSE.TXT to reflect GPL-2.0-only by @FliegendeWurst in #3223
• Post-Release 2.12.0: Backport bug fixes into main by @wadoon in #3242
• Update BSH dependency of recoder by @wadoon in #3250
• Post-Release: Backport Deployment Changes to KeY by @wadoon in #3246
• Post-Release 2.12.0: Java and Version by @wadoon in #3241
• Applying Java 17 refactorings by @wadoon in #3252
• Fix dependency issue in SMT translation by @FliegendeWurst in #3275
• UI: avoid freeze when applying SMT results by @FliegendeWurst in #3255
• Stop automode or exit on SIGINT by @FliegendeWurst in #3249
• updating README.md by @mattulbrich in #3288
• Problem statements in KeY file can now also be a (semi-)sequent by @wadoon in #3283
• Further Refactorings for Java 17+ by @wadoon in #3264
• SMT: add Z3_QF variant by @FliegendeWurst in #3287
• Fix for issue #3158 by @unp1 in #3224
• Some general minor code quality improvements by @unp1 in #3293
• Update beanshell to 2.0b6 by @unp1 in #3294
• Backport of KEY-2.12.1 into main by @wadoon in #3296
• Fix wrong quicksave failed warning by @unp1 in #3298
• Fix for issue #3286: Parsing of rule display names that contain spaces in origin labels by @unp1 in #3306
• Restore TermImpl to package private and strengthen immutability of term and sorts by @unp1 in #3304
• Fix Issue #3186: Model method looses nullability modifiers by @unp1 in #3307
• Revert lazy term index updates by @unp1 in #3312
• Allow origin labels to be switched off completely by @unp1 in #3316
• Proof Slicing: make dependency tracking optional by @FliegendeWurst in #3309
• replace JSR305 annotations with JSpecify by @wadoon in #3290
• A heap indicator in KeY's status bar by @wadoon in #3325
• fix ClassCastException in LogicPrinter by @wadoon in #3326
• Fix JavaDoc errors by @unp1 in #3329
• Fix broken addLabel Method in TermBuilder by @Drodt in #3331
• Heap status extension: proper max. value of progress bar by @FliegendeWurst in #3332
• Fix all warnings reported by ./gradlew javadoc by @unp1 in #3330
• Method names should not be created via VariableRenamer by @unp1 in #3231
• Create a basic CONTRIBUTING.md by @FliegendeWurst in #3333
• Print real condition in if labels by @FliegendeWurst in #3222
• Fix consistency of proof status and tasktree icon by @unp1 in #3344
• Show notification after running macro by @FliegendeWurst in #3269
• Update to Java 21 Runtime for Testing by @wadoon in #3282
• Add help buttons to extension settings by @FliegendeWurst in #3348
• suggesting a pull-request-template. by @mattulbrich in #3018
• A new grammar for configuration by @wadoon in #3099
• Fix (for issue #3347) that node selection gets forgotten when switching between proofs by @unp1 in #3349
• Re-enable check for non-unique taclet names and remove two taclet duplicates by @unp1 in #3359
• Avoid name clashes in rule applyUpdateOnRigid by @tobias-rnh in #3355
• Handle bound variables in SMT unknown translation by @FliegendeWurst in #3263
• Fix update of proof tree in case of filter changes (fixes #3367) by @unp1 in #3368
• Configurable enabled keys for JML condition evaluation by @wadoon in #3373
• Get rid of experimental flag using more fine-grained flags by @wadoon in #3370
• ADTs for KeY by @wadoon in #3161
• Renovation: package.html to package-info.java by @wadoon in #3381
• Fix passing of warnings by @wadoon in #3302
• Proof caching: use dependency graph to increase hit rate by @FliegendeWurst in #3305
• Always sort extension actions in context submenus (+bugfix to allow disabling extensions) by @FliegendeWurst in #3392
• Update README.md (license date and Java version) by @WolframPfeifer in #3412
• Activate the OverloadedOperatorHandler.java for Sequence datatype by @wadoon in #3398
• Solved an issue with row/column numbers in JML Parser by @LennartKleinwort in #3419
• Fix error handling for unknown sorts by @MarcoScaletta in #3428
• Hackathon: error reporting by @FliegendeWurst in #3426
• Fix position info for equality expr errors by @FliegendeWurst in #3429
• Add ADT Destructors by @Drodt in #3420
• JML enabled keys indicator for the Status Line by @wadoon in #3374
• fixes #1533 by @JonasKlamroth in #3423
• Hackeython smt mod by @BookWood7th in #3418
• added checkbox to disable example loader directly in dialog by @JonasKlamroth in #3424
• Generalizing Logic Data Structures by @Drodt in #3357
• Fix startup crash if ~/.key/colors.json is not present by @FliegendeWurst in #3439
• fix smt solver downloader script by @wadoon in #3445
• Update broken link in README.md by @FliegendeWurst in #3444
• Update pull_request_template.md by @mattulbrich in #3446
• Immutable and valid JML set statement by @wadoon in #3400
• Combine equalsMod... methods by @tobias-rnh in #3386
• Introducing a new function symbol seqUpd by @mattulbrich in #3385
• Cleanup of declaration of taclet options by @WolframPfeifer in #3408
• Boyer Moore Majority Vote by @mattulbrich in #3454
• Hackeython/error reporting by @mattulbrich in #3432
• Nicer error message for parse errors by @FliegendeWurst in #3417
• Fixes a StackOverflow when pretty printing a taclet by @unp1 in #3453
• Fix newnames handling for new local vars by @FliegendeWurst in #3438
• Prevent Dependency PO generation for void methods by @Drodt in #3422
• Update dependabot configuration by @wadoon in #3447
• Add key features for the FM tutorial by @wadoon in #3460
• Fixed the path-to-smt-solver bug in windows by @vb213 in #3434

New Contributors

• @tobias-rnh made their first contribution in #3355
• @LennartKleinwort made their first contribution in #3419
• @MarcoScaletta made their first contribution in #3428
• @JonasKlamroth made their first contribution in #3423
• @BookWood7th made their first contribution in #3418
• @vb213 made their first contribution in #3434

Full Changelog: KeY-2.12.2...nightly

KeY-2.12.2 (2023-11-10)

This release contains bug fixes and performance enhancements.

Changes

Performance:

• Z3 is now configurable to use the QF (quantifier-free) theory for problems without quantifiers.

Bug Fixes:

• The pretty printer no longer throws a ClassCastException when printing taclets using schema variables of an array type.
• Nullable and non-null modifiers attached to model methods are no longer lost.
• Term rule indices are now always up-to-date, preventing potential prover crashes.
• The counter-example dialog no longer freezes the GUI, if the example generation fails.
• The actual proof status and proof status icon in the task overview are now consistent after pruning without requiring a manual refresh.

KeY-2.12.1 (2023-10-13)

Changes

Bug fixes

• SMT solvers are properly terminated on timeout
• Proof Macro statistics are kept visible and only count the newly applied rules
• Stop button is disabled after use, re-enabled after stop completes (this is to avoid double activation)
• Fully disable origin tracking if it is disabled
• Proof slicing works even if a cut introduced no new formulas in any branch
• When marking goal(s) as interactive/automatic, proof tree no longer loses expansion state
• Fix proof tree behaviour when toggling goals
• Fix branch selection in caching
• Fix gradle detection of git branch
• Fix unit test
• Fix environments not disposed in tests, keep strategy info visible after applying
• Proof macro: record statistics correctly
• Fix: KeY files with errors cannot be edited

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 T...

KeY-2.10.0 (2021-12-23)

Core

• IMP: New SMT translation (!312), rework of the SMT communication (!381), and smaller fixes (!394)
• IMP: Renovating the KeY parser (!278)
• IMP: Rewrite of the JML parser in ANTLR (!306) with better exception message (!376)
• IMP: JML-Extension: Assert/Assume and *_free for block contracts (!342)
• FIX: Comment attachment in recoder (!399, !401)
• FIX: Collision of auxiliary contract (!396)
• FIX: Path handling of key files (!395)
• FIX: Pruning in closed branches looses rules (!388, #1480)
• FIX: Repaired file information if a directory is opened in KeY (!386, #1530)
• FIX: Proof loading in the CLI (!385)
• FIX: Invalid URLs under Windows (#1504, !264)
• FIX: lost error messages due to MalformedURLException (!290, #1529)
• FIX: catch headless to make key --auto runnable again (!382)
• FIX: \singleton of a non-location (e.g., \singleton(3)) now raises an error (!377)
• FIX: Completeness gap for array types (!367, #1566)
• FIX: add loop scope unwind (!326)

UI

• IMP: A better dialog for warnings (!374)
• IMP: Performance tuning and fixes for ProofTree (!391)
• IMP: Enables selection of proof in Proof Differences view (!256)
• IMP: Better SourceView Tooltip (!379)
• IMP: Add setting to disable load examples dialog window (!368)
• IMP: Enable syntax highlighting for JML starting with annotation markers (!325)
• FIX: make proof to load from bundle selectable (!237)
• FIX: Escaping comma when saving bookmarked filenames of KeYFileChooser (!387, #1551)
• FIX: make exception dialog able to show files in Jar files (!383)
• FIX: Resolve "SMT Option GUI throws NPE on startup" (!373)

Development

• Enabling of SonarQube in Merge Requests (!323, !378)
• Dependency fixes for Gradle 7 (!372)

We like to thank all the contributor to this release:

Alexander Weigl,
Alicia Appelhagen,
Benjamin Takacs,
Florian Lanzinger,
Jonas Schiffl,
Julian Wiesler,
Lukas Grätz,
Mattias Ulbrich,
Michael Kirsten,
Richard Bubel,
Wolfram Pfeifer

2.8.0 (2020-12-01)

Logic

• NEW: bsum taclets (!96)
• NEW: Taclets for more flexible handling of observer depency (!177)
• NEW: Loop contracts improvements (!188)
• NEW: Loop scopes: a new rule for proving loop invaraints (!313, !326)
• NEW: Support for Annotation Marker in JML (!308)
• NEW: created new file intDiv.key for newly added taclets concerning
  (!182, !171, !180, !157, !152, !144, !141, !135, !98)
• NEW: SMT preparation macro (!165)
• NEW: Completion Scopes (!305)
• FIX: Bugfixing handling of program variables of type "any" and parsing (!133)
• NEW: \infinite_uniton(int x; x >= 0; this[x]) is now available in binder syntax:
  (\infinite_uniton int x; x >= 0; this[x]).
  Old form is deprecated and will be removed in later versions. (!132)
• NEW: Adding "System.arraycopy" with contract to JavaRedux (!137)
• NEW: Explizit excption for nested updates (allowed in the KeY book, unsupported by implementation) (!319)
• FIX: Speed up in saving proofs (!120)
• FIX: Incompleteness issue when rewite taclet was applied and the goaltemplate… (!119)
• NEW: Loop contract (!?, !73)
• NEW: Loading and Storing proofs with compression (gzip) (!12)
• NEW: Saving of proofs (incl. dependening resources) into one file (zip) called "proof bundle" (!237)
• FIX: Fix of inner blocks (!82)
• FIX: KeY read files character-wise, now the file content is cached (!XXX)
• More jml synonyms (!85)
• FIX: user-provided notes are saved within the proof file (!304)
• FIX: Origin labels for user interactions could not be parsed
• FIX: Method signature resolve in JML expressions (!309)

UI

• NEW: Unifying and polishing the user interface (!123):
  • KeY uses a docking framework, including storable/loadable layouts (!189)
  • The settings are concentrated inside one dialog (!189, !266)
  • Adaptable colors and key strokes (!189, !236, !254)
  • Adaptable clutter rules (!7)
  • Key based navigation within the proof tree view (!198)
  • FIX: Handling of regex in search (!199)
  • NEW: Icons !227
• NEW: Heatmaps: Coloring formulae on the sequent based on their change activity (!38, !140)
• NEW: Saving of proof bundles (!148, !310)
• NEW: View of the current source code marking executed parts. (!99, !260, !263, !267, !325)
• NEW: GUI Extension inferface: You can easily plugin new GUI elements.
• NEW: Origin labels tracks the origin of formulae within a sequence (!122, !248)
• NEW: Intraction logging (HacKeYthon'18) brings logging of user interaction
  with exports to Proof Scripts (!84)
• NEW: Proof exploration
• NEW: Favourites in file dialogs (!252)
• NEW: License dialog (!253)
• NEW: View for proof differences based on formula distance matching (!255)
• NEW: Schiffl's search filter (!4)
• NEW: Pre-select previous selected contract in ProofManagementDialog (!287)
• FIX: Parsing of char, integer and long literals (!9, #1446, !214, !196)
• FIX: Collision of heatmap and search colors (!178)
• FIX: Slightly less confusing presentation of SMT solver results (!160)
• FIX: Cluttering with the status line (!244)
• NEW: Allow macro application via keyboard shortcut from tree (!268)
• NEW: Open Java files without considering a classpath (!243)

Scripts

• NEW: Rewrite command (!51)
• FIX: Several fixes and breaking changes: (!153, !146, !145)
• NEW: Improvements to the proof scripts (!314)

Environment

• NEW: Gradle became build tool (!179, !205, !208, !209, !280)
  • Changes to the test infrastructure (!196)
  • Export of maven dependecies
  • New distribution formats: either a FatJar or zip file
• NEW: Quality assessment via sonarqube and sonarcloud (!323)
• Java 11 ready (!47)
  • remove of JavaFX dependencies (!95)
• Integrate tests for well-definedness checks (!87 )

Eclipse

• Support of Eclipse PHOTON (!74)

Seveal small and large bug fixes:

(!331, !297, !296, !293,!290, !288, !286, !284, !277, !276, !273, !272, !271, !270, !265, !264, !234, !228, !227, !225, !224, !222, !219, !213, !212,
!209, !208, !205, !203, !201, !200, !199, !192, !190, !173, !170, !167, !163, !162, !158, !156,
!154, !153, !151, !146, !145, !139, !136, !133, !131, !119, !117,
!108, !99, !92, !83, !82, !81, !78, !77, !75, !73, !71, !70, !69, !68,
!67, !66, !65, !58, !52, !47, !46, !45, !40, !39, !37, !33, !31, !30, !24,
!23, !22, !14, !13, !10, !9, !8, !7, !3, !2)

We like to thank all the contributor to this release:

Alexander Weigl, Carsten Csiky, Dominic Steinhöfel, Florian Lanzinger, Hans-Dieter Hiep, Jelle
Kübler, Jonas Schiffl, Lukas Grätz, Lulu Luong, Mattias Ulbrich, Michael Kirsten, Mihai
Herda, Peter Schmitt, Richard Bubel, Sarah Grebing, Wolfram Pfeifer

KeY-2.6.3 (2017-10-11)

Full Changelog: KeY-2.6.2...KeY-2.6.3

KeY-2.6.2 (2017-04-13)

Full Changelog: KeY-2.6.1...KeY-2.6.2

KeY-2.6.1 (2017-01-31)

Full Changelog: KeY-2.6.0...KeY-2.6.1

KeY-2.6.0 (2016-12-22)

Full Changelog: KeY-2.4.0...KeY-2.6.0