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.

[codecov[bot]]

Codecov Report

Attention: Patch coverage is 60.52632% with 15 lines in your changes missing coverage. Please review.

Project coverage is 37.77%. Comparing base (1b48b9e) to head (04cc9ed). Report is 56 commits behind head on main.

:exclamation: Current head 04cc9ed differs from pull request most recent head 028663e

Please upload reports for the commit 028663e to get more accurate results.

Files	Patch %	Lines
...d/key/speclang/jml/translation/JMLSpecFactory.java	53.57%	12 Missing and 1 partial :warning:
...main/java/de/uka/ilkd/key/speclang/SLEnvInput.java	77.77%	0 Missing and 2 partials :warning:

Additional details and impacted files

@@             Coverage Diff              @@
##               main    #3431      +/-   ##
============================================
- Coverage     38.03%   37.77%   -0.26%     
+ Complexity    17089    17039      -50     
============================================
  Files          2099     2076      -23     
  Lines        127274   126988     -286     
  Branches      21386    21387       +1     
============================================
- Hits          48409    47975     -434     
- Misses        72892    73104     +212     
+ Partials       5973     5909      -64     

:umbrella: View full report in Codecov by Sentry.
:loudspeaker: Have feedback on the report? Share it here.

[WolframPfeifer]

I just stumbled across this PR recently and noticed that my original use case is not yet solved:

import java.util.Arrays;

class C {
    public static void main(String[] args) {
        int[] a = {5,7,3,9,3,5,9,0,2};
        System.out.println(Arrays.toString(a));
    }
}

Trying to load this file results in an exception of the following form:

Could not resolve MethodReference "Arrays.toString(a)" @6/28 in ...
...

Caused by: recoder.service.UnresolvedReferenceException: Could not resolve MethodReference "Arrays.toString(a)" @6/28 in ...

I noticed that there is a taclet option soundDefaultContracts now, but it is undocumented. Also, the exception above occurs independent of the value of the taclet option. I wonder:

• What is the effect of this PR exactly?
• How does it work with imports?
• How does it work for classes that are present in the library (aka JavaRedux)?

@flo2702 @JonasKlamroth @mattulbrich (addressing all authors or reviewers):

• Could one of you add a documentation for the taclet option in optionsDecl.key?
• Would it make sense to have a short section about the feature in the KeY developer manual (ideally with a link to it in the error message)?
• Feature Request: List the auto-generated contracts somewhere, make them viewable (e.g. in "Proof"->"Show Used Contracts", marked as "inferred" or similar). Or, are they already listed?