Tracing2

[lks9]

Replaces #3491

Related Issue

This pull request addresses #.

Intended Change

This adds functionality to check a single control-flow trace in KeY, so only one path in the symbolic execution path.

The idea is to record the control flow while running normally. And then we use the recorded path as a precondition for any proof obligation.

For experimenting and debugging method contracts and similar, this might be very useful:

• We do not need any auxiliary specification (loop invariants, called method contracts, proof scripts).
• For a method contract KeY could not verify, it might be useful to explore just a single path (debugging of method contracts).

Backgound

I already had a previous approach using JML assume, see https://github.com/lks9/retroACexampleKeY/

The current implementation uses new taclet rules traceIf, traceIfElse.

Plan

• [ ] Automatic Instrumentation for recording (outside KeY)
• [x] Trace conversion for use in KeY (use traceAfter(), traceBefore() and traced() predicates)
• [ ] Tracing rules for Exception-Handling
• [ ] Documentation
• [ ] Soundness?

Type of pull request

• New feature (non-breaking change which adds functionality)
• There are changes to the taclet rule base

Ensuring quality

TODO:

• I made sure that introduced/changed code is well documented (javadoc and inline comments).
• I made sure that new/changed end-user features are well documented (https://github.com/KeYProject/key-docs).
• I added new test case(s) for new functionality.
• I have tested the feature as follows: ...
• I have checked that runtime performance has not deteriorated.

Additional information and contact(s)

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