Softpedia >Windows >Programming >Other Programming Files >KeY >  Changelog

KeY Changelog

What's new in KeY 2.10.0

Dec 24, 2021
  • 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

New in KeY 2.8.0 (Dec 18, 2020)

  • Created new file intDiv.key for newly added taclets concerning
  • SMT preparation macro
  • Completion Scopes
  • 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.
  • Adding "System.arraycopy" with contract to JavaRedux
  • Explizit excption for nested updates (allowed in the KeY book, unsupported by implementation) !
  • Loop contract
  • Loading and Storing proofs with compression
  • Saving of proofs (incl. dependening resources) into one file (zip) called "proof bundle"
  • Bsum taclets (!96)
  • Taclets for more flexible handling of observer depency (!177)
  • Loop contracts improvements (!188)
  • Loop scopes: a new rule for proving loop invaraints (!313, !326)
  • Support for Annotation Marker in JML (!308)
  • FIX:
  • Bugfixing handling of program variables of type "any" and parsing (!133)
  • Speed up in saving proofs (!120)
  • Incompleteness issue when rewite taclet was applied and the goaltemplate… (!119)
  • Fix of inner blocks (!82)
  • KeY read files character-wise, now the file content is cached (!XXX)
  • More jml synonyms (!85)
  • User-provided notes are saved within the proof file (!304)
  • Origin labels for user interactions could not be parsed
  • Method signature resolve in JML expressions (!309)