KeY 4 Eclipse Starter¶
Unsupported historical content
This Eclipse integration is no longer supported or maintained. It targeted old Eclipse releases (Indigo/Luna era) and old versions of KeY; the update sites may no longer exist. This page is kept for historical reference.
KeY 4 Eclipse Starter is a basic Eclipse extension to start KeY from within Eclipse.
The following sections illustrate the main features of KeY 4 Eclipse Starter 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.
Prerequisites¶
KeY 4 Eclipse Starter is compatible with Eclipse Indigo (3.7) or newer.
Required update-sites and installation instructions are available in the download area.
Open KeY¶
-
Open KeY via main menu item "KeY, Open Application".
-
Select Application "KeY".
-
Use KeY as normal.
Verify a method contract¶
-
Select the method to verify.
-
Start proof via main menu item "KeY, Start Proof".
-
Select Application "KeY".
-
Instantiate proof in KeY as normal.
Load a proof or key file¶
-
Select the proof or key file to load.
-
Start proof via main menu item "KeY, Load File".
-
Select Application "KeY".
-
Instantiate proof in KeY as normal.
Stop auto mode when breakpoint is hit¶
-
Define a Line, Method or Java Exception breakpoint, a Watchpoint or a KeY Watchpoint as usual.
-
Select toolbar item "Stop when a breakpoint is hit." before starting the auto mode.
-
Auto mode stops when breakpoint is hit.
