Add a stricter dependency contract proof obligation

[frereit]

Intended Change

The current proof obligation (DependencyContractPO) only verifies that the return value of a method only depends on the locations in the accessible clause. In contrast, this new proof obligation additionally verifies that any objects on the heap (except those newly created) only depend on the locations in the accessible clause.

The formula that is generated by this proof obligation for a method m with contract $(\mathit{pre}, \mathit{post}, \mathit{mod}, \mathit{dep})$ is roughly

$$\mathit{pre} \wedge \mathit{freePre} \wedge \langle \mathtt{res = m(args...)@C; } \rangle (h_1 = \mathtt{heap} \wedge r_1 = \mathtt{res}) \wedge \{u\} \langle \mathtt{res = m(args...)@C; } \rangle (h_2 = \mathtt{heap} \wedge r_2 = \mathtt{res}) \rightarrow \mathit{mod} \subseteq \mathit{dep} \wedge r_1 = r_2 \wedge \forall o; \forall f; ((o,f) \in \mathit{mod} \rightarrow o.f@h_1 = o.f@h_2) $$

While testing, you may run into #3563, so beware.

A simple example which proves succesfully with the current proof obligation, but cannot be proven with this new one is as follows:

/*@ public normal_behavior
@ accessible x;
@ assignable x;
@ ensures \result == x; 
@*/
public int foo() {
  if (this.y > 0) {
    this.x += 1;
    return x - 1;
  }
  return this.x;
}

Plan

• Code cleanup
• Document the changes
• Add tests
• Discussion
• UI changes?

Type of pull request

• New feature (non-breaking change which adds functionality)
• Breaking change (fix or feature that would cause existing functionality to 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 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.

[Drodt]

This PR is the result of the 2025 HacKeYthon

[mattulbrich]

Thanks, guys! Looks cool.

Contracts are used to conservatively abstract from method invocations. The (old) dependency contracts are used to show that the value of calls to pure methods does not change since the dependency set remains untouched.

Is there a similar use case for the stronger dependency contracts that exploit the proofs? The method-invocation rule would probably have to ensure that the read variables of the called method are a subset of the accessible locations in the calling method. ...

[mattulbrich]

Is planned to have a taclet option to switch between the old and new PO?

[Drodt]

Thanks, guys! Looks cool.

Contracts are used to conservatively abstract from method invocations. The (old) dependency contracts are used to show that the value of calls to pure methods does not change since the dependency set remains untouched.

Is there a similar use case for the stronger dependency contracts that exploit the proofs? The method-invocation rule would probably have to ensure that the read variables of the called method are a subset of the accessible locations in the calling method. ...

The motivation (for me) was first to enable dependency contracts for void methods and second to see if it could be done. We did briefly consider if it would be useful but I think we need more experimentation for a proper use case.

For that reason, a taclet option is not planned. (And we should not make it a taclet option as it does not affect the semantics of the Kripke structure.)