Skip to content

2.8.0 (2020-12-01)
Compare
Choose a tag to compare
@wadoon wadoon released this 30 Jan 13:05
· 4049 commits to main since this release
KeY-2.8.0
9849f7b

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

Assets 5
Loading