Skip to content

Changelog

2.12.2 (2023-11-10)

This release contains bug fixes and performance enhancements.

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.

2.12.1 (2023-10-13)

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

2.12.0 (2023-08-18)

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

Features

UI/UX Improvements

🛠 Maintenance/Internal Changes

🐛 Bug Fixes

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

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

2.6.3 (2017-10-11)

2.6.2 (2017-04-13)

2.6.1 (2017-01-31)

2.6.0 (2016-12-22)

2.4.1 (2015-02-18)

2.4.0 (2015-02-17)

  • Information flow reasoning
  • Full support for symbolic execution with bitwise operations
  • Improved test case generation
  • Improved user interface
  • Support for CVC4 SMT solver backend

2.2.3 (2014-10-06)

  • Fix concurrency issue introduced in 2.2.2

2.2.2 (2014-07-11)

  • Support for CVC3 version 2.4.1 SMT backend
  • Bug fixes

2.2.1 (2014-05-27)

  • Test case generation using bounded SMT (requires Z3, OpenJML)
  • Bug fixes

2.2.0 (2014-04-29)

  • Counter example generation using bounded SMT (requires Z3)
  • Increased JML support / JML extensions
  • block contracts (extension) / assert statements
  • \min and \max numerical quantifiers
  • changed default semantics of signals_only to include unchecked exceptions
  • model methods (new implementation)
  • old clause (variable binder in contract)
  • nearly everything parseable
  • Verification of a large class of recursive methods
  • generalized variants to all ordered sets
  • Proof obligations for specification well-definedness
  • Term labels
  • Rule triggers (extended taclet syntax)
  • More efficient handling of heap disjointness and heap selects
  • Improved reasoning about bounded sums/products
  • User Interfaces
  • rule focus for inner nodes
  • improved search
  • detailed proof statistics
  • auto save and quick save features
  • keyboard shortcuts
  • Reduced memory footprint
  • A lot of bug fixes
  • Java 8 compatibility
  • Re-implemented .key parser

2.0.2 (2013-09-19)

  • Support for latest versions of Z3 and CVC3
  • Windows 8 compatibility
  • Fix a soundness issue with types and heap access
  • Various bug fixes

2.0.1 (2013-06-19)

  • Bug fixes
  • Incompleteness with Java integer arithmetics
  • Command line mode fixes
  • various other

2.0.0 (2013-04-18)

  • New explicit heap modeling
  • Data types for location sets and heaps
  • The heap is now a special (local) variable
  • Dynamic frames
  • JML extension for dynamic frame specification
  • Re-implementation of JavaCard transactions
  • Verification of (primitive) recursive methods
  • Sequence ADT
  • Nearly complete JML support
  • model fields and methods
  • initially clauses and class axioms
  • measured_by clauses
  • accessible clauses
  • sum and product comprehension
  • the \bigint type, mixed integer semantics
  • weak purity by default
  • reachability predicate
  • \index and \values keywords for enhanced for-loops
  • Escape to dynamic logic from within JML
  • MonKeY batch mode
  • GUI changes
  • new dialog to enter invariants interactively
  • search in sequents and proof trees
  • logical symbols in Unicode
  • Runnable from command line without windowing system
  • Improved integration of SMT solvers
  • SMT-LIB 2.0 backend interface
  • possible to run multiple solvers in parallel
  • support for integer division (Z3 only)

  • 150 bug fixes

  • Discontinued features
  • RTSJ support
  • Test case generation
  • OCL
  • Proof reuse

1.6.5 (2013-01-23)

  • Minor bugfixes
  • Java 7 compatibility

1.6.0 (2010-10-06)

  • Support for Strings
  • Enhanced JML support
  • Improved integration of external SMT solvers
  • Improved "verification-based testing" mechanism
  • Real Time Java (RTSJ) calculus
  • GUI improvements
  • Various bugfixes

1.4.0 (2009-03-25)

  • Unified proof obligation framework
  • sharing of proof obligations across different specification languages
  • unified API for adding new proof obligations
  • same GUI elements used for all specification languages
  • more elegant translation of \old, @pre-like constructs
  • Improved JavaCard DL Specification interface
  • specification of DL invariants
  • Rewrite of JML front-end
  • ghost variables/fields and JML set statement
  • non_null by default
  • \old in loop invariants supported
  • \object_creation(type) in JML assignable clauses
  • New standalone OCL front-end
  • discontinued support for Borland Together integration
  • Java language support enhancements:
  • enum types (partially)
  • inner and anonymous classes
  • enhanced for loop
  • variable method arguments
  • covariant method signature
  • Generation of JML specifications
  • Strictly pure queries can be pushed directly into an update
  • Stable proof loading and saving
  • Classpath directive
  • various bugfixes

1.2.0 (2007-11-30)

  • significantly improved proof strategies wrt. quantifier treatment and arithmetics
  • improved proof tree view, i.e.
  • hiding of closed subtrees
  • hiding of intermediate proof steps
  • search in proof tree
  • improved proof saving and loading
  • includes alpha version of the visual debugger
  • various bugfixes

1.0.1:

  • fixed an installation problem when KeY had not been installed before

1.0.0:

  • KeY-Book examples are based on this version (except Schorr-Waite, which provides a developer version on the book example site)
  • new proof-obligation generation framework
  • used currently only by the OCL translation; adaption of JML translation is underway
  • new method lemma rule
  • considerable improvements concerning arithmetics
  • lots of bugfixes and improved stability

1.0pre1a:

  • bug fixes and improvements
  • polynomial integer simplification

1.0pre1:

  • pre-release of upcoming 1.0
  • several improvements and fixes

0.99.2 (?)

  • fixed: Initialisation procedure of the KeY prover (KeY did not work properly if installed on a fresh system without a working KeY configuration file)
  • fixed: Source Code Distribution 0.99.1 was way too big

0.99.1 (?)

  • bug fixes concerning JML front-end

0.99 (?)

  • first version with the JML front-end
  • support of loop invariants
  • lots of new stuff