Well-Definedness-Checks Cannot be Selected in GUI

[mi-ki]

Description

On the current main branch, presumably due to #3640, it is not possible to select a well-definedness check on any loaded Java file via the GUI anymore. Various combinations of switching it off, on, etc. did not help. It can now only be done when loading a well-definedness proof obligation directly from a KeY file. Essentially, well-definedness checks are now rendered unusable for new Java files if you are no expert in writing KeY files by "guessing" the syntax for how well-definedness proof obligations are addressed in a KeY file.

Reproducible

always

Steps to reproduce

1. Load KeY for any Java file
2. Switch the taclet options to wdChecks:on
3. Reload
4. See that you do not see a well-definedness proof obligation

What is your expected behavior and what was the actual behavior?

Expected: Possibility to choose a well-definedness proof obligation
Actual: No possibility to choose a well-definedness proof obligation

Additional information

Not even a stacktrace, as the option is not usable anymore.

---

• Commit: cacb625

[mi-ki]

It appears that nobody checked the consequences of #3640 on the GUI. Is the GUI not a priority anymore?

[WolframPfeifer]

I did not do the review, but we recently had a short discussion about it. WD and Information Flow is triggered via profiles now. I just quickly checked for WD that it works on current main (select WD profile in right corner when loading a file):

The WD proof obligation(s) are shown and the proof(s) can be started as before (as far as I could tell, I did not really use the feature much).

One drawback seems to be that you cannot change the profile in the example dialog, so you have to load example files manually with the desired profile selected. Also, I am not sure how it interacts with specifying the profile in the .key file.

@wadoon Is there any up-to-date documentation? The description in the PR is not really helpful, as it lists pros and cons and different possible changes, not the actual result.

[mi-ki]

Oh, thanks for making me aware of the profile selection in the file menu. This has not been obvious to me. Hence, this means that well-definedness checks can only be chosen after reloading KeY with another profile now, right? I think this really renders it unusable for non-KeY-experts now. What is then the use of the taclet option now?

[WolframPfeifer]

No, actually you can select the profile directly when loading a file for the first time (just not in the example dialog, apparently).

However, I also don't really understand the interplay between WD profile and wdChecks taclet option, as well as WD profile selection in the dialog and .key file (which overwrites which?).
@wadoon @unp1 Maybe one of you can help with an explanation? I agree to @mi-ki that it is unclear you to use at the moment, in particular without documentation.

[mi-ki]

Ah, understood, now the loading makes more sense to me. Thanks!
After a bit more experimenting, it seems that the profile overwrites the taclet options.

Hence, now I see how well-definedness checks can be selected. Only selecting the taclet option does not seem to have an effect anymore, however.

[mi-ki]

Oh, and what is meant by the note Stability unknown in the profile selection dialogue (seen in the above screenshot) by the way?

[wadoon]

One drawback seems to be that you cannot change the profile in the example dialog, so you have to load example files manually with the desired profile selected. Also, I am not sure how it interacts with specifying the profile in the .key file.

@WolframPfeifer Our examples are loaded by KeY files. In these files, the correct profile should be stated, i.e., \profile "java-infflow";

[wadoon]

Oh, and what is meant by the note Stability unknown in the profile selection dialogue (seen in the above screenshot) by the way?

One consequence of the #3640 was the reactivation of the WD run-all-proofs. Some of the tests failed, hence, I was not sure about the quality of WD in the current context. KeY and its WD feature have just diverged.

As there was no official manual inspection, no combination of WD and KeY's other features, I'd conclude the current state of WD is unknown.

@mi-ki If you can re-check the current behavior, we can easily remove the words. Task would be tracked here #3741.

[wadoon]

Thanks! After a bit more experimenting, it seems that the profile overwrites the taclet options.

WD should be forcefully activated. I did not see any sense of using WD profile w/o wdChecks:on.

This also avoids the required reloading after Taclet Option changes.

Hence, now I see how well-definedness checks can be selected. Only selecting the taclet option does not seem to have an effect anymore, however.

@mi-ki Would it also not make sense to select the WD semantics in the open menu? Documented here: #3739

[wadoon]

I suggest that this issue can be closed. The main concern is w/o subject.