Re-work (horizontal) compatibility check

[AlexanderKnueppel]

The actual check is implemented in pretty ad-hoc fashion and should be both refactored and re-worked.

Current workflow:

To verify compatibility between provided/required intertface, two conditions are checked for every required method: either (1) the provided interface contains a method with the exact same signature or (2) the mapped method is behaviorally compatible in the sense of liskov (class: du.kit.archicorc2.core\src\edu\kit\archicorc2\core\compatibility\CompatibilityChecker.java):

For verification, a java-stub is generated, where the required method calls the provided method. Using contracting, this allows us rather easily to verify whether the provided method is sufficient for the required one.

There are numerous outcomes:

• A proof is generated automatically
• If that is not possible, KeY will start an interactive session, where the user can try to prove compatible
• If that is not possible, the proof cannot be generated.
• Other outcomes: syntax error and timeout

Isseues:

• KeY is employed as the primary verifier. However, sometimes the generated stub can be verified automatically, sometimes only interactively, and sometimes not at all.

Envisioned Solution
If have the feeling that this should completely rewritten. The questions that arise:

• Is such a stub a useful idea?
• Is KeY the best veifier for this? what about Z3? Is is only necessary to check implication of specifications. There is no need here to check concrete code
• ...?