mattulbrich
commented
1 year ago There is a long discussion on gitlab.
Open wadoon opened 1 year ago
mattulbrich
commented
1 year ago There is a long discussion on gitlab.
This issue was created at git.key-project.org where the discussions are preserved.
## Description In the process of trying to understand the underlying processes within KeY, to be able to implement a new construct `\some` as part of my bachelor's thesis, I experimented with the other "quantifiers", i.e. `\forall`, `\exists`, `\min`, `\max`, `\sum` and `\num_of`. During this process I found that the latter 4 constructs don't work as expected. As I didn't assume the issue to be within KeY itself at first, I tried to get more information on those constructs, in case I misunderstood the syntax, or similar. Therefore I both read the corresponding sections in the KeY-Book, as well as the JML reference manual. Finally I had to come to the conclusion that I'm not making any apparent mistakes and that the problem is more covert. I also showed those issues and my findings to (at)lukas as part of our recurring meeting for my bachelor thesis and he shared my opinion that it could indeed be a more underlying problem. In any case, that's why I decided to create this bug report, so that the issue can be resolved, one way or another. ## Reproducible Yes, for me the issue is reproducable, for both commit d9c6bcbac182cf8fbca666e248c0e4b544e96dd9 (the master branch commit I last tested it on), as well as the newest official KeY release. ### Steps to reproduce 1. Create a minimal working `test.java` file with the following contents ```java package BugTest; public class Main { /*@ @*/ public void do_smth() {} } ``` 2. Add the corresponding JML statements (in my case they works as expected) ```java package BugTest; public class Main { /*@ @ ensures (\sum int i; false; i) == 0; @ ensures (\num_of int i; 1 <= i && i < 5; true) == 4; @*/ public void do_smth() {} } ``` 3. Load the file into KeY and try to run a proof. It will succeed. 4. Add at least one of the following JML statements (this doesn't work as expected) ```java /*@ ensures (\num_of int j; j >= 1; j < 5) == 4; @ ensures (\sum int k; k >= 1 && k <= 2; k) == 3; @ ensures (\min int l; l >= 1 && l < 10; l) == 1; @ ensures (\max int m; 0 < m && m <= 10; m) == 10; @*/ ``` 5. Reload the file into Key and try to run a proof. It will **not** succeed, but rather not be able to close a goal regarding the added statement. The _expected behaviour_ would be for all of the statements provided in _4_ to work, as they are, at least as far as I'm informed, in accordance to the specification. The _actual behaviour_ is that they don't work and I have no idea why. --- * Commit: d9c6bcbac182cf8fbca666e248c0e4b544e96dd9
Information: