HacKeYthon 2025 - Spotted Issues

[adeleveschetti]

HacKeYthon 2025 - Spotted Issues

Home

• "If you are new to the KeY System, you should start with the excerpt Using the Prover from the KeY Book." The correct link: https://link.springer.com/content/pdf/10.1007/978-3-319-49812-6_15
• "How to use the KeY tool for end user (home page of the documentation)" The correct link: https://keyproject.github.io/key-docs/changelog/

User Guide

• General comment. The menu on the left has bold formatting for “macrosections” (UI Features, Languages, Proof Scripts). However, “Languages” is not clickable. Also, UI Features and Proof Scripts are structured in two different ways: the first is only a list of content of the section and the second is not
• Changelog:
  • the list in 2.12.2 -> Bug fixes has periods at the end of each sentence, but the other lists on the page do not
  • 2.12.2: Bug fixes and performance should not have “:”
  • 2.8.0: typo in “Seveal small and large bug fixes” -> Several. Also it is just a list of numbers
  • 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) are empty sections
• 0.99 : “lots of new stuff”
• ADTs: then the title of the section is User-defined abstract data types
• Embedding JavaDL expressions and functions into JML expressions: it is a very old section (2011)
• Applying KeY to programs with generics: typo in “The reason why generics are currently not implemented in KeY lie in the type system of KeY:” -> “lies”
• Polarity triggers for rewrite taclets: it is written in first person
• Polarity triggers for rewrite taclets: old topic (2012). The subsection names are in caps lock, the subsections in the rest of the documentation are not
• UI Features -> Index: on the left side we have “Proof Exploration” but in the Index it’s only “Exploration”
• Languages -> Grammar -> Reference: it is a list of syntax elements, useful?
• Proof Scripts: the title of the section is “Scripting Interactive Proofs” but on the left side it is only “Proof Scripts”
• Proof Scripts: the subsection “Mutators” should not have a period at the end (now it is “Mutators.”)
• Proof Scripts: “In this documentation the scripts that allow for branching statements are eplained. (see [Explanation of linear scripts] for the other version of scripts in KeY)” -> Period after the “)”
• Making interactive persistent using proof scripts: from 2015
• Making interactive persistent using proof scripts: “The quantified formula can also be specified if wanted. This here for the antecedent.” sentence not well structured
• Making interactive persistent using proof scripts: “(not necessarily the first in the Goal pane in the GUI)” -> panel
• Macros: “Generated on: ${new Date()}”
• Variables: a lot of KeY options have “no documentation” as a description
• Language Constructs -> Variables and Types: the first entry of the list has a capital letter after “:” and the other two do not. The second entry has a period at the end, the other two do not
• Languages -> None: to be removed
• Proof Exploration: image of exploration steps is broken

KeYclipse

• General comment: KeYclipse then the title is KeYClipse (formatting error)
• KeYclipse: "KeY project" maybe a typo from LaTeX
• KeYclipse: JML Editing extends the Java development tools (JDT) with support for JML to make writing JML specifications as convenient as writing Java source code.
  • This link https://eclipse.org/jdt/ should be replaced with https://github.com/eclipse-jdt/
  • This link http://www.jmlspecs.org/ should be replaced with https://www.cs.ucf.edu/~leavens/JML/index.shtml
• SED -> Prerequisites: Required update-sites and installation instructions are available in the download area.
  • The download link does not exist anymore, maybe it can replaced with: https://formal.kastel.kit.edu/~key/download/releases/2.6/eclipse/
• SED -> : Based on this, provides the Debug Platform language independent facilities for debugging (Debug Core and Debug UI).
  • The link does not exist anymore, maybe it can be replaced with: https://www.eclipse.org/community/eclipse_newsletter/2017/june/article1.php
• MonKeY -> Prerequisites: Required update-sites and installation instructions are available in the download area. -> The link does not work anymore.
• KeY IDE or KeYIDE? They are both used.
• JML Editing: The following screenshot shows for instance the extended syntax highlighting of the Java Editor:\
  • Also, in Current Functionality: Support of JDT's Rename and Move Refactorings
  • I think “\” should be removed (maybe typos from LaTeX).
• Development -> Build Tool: Gradle -> Test: For more information on testing see the gradle manual
  • The link is fine, but it should not be in the whole sentence. Also, the period at the end of the sentence is missing.
• KeY basics: then the title of the section is “KeY basics in Eclipse (Cross-project Functionality)”
• SED: then the title of the section is “Symbolic Execution Debugger”
• Stubby: then the title of the section is “Stubby - The Stub Generator”
• Starter: then the title of the section is “KeY 4 Eclipse Starter”
• VisualDBC: then the title of the section is Visual DbC
• Resources: then the title of the section is KeY Resources

Development

• Development: if you clink on the link, the section is called “Overview”
• Development: some sections (Build Tool: Gradle, Rewrite of the KeYParser, SMT Translation) have an abstract and some do not
• GUI extensions: the formatting of the subsections is different from the other sections
• Regression tests for proved rules: old topics (2014, 2015). Also the subsection Changes has a different formatting
• Testing -> None: need to be removed
• Testing of KeY: 2015
• Write Documentation: then the title of the section is “How to write documentation”
• Write Documentation: the title of the subsection “Local setup” has a different formatting than the rest of the subsections (same font of subsubsections)