KeY provider/applicant: accessible of void methods

[WolframPfeifer]

Void methods in KeY should not have accessible clauses. While parsable, KeY throws an error when trying to prove the contract: "Dependency contracts are currently not allowed for void methods"

The reason for this is the current semantics of accessible clauses in KeY, which is roughly: "The method result only depends on the locations specified in the accessible clause". This is a subject of discussion in KeY (see KeYProject/key#3565), but for the moment, we should just not generate these clauses for void methods.

[Robert-Brune]

Do we actually need those accessible clauses at all?
I think the contract is still sound without them,
or are they required in certain proofs?

[WolframPfeifer]

For observers (that is, (model) methods with a non-void return type, invariants, model fields), accessible clauses describe a second contract (called "Dependency Contract") in addition to the "standard" functional contract.
This results in the following proof obligation (KeY book p. 324):

You can also see there that this only makes sense for methods that return a value.

When proving with Dynamic Frames, it is often crucial to know that the value of an observer did not change. For example, you might want to prove that the invariant of object o1 did not change when calling a method m on object o2. For this, you need to know that their footprints are disjoint in the beginning, o2.m() only writes (or adds fresh locations) to o2.footprint, and the invariant of o1 only depends on o1.footprint. This is a very common pattern, so for all observers, we need to have these accessible clauses.