KeY

Java Card DL

The theoretical foundation of KeY is a formal logic called Java Card DL. DL stands for Dynamic Logic. It is a version of a first-order dynamic logic tailored to Java Card programs. As such, it for example allows statements (formulas) like ${\displaystyle \varphi \to [\alpha ]\psi }$, which intuitively says that the post-condition ${\displaystyle \psi }$ must hold in all program states reachable by executing the Java Card program ${\displaystyle \alpha }$ in any state that satisfies the pre-condition ${\displaystyle \varphi }$. This is equivalent to ${\displaystyle \{\varphi \}\alpha \{\psi \}}$ in Hoare calculus if ${\displaystyle \varphi }$ and ${\displaystyle \psi }$ are purely first order. Dynamic logic, however, extends Hoare logic in that formulas may contain nested program modalities such as ${\displaystyle [\alpha ]}$, or that quantification over formulas which contain modalities is possible. There is also a dual modality ${\displaystyle ⟨\alpha ⟩}$ which includes termination. This dynamic logic can be seen as a special multi-modal logic (with an infinite number of modalities) where for each Java block ${\displaystyle \alpha }$ there are modalities ${\displaystyle [\alpha ]}$ and ${\displaystyle ⟨\alpha ⟩}$.

Deduction component

At the heart of the KeY system lies a first-order theorem prover based on a sequent calculus. A sequent is of the form ${\displaystyle \mathrm{\Gamma }⊢\mathrm{\Delta }}$ where ${\displaystyle \mathrm{\Gamma }}$ (assumptions) and ${\displaystyle \mathrm{\Delta }}$ (propositions) are sets of formulas with the intuitive meaning that ${\displaystyle \underset{\gamma \in \mathrm{\Gamma }}{\bigwedge }\gamma \to \underset{\delta \in \mathrm{\Delta }}{\bigvee }\delta }$ holds true. By means of deduction, an initial sequent representing the proof obligation is shown to be constructible from just fundamental first-order axioms (such as equality ${\displaystyle e\dot{=}e}$).

Symbolic execution of Java code

During that, program modalities are eliminated by symbolic execution. For instance, the formula ${\displaystyle x\dot{=}0\to [x++;]x\dot{=}1}$ is logically equivalent to ${\displaystyle x\dot{=}0\to x\dot{=}0}$. As this example shows, symbolic execution in dynamic logic is very similar to calculating weakest preconditions. Both ${\displaystyle [\alpha ]\psi }$ and ${\displaystyle wp(\alpha ,\psi )}$ essentially denote the same thing – with two exceptions: Firstly, ${\displaystyle wp}$ is a function of some meta-calculus while ${\displaystyle [\alpha ]\psi }$ really is a formula of the given calculus. Secondly, symbolic execution runs through the program forward just as an actual execution would. To save intermediate results of assignments, KeY introduces a concept called updates, which are similar to substitutions but are only applied once the program modality has been eliminated. Syntactically, updates are consist of parallel (side-effect free) assignments written in curly braces in front of a modality. An example of symbolic execution with updates: ${\displaystyle [x=3;x=x+1;]x\dot{=}4}$ is transformed to ${\displaystyle \{x:=3\}[x=x+1;]x\dot{=}4}$ in the first step and to ${\displaystyle \{x:=4\}[]x\dot{=}4}$ in the second step. The modality then is empty and "backwards application" of the update to the postcondition yields a precondition where ${\displaystyle x}$ could take any value.

Example

Suppose one wants to prove that the following method calculates the product of some non-negative integers ${\displaystyle x}$ and ${\displaystyle y}$.

<span id="mwfA"></span><span class="kt" id="mwfQ">int</span><span class="w" id="mwfg"> </span><span class="nf" id="mwfw">foo</span><span class="w" id="mwgA"> </span><span class="p" id="mwgQ">(</span><span class="kt" id="mwgg">int</span><span class="w" id="mwgw"> </span><span class="n" id="mwhA">x</span><span class="p" id="mwhQ">,</span><span class="w" id="mwhg"> </span><span class="kt" id="mwhw">int</span><span class="w" id="mwiA"> </span><span class="n" id="mwiQ">y</span><span class="p" id="mwig">)</span><span class="w" id="mwiw"> </span><span class="p" id="mwjA">{</span> <span class="w" id="mwjQ"> </span><span class="kt" id="mwjg">int</span><span class="w" id="mwjw"> </span><span class="n" id="mwkA">z</span><span class="w" id="mwkQ"> </span><span class="o" id="mwkg">=</span><span class="w" id="mwkw"> </span><span class="mi" id="mwlA">0</span><span class="p" id="mwlQ">;</span> <span class="w" id="mwlg"> </span><span class="k" id="mwlw">while</span><span class="w" id="mwmA"> </span><span class="p" id="mwmQ">(</span><span class="n" id="mwmg">y</span><span class="w" id="mwmw"> </span><span class="o" id="mwnA">></span><span class="w" id="mwnQ"> </span><span class="mi" id="mwng">0</span><span class="p" id="mwnw">)</span> <span class="w" id="mwoA"> </span><span class="k" id="mwoQ">if</span><span class="w" id="mwog"> </span><span class="p" id="mwow">(</span><span class="n" id="mwpA">y</span><span class="w" id="mwpQ"> </span><span class="o" id="mwpg">%</span><span class="w" id="mwpw"> </span><span class="mi" id="mwqA">2</span><span class="w" id="mwqQ"> </span><span class="o" id="mwqg">==</span><span class="w" id="mwqw"> </span><span class="mi" id="mwrA">0</span><span class="p" id="mwrQ">)</span><span class="w" id="mwrg"> </span><span class="p" id="mwrw">{</span> <span class="w" id="mwsA"> </span><span class="n" id="mwsQ">x</span><span class="w" id="mwsg"> </span><span class="o" id="mwsw">=</span><span class="w" id="mwtA"> </span><span class="n" id="mwtQ">x</span><span class="w" id="mwtg"> </span><span class="o" id="mwtw">*</span><span class="w" id="mwuA"> </span><span class="mi" id="mwuQ">2</span><span class="p" id="mwug">;</span> <span class="w" id="mwuw"> </span><span class="n" id="mwvA">y</span><span class="w" id="mwvQ"> </span><span class="o" id="mwvg">=</span><span class="w" id="mwvw"> </span><span class="n" id="mwwA">y</span><span class="w" id="mwwQ"> </span><span class="o" id="mwwg">/</span><span class="w" id="mwww"> </span><span class="mi" id="mwxA">2</span><span class="p" id="mwxQ">;</span> <span class="w" id="mwxg"> </span><span class="p" id="mwxw">}</span><span class="w" id="mwyA"> </span><span class="k" id="mwyQ">else</span><span class="w" id="mwyg"> </span><span class="p" id="mwyw">{</span> <span class="w" id="mwzA"> </span><span class="n" id="mwzQ">y</span><span class="w" id="mwzg"> </span><span class="o" id="mwzw">=</span><span class="w" id="mw0A"> </span><span class="n" id="mw0Q">y</span><span class="w" id="mw0g"> </span><span class="o" id="mw0w">/</span><span class="w" id="mw1A"> </span><span class="mi" id="mw1Q">2</span><span class="p" id="mw1g">;</span> <span class="w" id="mw1w"> </span><span class="n" id="mw2A">z</span><span class="w" id="mw2Q"> </span><span class="o" id="mw2g">=</span><span class="w" id="mw2w"> </span><span class="n" id="mw3A">z</span><span class="w" id="mw3Q"> </span><span class="o" id="mw3g">+</span><span class="w" id="mw3w"> </span><span class="n" id="mw4A">x</span><span class="p" id="mw4Q">;</span> <span class="w" id="mw4g"> </span><span class="n" id="mw4w">x</span><span class="w" id="mw5A"> </span><span class="o" id="mw5Q">=</span><span class="w" id="mw5g"> </span><span class="n" id="mw5w">x</span><span class="w" id="mw6A"> </span><span class="o" id="mw6Q">*</span><span class="w" id="mw6g"> </span><span class="mi" id="mw6w">2</span><span class="p" id="mw7A">;</span> <span class="w" id="mw7Q"> </span><span class="p" id="mw7g">}</span> <span class="w" id="mw7w"> </span><span class="k" id="mw8A">return</span><span class="w" id="mw8Q"> </span><span class="n" id="mw8g">z</span><span class="p" id="mw8w">;</span> <span class="p" id="mw9A">}</span>

One thus starts the proof with the premise ${\displaystyle x\ge 0\wedge y\ge 0}$ and the to-be-shown conclusion ${\displaystyle z\dot{=}x\cdot y}$. Note that tableaux of sequent calculi are usually written "upside-down", i.e., the starting sequent appears at the bottom and deduction steps go upwards. The proof can be seen in the figure on the right.

Additional features

Symbolic Execution Debugger

The Symbolic Execution Debugger visualizes the control flow of a program as a symbolic execution tree that contains all feasible execution paths through the program up to a certain point. It is provided as a plugin to the Eclipse development platform.

Test Case Generator

KeY is usable as a model-based testing tool that can generate unit tests for Java programs. The model from which test data and the test case are derived consists of a formal specification (provided in JML) and a symbolic execution tree of the implementation under test which is computed by the KeY system.

Distribution and Variants of the KeY System

KeY is free software written in Java and licensed under the GNU General Public License, version 2. It can be downloaded from the project website in source or as pre-compiled JAR.

KeY-Hoare

KeY-Hoare is built on top of KeY and features a Hoare calculus with state updates. State updates are a means of describing state transitions in a Kripke structure. This calculus can be seen as a subset to the one that is used in the main branch of KeY. Due to the simplicity of the Hoare calculus, this implementation is essentially meant to exemplify formal methods in undergraduate classes.

KeYmaera/KeYmaeraX

KeYmaera (previously called HyKeY) is a deductive verification tool for hybrid systems based on a calculus for the differential dynamic logic dL . It extends the KeY tool with computer algebra systems like Mathematica and corresponding algorithms and proof strategies such that it can be used for practical verification of hybrid systems.

KeYmaera has been developed at the University of Oldenburg and the Carnegie Mellon University. The name of the tool was chosen as a homophone to Chimera, the hybrid animal from ancient Greek mythology.

KeYmaeraX developed at the Carnegie Mellon University is the successor of KeYmaera. It has been completely rewritten.

KeY for C

KeY for C is an adaption of the KeY System to MISRA C, a subset of the C programming language. This variant is no longer supported.

ASMKeY

There is also an adaptation to use KeY for the symbolic execution of Abstract State Machines, that was developed at ETH Zürich. This variant is no longer supported.