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?