KeY basics in Eclipse (Cross-project Functionality)
The following functionality is independent from a specific KeY-based Eclipse project.
The following sections illustrate features independent from a specific KeY-based Eclipse project using screenshots.
Each section contains numbered screenshots that explain a usage scenario step by step.
Clicking on each picture produces a more detailed view.
The screenshots may differ from the latest release.
Problem: An error containing "Consider using a classpath if this is a classtype that cannot be resolved" or "Could not resolve UncollatedReferenceQualifier" is shown.
The following screenshot shows such an error message which occurred when a proof for method magic() (see listing of Main) was started.
Such an error message is shown whenever KeY was unable to find a type in KeY's class paths specified in the project properties.
KeY operates on source code and not on compiled byte code.
This requires to provide the source code of all used types or at least stubs of called methods. Method stubs can be specified with JML.
KeY itself provides such stubs and specifications only for a minimal fraction of the Java API.
Create a new folder, for instance named "lib_specs", within the project and ensure that the folder is not part of the regular Java class path used by JDT.