COSTA and KeY Integration web page

On this website you find instructions how to install COSTA and KeY as well as the examples mentioned in paper submitted to SoSyM iFM special issue 2013.

Requisites:

To run KeY and COSTA you need the JDK 1.6 (Java 6) from Oracle/Sun.

Examples:

Examples can be downloaded from http://costa.ls.fi.upm.es/costa-key/costa-key-examples.tgz

Costa (Linux only):

For the COSTA Eclipse plug-in you need to add the following installation site (Help -> Install New Sotfware...) http://costa.ls.fi.upm.es/costa-key/update-site/

Afterwards select this installation site, select both features, COSTA plugin, and follow the eclipse wizard's instructions. After installation you should see a new menu item "Costa Analyzer" and a toolbar button "Analyze Method".

KeY:

The KeY distribution which integrates Costa and KeY is available at http://www.key-project.org/IFM13_COSTA_KeY/webstart/KeY.jnlp.
To generate the proofs the following options must be selected:
  • "Taclet Options" (you need to load a problem first, the make the changes, then load it again. Afterwards the selection is fixed)
    • assertions: on
    • programRules: Java
    • intRules: arithmeticSemanticsIgnoringOF
    • initialisation: disableStaticInitialisation
    • localVariableDeclaration: costa
    • runtimeExceptions: allow
  • "One Step Simplification":
    • Strategy setting (left tab pane):
    • Stop At: Default
    • Logical Splitting: Delayed (only PascalTriangle requires Logical Splitting:free)
    • Loop Treatment: Invariant
    • Method Treatment: Expand
    • Dependency Contracts: On
    • Query Treatment: Off
    • Arithmetic Treatment: DefOps
    • Quantifier Treatment: No Split With Progs
    • User-specific taclets: all off
    • Max. Rule Applications: Set it to the maximum value (some examples requires more than 20.000 nodes)

Using Costa + KeY:

1) Annotating Java source code using Costa: The first step is to create a Java project to add the examples directory, and move the examples directory to src directory created by Eclipse (you can use o.s. copy and paste to add the examples). Example files are not annotated so the next step is to analyze them and generate JML annotations. Just follow these simple steps:
  • * Select the Costa menu option
  • * Analyze Method
  • * Select the method and set the option Intermediate Information to "As JML annotation"
  • * Click in "Edit Preferences"
  • * Depending on the example, the option "Select the Analysis Level" must have:
    • - Integer examples: "KeY"
    • - Heap examples: "KeY"
    • - Heap Sensitive examples (factorial, fieldcomp, nestloops, arrayelem): "KeY Heap Sensitive"
    • - Conditional examples (basiccond, noteqcond, multicond, nestedlcond, multiloop): "KeY Heap Conditional"
2) Generating the proof using KeY
  • * Cancel the initial example loading message
  • * Load the Java file selecting the file in the source code directory (File -> Load)
  • * Run the proof (Proof -> Start)
  • * Save the results (File -> Save)
3) Checking the proof using KeY
  • * Load the proof, selecting the .proof file previously generated (File -> Load)