Java Coverage¶
Under construction
This page is still under construction; its content may still change.
KeY verifies sequential Java. This page summarises which Java language features the prover currently understands, when each feature entered the Java language, how it evolved afterwards, and where KeY's support is complete, partial, or missing. Support for modern Java keeps evolving, so this is a moving target; the table reflects the status as of KeY 3.0.
Legend¶
| Symbol | Meaning |
|---|---|
| Fully supported: parsed, converted, and backed by proof rules | |
| ( ) | Partially supported: accepted, but with the limitation noted in Comments |
| Not supported: rejected by the front-end, or accepted but not soundly modelled (see Comments) |
Runtime and JVM features¶
KeY verifies sequential Java without a model of the JVM runtime, so these concurrency, memory-management, class-loading and reflection capabilities are not supported (KeY may still load code that calls their APIs, but does not reason about them).
| Feature | Introduced (JEP/JSR) |
Later changes (JEP · JLS) |
KeY | Comments |
|---|---|---|---|---|
| Multithreading | Java 1.0 (1996) | §17 (threads & locks) | Not supported; KeY reasons about sequential Java only. | |
| Garbage collection | Java 1.0 (1996) | runtime / JVM feature | Not supported. | |
| Dynamic class loading | Java 1.0 (1996) | §12.2 (class loading) | Not supported. | |
| Reflection | Java 1.1 (1997) | library (java.lang.reflect) |
Not supported. |
Java language feature support¶
The Introduced and Later changes columns link the defining JEP (or, for Java 5 to 8 features that predate the JEP process, the JSR) together with the relevant JLS section.
| Feature | Introduced (JEP/JSR) |
Later changes (JEP · JLS) |
KeY | Comments |
|---|---|---|---|---|
| Classes, interfaces, inheritance, fields, methods | Java 1.0 (1996) | §8, §9 (stable core) | Fully supported. KeY's core object model. Newer interface features have their own entries: private / default methods and sealed classes / interfaces. | |
Statements & control flow (if, while, do, for, labelled break/continue) |
Java 1.0 (1996) | §14 (stable) | Fully supported. | |
| Arrays, incl. multi-dimensional | Java 1.0 (1996) | §10 (stable) | Creation, access, ArrayStoreException and out-of-bounds all modelled. |
|
Exceptions (try/catch/finally, throw) |
Java 1.0 (1996) | §11.3, §14.20 (stable) | Fully supported. | |
| Nested, member & anonymous classes | Java 1.1 (1997) | §8.1.3, §15.9.5 | Static-nested, inner and anonymous classes all load. | |
| Local classes (declared in a method body) | Java 1.1 (1997) | §14.3 | Not supported; declare it as a nested or member class instead. | |
switch statement |
Java 1.0 (1996) | selector types widened: enum (JSR 201, Java 5), String (JSR 334, Java 7), both under §14.11; arrow labels (JEP 361, Java 14) & patterns (JEP 441, Java 21); see below |
Desugared to an if-cascade. Integer selectors work; an enum selector needs qualified case labels (case E.C:); the standard unqualified case C: fails to resolve (see Strings in switch for String). |
|
instanceof type test |
Java 1.0 (1996) | pattern binding added Java 16 (JEP 394, see below) | Plain type test only; the pattern-binding form is separate. | |
Floating point (float, double) |
Java 1.0 (1996) | always strict semantics restored in Java 17 (JEP 306, §15.4) | Supported. Requires installed SMT solver. | |
| Generics | Java 5 (2004), JSR 14 | diamond (JSR 334, Java 7, §15.9.1), improved inference (JSR 335, Java 8, §18), var lambda params (JEP 323, Java 11) |
Not supported in any form: <T>, <T extends S>, wildcards, generic methods and diamond <>. See Programs with generics. |
|
Enhanced for (for-each) |
Java 5 (2004), JSR 201 | §14.14.2 (stable) | Rewritten to an indexed / iterator loop. | |
| Autoboxing / unboxing | Java 5 (2004), JSR 201 | §5.1.7, §5.1.8 | Parses, but boxing/unboxing is not modelled (method resolution assumes its absence), so reasoning would be unsound. | |
| Enums | Java 5 (2004), JSR 201 | §8.9 (stable) | ( ) | Desugared to classes; declarations (including constant-specific bodies) load. Calculus support only partial. See also the switch row for the enum-label caveat. |
| Varargs | Java 5 (2004), JSR 201 | §8.4.1 (stable) | Desugared to an array parameter. | |
| Static imports | Java 5 (2004), JSR 201 | §7.5.3, §7.5.4 | import static is not supported. |
|
| Annotations | Java 5 (2004), JSR 175 | type annotations (JEP 104, Java 8, §9.7.4), repeating annotations (Java 8, §9.6.3) | ( ) | Parsed and ignored on declarations; declaring @interface types and type/repeating annotations are not supported. JML lives in comments, not annotations. |
| Binary literals & underscores in numeric literals | Java 7 (2011), JSR 334 | §3.10.1 (stable) | Fully Supported. | |
Strings in switch |
Java 7 (2011), JSR 334 | the only Java 7 change to switch: String selectors, compiled via hashCode/equals (§14.11); unchanged since |
( ) | Parses. Calculus uses == instead of equals; reasoning about String labels is limited. |
try-with-resources |
Java 7 (2011), JSR 334 | effectively-final resources (JEP 213, Java 9, §14.20.3) | Supported. API specification of Throwable#addSuppressed does not have a meaningful specification and needs to be provided by the thrown exception or as a separate bootclasspath. |
|
Multi-catch (catch (A \| B e)) |
Java 7 (2011), JSR 334 | §14.20 | Fully supported. | |
| Lambda expressions | Java 8 (2014), JEP 126 | var parameters (JEP 323, Java 11, §15.27.1) |
Not supported; see also method references. | |
| Method references | Java 8 (2014), JEP 126 | §15.13 | Not supported; see also lambda expressions. | |
Default / static interface methods |
Java 8 (2014), JEP 126 | private interface methods (JEP 213, Java 9, §9.4) | ( ) | Interfaces without private and default methods are supported; private/default methods of interfaces load as well but throw an exception when trying to prove anything |
Modules (module-info, JPMS) |
Java 9 (2017), JEP 261 | §7.7 | Not supported (a module-info currently triggers an internal error); KeY verifies classes, not modules. |
|
var (local variable type inference) |
Java 10 (2018), JEP 286 | §14.4.1 | ( ) | Primitive inference works (var x = 3, for (var i…)); a reference-typed initializer (e.g. var s = "…") currently throws an internal error. |
switch expressions (arrow labels, yield) |
Java 14 (2020), JEP 361 | §15.28, §14.11 | Not supported. | |
| Text blocks | Java 15 (2020), JEP 378 | §3.10.6 | Desugared to ordinary string literals. | |
| Records | Java 16 (2021), JEP 395 | record patterns added Java 21 (JEP 440, see below) | * | Desugared to classes with final fields (see examples/Java/Records).* Compact and synthetic constructors cannot carry a JML specification. For synthetic ones a default contract is generated. |
Pattern matching for instanceof |
Java 16 (2021), JEP 394 | §14.30.2, §15.20.2 | The pattern-binding form is not supported; plain instanceof is supported. |
|
| Sealed classes & interfaces | Java 17 (2021), JEP 409 | §8.1.1.2, §9.1.1.4 | ( ) | sealed / non-sealed modifiers are accepted, but the permits clause is ignored, so sealing is not enforced. |
Pattern matching for switch |
Java 21 (2023), JEP 441 | §14.11.1, §14.30 | Type patterns (case Integer i) and record patterns (case Point(...)) are not supported. |
|
| Record patterns | Java 21 (2023), JEP 440 | §14.30.1 | Not supported; see records. | |
| Java Card (transactions, atomic updates) | Java Card 2.2.x | Enabled via the JavaCard taclet option; KeY provides a complete Java Card 2.2.x calculus. |
How this table was checked
Each row is backed by a minimal, javac-compiling example (one Java
construct each, generics in several variants) that is loaded into KeY to see
whether the front-end accepts or rejects it. These live in KeY's test suite as
key.core/.../java/coverage/{supported,rejected}/ and are pinned by the test
JavaFeatureCoverageTest, which fails if a supported feature stops parsing
or a rejected one starts, a built-in reminder to update this table. A
means the construct loads; a
means it is rejected at load time
(usually "Unsupported element detected given by Java Parser") or, where
noted, loads but is not soundly modelled.