Evaluation Instructions

The following sections explain the functionality of the evaluation wizard and how questions are asked. Please read them carefully before you continue.

1 Screencast

2 Target of Questions

The evaluation wizard asks questions related to the content currently shown in Eclipse. In the screenshot below questions are asked about the currently opened web browser. During this evaluation, questions will be asked about a proof attempt opened in KeY (external window) or the Symbolic Execution Debugger (perspective in Eclipse).

The evaluation wizard does not block Eclipse. This means that Eclipse is fully functional and can be used without closing the evaluation wizard.

3 Error Markers

An error marker is used to indicate that a question is not completely answered. An error marker or its absence does not indicate whether a given answer is correct or not.

4 Question Types

The following question types are used during this evaluation:

By selecting an answer, related sub questions might become visible.

5 Trust in Correctness of a Given Answer

The emoticons shown to the right of a question are used to collect your trust in the correctness of your given answer:

6 Jump to a not Completely Answered Question

If a question is not completely answered an error message is shown in the title area. You can click on the error message to make the related question visible.

7 Toolbar

The toolbar of the evaluation wizard provides functionality related to the current wizard page:

  1. If available, the first items open a previously shown introduction page (like this one) again in a separate shell.
  2. If available, the reset item restores the workbench with the target of the current questions. During this evaluation, you should click on it if you have for instance accidentally closed or modified the proof or the Java source code with JML specifications.
  3. The pin window item defines if the evaluation wizard is shown always on top of Eclipse or not.

8 Closing the Wizard

Closing the wizard does not cancel the evaluation. The evaluation can be continued at any time just by opening the wizard again (main menu item Evaluation, Understanding Proof Attempts).