soundiness first steps

[mattulbrich]

Related Issue

This pull request is a new feature.

Intended Change

Implements a soundiness info window that analyzes KeY proofs and displays potential sources of unsoundness in a structured HTML report. The feature helps users identify taclet options, memory settings, and proof characteristics that may affect verification soundness. Integrated into the proof statistics dialog and context menu.

Key features:

• General KeY Settings analysis (memory, static initialization, JML, source consistency)
• Taclet Options analysis with plain English impact descriptions
• Source Analysis (skeleton for future expansion)
• Proof Tree Analysis (goals, lemmas, assumptions, rule applications)
• Disclaimer about KeY limitations (reflection, native methods, sequentiality, floating-point)

Type of pull request

• New feature (non-breaking change which adds functionality)
• Refactoring (behaviour should not change or only minimally change)
• There are changes to the (Java) code

Ensuring quality

• I made sure that introduced/changed code is well documented (javadoc and inline comments).
• I have tested the feature as follows: Opened proof statistics dialog, clicked "Show Soundiness Report" button, verified HTML report displays correctly with all four compartments (General KeY Settings, Taclet Options, Source Analysis, Proof Tree Analysis).
• I have checked that runtime performance has not deteriorated.

Additional information and contact(s)

Files added/modified:

• key.ui/src/main/java/de/uka/ilkd/key/gui/soundiness/SoundinessAnalyzer.java - Static utility class generating HTML reports
• key.ui/src/main/java/de/uka/ilkd/key/gui/soundiness/SoundinessDialog.java - Simple modal dialog displaying HTML
• key.ui/src/main/java/de/uka/ilkd/key/gui/soundiness/SoundinessExtension.java - Extension point registration
• key.ui/src/main/java/de/uka/ilkd/key/gui/soundiness/ShowSoundinessAction.java - Context menu action
• key.ui/src/main/java/de/uka/ilkd/key/gui/windows/ShowProofStatistics.java - Added soundiness button

Documentation updated:

• AGENT.soundiness.md - Design document
• IMPLEMENTATION_SUMMARY.md - Implementation summary

Build status: BUILD SUCCESSFUL on key.ui module.

The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.

by Qwen3.5 397B A17B

[unp1]

Thanks! Like it :-) Only bikesheding: For stricter then necessary, orange seems more like a warning. Dark green or blue?

[wadoon]

Should it not be 3.0?

[wadoon]

Strange to use fqn here.

[wadoon]

Would it not be wise to give the proof object to the action?

[wadoon]

Is the selected proof, also the proof for which the ContextMenu was requested?

[wadoon]

Will this file be removed?

[WolframPfeifer]

List of things that came to my mind while playing around a bit with the prototype:

• The taclet options list should also show the key, not only the value (i.e. "runtimeExceptions:ban" instead of "ban" at the moment).
• I think the description "arithmetic wraps around like in Java" for arithmeticSemanticsIgnoringOF is wrong
• Should the dialog also explain about proof caching? Due to the pragmatics of the implementation, we are only absolutely sure that a cache hit is applicable (i.e., replayable at the current proof) after doing the replay. There might be "spurious" cache hits, even if I am not sure where they come from.
• The proof statistics dialog looks weirdly wide now due to the new button.
• I would prefer a bullet point list also for "1. General KeY Soundness", to make it easier to read.
• http://soundiness.org/ lists the following things (among what is already shown in the dialog). Not sure what we should mention explicitly:
  • implicit method invocations (finalizers, class initializers, Thread.<init>, etc.)
  • exceptions and flow related to that
  • invokedynamic
  • code generation at runtime, dynamic loading
  • different class loaders
  • key native methods (Object.run, Object.doPrivileged)
• The dialog might also be a good place to list some information from https://www.key-project.org/applications/program-verification/ (generics, library methods, ...) or even https://www.key-project.org/jml-support-in-key/ (maybe semantics of assignable/accessible, invariants?), or link to these pages.
• What about dependencies to other contracts? The information is present (I think in class ProofCorrectnessMgt) and shown in the proof list, but maybe it should also be listed here.