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/1621) where the discussions are preserved. ---- `IssueDialog` and `EditSourceFileAction` should be rewritten. Currently, it is unclear when "Edit File" button is enabled in the...
This issue was created at [git.key-project.org](https://git.key-project.org/key/key/-/issues/1663) where the discussions are preserved. ---- ## Description The story is well-known (see #491) and a solution exists but I think there could be...
This issue was created at [git.key-project.org](https://git.key-project.org/key/key/-/issues/1694) where the discussions are preserved. ---- ## Description The new exception dialogue has nice UI features. However, there are some teething issues. This is...
## Description User-defined/Built-in KeY sorts are supposed to be accessible from within JML using a `\dl_` escape. However, this does not work within quantified expressions. ### Steps to reproduce always...
This MR brings overloaded operators to KeY lang: 1. On function and predicate definitions you can additional add prefix, infix, and postfix notations. ``` \functions { int add(int, int) \infix(+);...
## Description Using assertions as ~last~ statement inside an **(otherwise empty)** if-then-block raises a class cast exception ## Reproducible always. ### Steps to reproduce Try to load: ```java class A...
## Description `sort_Field` is not defined, but used here: https://github.com/KeYProject/key/blob/022f0facc33017f34bba2df8594a5fb40678d3cc/key.core/src/main/resources/de/uka/ilkd/key/smt/newsmt2/FieldConstantHandler.preamble.xml#L14 ## Reproducible always ### Steps to reproduce 1. Load some proof (I used Exercise7.java from #1000) 2. Do some simplifications...
## Description > Please describe your concern in detail! The SourceView seems not too highlight symbolically executed statements in green, if the contract to be proven is inherited. ## Reproducible...
## Related Issue This pull request addresses #3378. ## Intended Change This reverts commit 4759370f719ed506746e7a2a13832eac48cfc6c1. As discussed during a developers meeting, the highlighting is quite important during drag'n'drop. It reenables...
## Description If a generic sort is used inside a problem definition (in a .key file), this leads to a broken sequent. ## Reproducible always ### Steps to reproduce Load...
Metadata
Owner
Metadata
KeY Theorem Prover for Deductive Java Verification