Hackeython unknown methods

[flo2702]

Related Issue

This pull request addresses #1663

Intended Change

When using a library method without an explicit contract, instead of getting stuck in the proof, KeY now assumes the following default contract

public behavior
    ensures true;
    diverges true;
    signals_only Throwable;
    assignable \everything;

In addition, there is a proof setting soundDefaultContracts which can be turned off. In this case, the following default contract is used instead, which may be useful for exploratory proofs

public normal_behavior
    ensures true;
    assignable \strictly_nothing;

Type of pull request

• [ ] Bug fix (non-breaking change which fixes an issue)
• [ ] Refactoring (behaviour should not change or only minimally change)
• [x] New feature (non-breaking change which adds functionality)
• [ ] Breaking change (fix or feature that would cause existing functionality to change)
• [x] There are changes to the (Java) code
• [ ] There are changes to the taclet rule base
• [ ] There are changes to the deployment/CI infrastructure (gradle, github, ...)
• [ ] Other:

Ensuring quality

• [x] I made sure that introduced/changed code is well documented (javadoc and inline comments).
• [x] I made sure that new/changed end-user features are well documented (https://github.com/KeYProject/key-docs).
• [x] 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)

This was done during HacKeYThon 2 by @JonasKlamroth and @flo2702

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