key
key copied to clipboard
KeYProject
KeY Theorem Prover for Deductive Java Verification
This issue was created at [git.key-project.org](https://git.key-project.org/key/key/-/issues/501) where the discussions are preserved. ---- * Mantis: [MT-1096](http://i12www.ira.uka.de/~klebanov/mantis/view.php?id=1096) * Submitted on: 2011-05-20 by (at)grahl * Updated: 2012-02-08 ### Description > Every change concerning...
Experiment to logically group steps in proof. Two main features: - "Reorder" proof steps such that adjacent proof steps modify the same formula (no interweaving of two simplification chains) -...
## Description Try to load the file below. It contains a syntax error (`==` instead of `=` in the problem statement), but the error message produced by KeY is bad:...
## Intended Change Based on #3420. Changes the JML pareser to accept definitions of ADTs. Datatypes have a list of _constructors_ separated by `|`, and a body of functions. ```java...
This PR is meant as a wip - tryout - branch for mixfix parsing in KeY ## Related Issue We want to define syntax for symbols in .key files. This...
This issue was created at [git.key-project.org](https://git.key-project.org/key/key/-/issues/29) where the discussions are preserved. ---- * Mantis: [MT-1499](http://i12www.ira.uka.de/~klebanov/mantis/view.php?id=1499) * Submitted on: 2014-10-28 by (at)mulbrich * Updated: 2014-10-29 ### Description > When KeY encounters...
## Idea At the moment, there are two places where the taclet options can be set: 1. The old dialog: "Options" -> "Show Taclet Options":  2. The newer unified...
## Idea At the moment, during the automatic proof search the GUI of KeY "freezes", i.e. does not respond to input events except for a click on the stop button....
## Please describe your proposal in a ONE sentence If the proof tree view is not visible the GUI proof tree should not be updated. ## Underlying problem Updating the...
This issue was created at [git.key-project.org](https://git.key-project.org/key/key/-/issues/1703) where the discussions are preserved. ---- This feature request documents the need for an option to omit all type hierarchy related symbols (e.g. u2i/i2u,...
Metadata
Owner
Metadata
KeY Theorem Prover for Deductive Java Verification