2.8.0 (2020-12-XX)

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 )

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