Dieses Kapitel untersucht das kritische Konzept der Verhaltensersetzbarkeit im Kontext des JVM-Bytecodes, aufbauend auf den grundlegenden Arbeiten von Liskov und Wing. Es unterstreicht die Wichtigkeit, sicherzustellen, dass Typen, die durch Subtypisierung in Zusammenhang stehen, Verhaltenskonsistenz aufrechterhalten, was für die Korrektheit und Flexibilität objektorientierter Programme unverzichtbar ist. Das Kapitel führt einen bahnbrechenden Ansatz zur Modellierung und Verifizierung von Verhaltensersatzbeschränkungen innerhalb eines deduktiven Verifikationsrahmens ein, wobei der ByteBack-Verifier zum Einsatz kommt. Diese Methode erweitert die Fähigkeiten des Prüfers, mit mehreren JVM-Sprachen, einschließlich Java, Scala und Kotlin, umzugehen, wodurch sie auf eine breite Palette von Programmen anwendbar ist. Das Kapitel geht auf die Herausforderungen ein, die von Sprachfunktionen ausgehen, die statische Typprüfungen wie das Überschreiben von Methoden in Java umgehen können, und präsentiert innovative Lösungen, um diese Probleme zu lösen. Außerdem wird die Erweiterung von ByteBack mit Spezifikationsmerkmalen wie Ghost-Prädikaten, Klasseninvarianten und Spezifikationsvererbung diskutiert, die für das Nachdenken über die Substituierbarkeit von entscheidender Bedeutung sind. Das Kapitel schließt mit einer Reihe von Experimenten, die die Fähigkeit des Prüfers demonstrieren, Substitutionseigenschaften in komplexen, mehrsprachigen Programmen präzise zu analysieren und zu verifizieren, und die seine praktischen Anwendungen und Vorteile gegenüber bestehenden Verifikationstechniken hervorheben.
KI-Generiert
Diese Zusammenfassung des Fachinhalts wurde mit Hilfe von KI generiert.
Abstract
Subtyping in object-oriented languages is widely based on Liskov’s substitution principle, which offers static correctness guarantees of type safety while abstracting implementation details. Unfortunately, the type systems of languages like Java cannot statically enforce full behavioral substitutability, and in fact there are numerous examples of libraries some of whose components are related by inheritance but not substitutable (for example, because they do not implement “optional” operations).
In this paper, we present a novel approach to precisely specify and reason about substitutability in JVM languages. A distinctive feature of our approach is that it targets JVM bytecode, as opposed to a program’s source code, as it is based on the ByteBack deductive verifier. To support reasoning about substitutability, we extended ByteBack with ghost specifications, a (restricted) form of class invariants, and substitutability-preserving specification inheritance (precondition weakening and postcondition strengthening). Equipped with these features, ByteBack can now reason precisely about behavioral substitutability violations in a way that is applicable to realistic examples (such as with optional operations of Java’s List interface). Our experiments also demonstrate that ByteBack can analyze substitutability in programs written in a combination of JVM languages, including multi-language code where Scala or Kotlin code interacts with Java libraries.
Hinweise
Work partially supported by SNF grant 200021-207919 (LastMile).
1 Introduction
Since Liskov and Wing’s influential work [17], behavioral substitutability is a widely accepted, fundamental requirement of types related by subtyping—especially relevant for object-oriented programming [20]. Informally, a type T is substitutable for another type S if replacing an instance of S with an instance of T does not break the behavior of the code using it. Thus, a type system that can statically check substitutability combines correctness guarantees (absence of behavioral incompatibility errors) with flexibility (transparently switching between different implementations through polymorphism). This is why most modern statically typed object-oriented languages are designed with type systems that enforce substitutability.
Unfortunately, other features of a programming language may still allow developers to bypass a type system’s static checks and introduce subtypes that are not truly substitutable. Take the example of Java: the overriding of a method m in a class D that inherits from another class C can simply throw an UnsupportedOperation exception; then, D is not substitutable for C, because the call o.m() terminates normally if o is an instance of C, and exceptionally if it is an instance of D—even though D is a subtype of C because they are related by inheritance. This substitutability-breaking pattern is not merely a theoretical possibility: there is empirical evidence that it is (deliberately) adopted in popular Java libraries to selectively enable or disable inherited operations [18, 19, 27].
Anzeige
In this paper, we introduce an approach to model behavioral substitutability constraints within a deductive verification framework, which we use to precisely reason about the behavior of programs involving these features. We develop our approach on top of our ByteBack verifier [22, 23], which works on JVM bytecode. Extending ByteBack makes our approach applicable to different languages that run on the JVM, such as (any versions) of Java, as well as (subsets of) Scala and Kotlin. This capability is especially relevant when verifying Scala or Kotlin programs that use Java libraries with optional operations, such as in Sec. 2’s capsule example; using our approach, we are able to consistently check substitutability violations (or to prove their absence) even in multi-language programs.
To support reasoning about substitutability, we extend ByteBack with three specification features, which we present in detail in Sec. 3: i) Ghost specification predicates, which we use as “flags” denoting whether a certain operation is or is not available; ii) A (restricted) form of class invariants, which specify, in each concrete class, which specification predicates hold; iii) Substitutability-preserving specification inheritance (precondition weakening and postcondition strengthening), which propagates the information about available operations through the inheritance hierarchy.
While these specification features are fairly standard in source-level deductive verifiers for object-oriented languages (for example, JML-based verifiers such as KeY [1] and OpenJML [6] support them), they become considerably more challenging to implement at the level of bytecode—in a way that is applicable to multi-language programs, and without access to any source code of clients or libraries. As we discuss in Sec. 3.6, our approach relies on mechanisms to “attach” a specification to existing classes in the system, as well as to correctly propagate such attached specifications to other classes that are related by inheritance.
The extension of ByteBack described in the present paper is, to our knowledge, the first deductive verification technique that can reason about behavioral properties of programs combining different JVM languages. Even when applied to single-language programs, working at the level of bytecode has the advantage of handling robustly any versions of Java (and other JVM languages); in contrast, as we discuss in Sec. 5, source-level deductive verifiers usually only support older versions of Java. Another distinguishing capability of our approach is verifying programs that use complex libraries (such as the JDK) by directly analyzing the compiled bytecode, without need to build or access the libraries’ source code. Sec. 4 discusses several experiments that demonstrate these capabilities on benchmark examples in Java, Kotlin, and Scala.
Anzeige
Contributions and positioning. In summary, the paper makes the following contributions: i) Specification features to express substitutability properties on top of the type system of JVM languages; ii) A verification technique based on these specification features; iii) An implementation of the verification technique built on top of the ByteBack verifier [23]; iv) An experimental evaluation with 22 programs involving unsupported operations in Java, Kotlin, and Scala; v For reproducibility, our version of ByteBack and all experimental artifacts are available in a replication package [24].
While our implementation is based on ByteBack’s previous instances [22, 23], this paper’s contributions substantially extend our previous work with specification and verification features necessary to reason about behavioral substitutability, and with a newly engineered implementation that makes them applicable to single- and multi-language bytecode programs. For simplicity, “ByteBack ” will refer to the new verification technique, and its implementation, described in the rest of this paper—unless we explicitly point out that we are referring to earlier work.
Fig. 1.
An example of behavioral substitutability errors that are uncaught by the Java and Scala type systems, which can be precisely analyzed with this paper’s deductive verification technique. The annotations use a simplified BBlib syntax, similar to the one used in previous work on ByteBack [22, 23].
2 Motivating Example
The best-known example of Java libraries that violate behavioral substitutability is probably that of java.util’s collections—in particular, interface List. Operations such as add are denoted optional, and hence some concrete classes inheriting from List may choose not to implement those operations, or to implement them only for a restricted set of valid inputs.
Fig. 1a shows a snippet of Java code that incurs this issue. First, there is a call of add on target ml, which is an instance of ArrayList. Since ArrayList is a subtype of List that implements all optional operations, the call ml.add(42) returns without errors. Then, there is a call of add on target il, which is an instance of List returned by static method List.of. As explained by the JDK’s documentation, List.of always returns immutable lists;1 therefore, the call il.add(42) fails with an UnsupportedOperation exception. However, the compiler accepts this code because, according to the type system’s rules, every instance of List should support method add.
Fig. 1b demonstrates the same kind of problem in Scala code that uses Java data structures. Scala’s library function asScala converts instances of java.util.List to instances of mutable.Buffer; this is usually sound, because Java lists are generally mutable. However, List.of actually returns an immutable list, which asScala simply wraps around; hence, calling modification operations, such as append, on instance bi of Buffer results in an exception at runtime. Even though Scala’s own collection library has been carefully designed to avoid such behavioral substitutability problems, Scala code may still indirectly suffer from the limitations of Java’s collections design.
To round off this brief diagnosis of the problem, we observe that the issue with using methods such as List.of is twofold: i) first, this method returns instances of List where some operations are not available (breaking List’s behavioral interface); ii) second, there is no type2 corresponding to an immutable variant of List that we can explicitly convert List.of’s output to.
Specifying substitutability. Fig. 1 outlines how our approach supports precisely specifying different behavioral variants of List. Fig. 1c shows how we equip type List with a behavioral specification predicate is_mutable(), which returns
iff the current instance of List is indeed modifiable. Since we do not have access to the source code of List, ByteBack provides the
annotation to augment any compiled class in the system with specification elements. Method is_mutable() is marked with ByteBack annotations
(it is used for behavioral specifications, and hence any of its implementations must be side-effect free) and
(its value does not depend on the current instance of List’s state, since a list cannot become immutable after it is initialized).
After provisioning predicate is_mutable(), we can use it to specify any other members of List: Fig. 1c shows the specification of methods add and of.3 For add, the specification says that it returns normally when is_mutable() is true, and with an exception when is_mutable() is false. For of, the specification says that it returns an instance
of List for which is_mutable() does not hold—which is how we specify that List.of returns unmodifiable lists. Since Java does not allow
methods, we provide a dummy implementation of
method List.of, but the
annotation instructs ByteBack to effectively ignore it.
Fig. 1d lists other specifications that use is_mutable(). Precisely, we equip concrete classes ArrayList and LinkedList—both subclasses of List—with a class
: is_mutable() always holds for their instances. The syntax of these class invariants is somewhat cumbersome, as it uses a utility method Ghost.of that we designed as part of this paper’s contributions. Since specification predicates such as is_mutable() are only supplied during ByteBack’s analysis—after the Java program under verification has been compiled into bytecode—we cannot rely on Java’s standard inheritance mechanisms to propagate specification elements to subclasses. Instead, ByteBack deploys a custom specification propagation algorithm, which weaves usages of Ghost.of into the type hierarchy during analysis. In Fig. 1d, Ghost.of is used to equip
(the current instance of ArrayList or LinkedList) with predicate is_mutable() declared in ListSpec.
Fig. 1e uses is_mutable() to specify a precondition for asScalaBufferConverter, to which asScala delegates the conversion of a Java List to a Scala mutable Buffer. Using in Scala the same mechanisms seen in ArrayList’s specification, Fig. 1e states that only mutable Java lists can be converted to mutable Scala buffers.
Verifying substitutability. Equipped with Fig. 1c and Fig. 1d’s specifications, ByteBack can reason precisely about Fig. 1a’s example. Thanks to ArrayList’s class invariant, it knows that ml.add(42) terminates normally; thanks to
’s postcondition, it knows that il.add(42) terminates by throwing an UnsupportedOperation exception—which may or may not be correct behavior, depending of whether the surrounding code expects that exception. ByteBack also issues a verification error for Fig. 1b’s example: the call to asScala violates Fig. 1e’s precondition, and hence it is invalid.
Fig. 2.
An overview of ByteBack’s verification workflow.
3 How ByteBack Specifies and Verifies Substitutability
Fig. 2 overviews how the deductive verification technique described in this paper works. Since our contributions is built atop ByteBack, the overall workflow remains similar to the one introduced in ByteBack’s previous work [22, 23]—with some important differences that we outline in Sec. 3.1 and Sec. 3.5 and describe in greater detail in the other subsections.
3.1 ByteBack Specification: Overview
Users of ByteBack add specifications the source code by means of BBlib—ByteBack’s source-level annotation library. Sec. 3.2 summarizes the core annotations provided by BBlib (such as pre- and postconditions), as well as those that are especially geared towards the present paper (such as class invariants). A key novel feature are attached specifications: users can list specification elements in separate ghost classes, and instruct ByteBack to weave them into the project under verification’s implementation. Sec. 3.3 describes this mechanism, which is especially useful to supply specifications for components whose source code is not available (including system libraries). In an object-oriented language, subtyping is connected to class inheritance; correspondingly, Sec. 3.4 describes how BBlib’s specifications are also inherited, following rules that are consistent with behavioral subtyping (i.e., precondition weakening and postcondition strengthening).
3.2 BBlib Specification Elements
BBlib annotations include all fundamental behavioral specification elements; since they were introduced in the previous work on ByteBack, we only summarize them here to make the paper self contained. Method specification elements include preconditions (
) and postconditions (
), as well as annotations to specify exceptional vs. normal behavior:
specifies a method that throws an exception of class E when it is called on an object where condition c holds; conversely,
specifies a method that returns normally when it is called on an object where condition c holds. For example, Fig. 1c specifies that method List.add terminates normally if
is_mutable() holds, and with an UnsupportedOperation exception otherwise.
Method bodies may include generic assertions (
leads to a verification error iff c does not hold when execution reaches it), assumptions (
ignores all executions where c does not hold), and loop invariants (
captures the fundamental inductive property of the loop where it appears).
Class-level specifications use annotation
, which asserts that property c must hold for all instances of the specified class. For instance, Fig. 1d annotates class ArrayList with the invariant
, which every object \(\ell \) of class ArrayList must satisfy. Such support for class invariants has been introduced in ByteBack only recently, as it is necessary to reason about substitutability. Nevertheless, ByteBack’s class invariants are still limited in expressiveness: a class C with
is simply equivalent to annotating every method of C with a “free”4 precondition I and a (regular) postcondition I, and every constructor of C with a postcondition I. This simple class invariant semantics is sufficient for this paper’s purposes, but it falls short of a full-fledged invariant methodology [5, 12, 15, 16, 26, 28], which should support temporary violations of the class invariant (for example, by private methods), as well as expressing invariants that depend on the state of multiple objects.
BBlib expresses specification predicates as methods marked with
. ByteBack checks that every method m equipped with such annotation can be expressed as a purely logic predicate: i)m must return a
, ii) have a signature consistent with m, iii) be pure and aggregable,5 and iv) only call other
methods. Annotation
generalizes the
annotation used in previous work [22, 23], since
also allows recursive calls in a behavior method body. Other annotations further constrain what a behavior method can predicate over. By default, a behavior method b used to specify a method m has access to m’s arguments (possibly including its returned value, if m does not return
), as well as to the current object’s state (e.g., through its fields). If b is annotated with
, it cannot depend on the object state directly. Conversely, if b is annotated with
, it can also access the current object’s pre-state (the state just before executing m). Thus,
behaviors are used in postconditions, where they relate the post-state to the pre-state. On the other hand,
behaviors are useful to specify properties that hold “absolutely”, such as is_mutable() in Fig. 1c: an instance of List is either mutable or immutable, and cannot change this property without being explicitly converted into a new object. Thus, annotation
is especially useful for behavioral substitutability properties like those we reason about in this paper; declaring them as
simplifies framing, since ByteBack only needs to check that their definitions do not refer to the object state.
3.3 Attached and Ghost Specifications
In previous work, all BBlib annotations had to be introduced in the source code of the element they refer to; for example, a method m’s postcondition had to appear just before m’s declaration in the program. This mechanism is limiting in all cases where we do not have access to a program’s source code, or we simply do not want to alter it in any way. Fig. 1’s example is a representative instance of this scenario: even if we had access to the source code of the JDK’s collections library, recompiling them just to introduce a handful of specification elements would be practically very inconvenient. In this work, we introduce the attaching mechanism, which enables users to add specifications to any element of the program under verification, regardless of whether they have access to its source code.
Attached specifications. A class S annotated with
instructs ByteBack to apply all specification features introduced in S to class C. Precisely, the specification of any method m in S whose signature matches that of a method with the same name in C is used as specification of m in C. The attaching mechanism is compositional: users can attach multiple specification classes to the same class C—each specifying only a part of C’s interface. If C includes some source-level specification of its own, users can selectively keep some of them, while overriding (or adding) the specifications of other methods. Take the example of Fig. 1c: specification class ListSpec only provides specifications for methods add and of in List. An “attached” specification class may also include additional methods, typically to introduce predicates and other specification elements—such as method is_mutable() in Fig. 1c’s attached specification class ListSpec.
Ghost specifications.Ghost code denotes code that is introduced only for the purpose of expressing a specification (or other annotations needed for deductive verification purposes) [9]. The term “ghost” was chosen because it suggests that it could be removed without having any effects on the program’s behavior. According to this definition, all BBlib annotations are ghost code; however, in this paper we will use the term “ghost specification” in a stricter sense to denote only attached specifications. The distinction matters for ByteBack because an attached specification, unlike a regular source-level specification, is not processed by the compiler consistently with its intended semantics. In particular, ghost specifications are not propagated by inheritance because the compiler does not know that they refer to methods in a different class from where they are declared. To work around this limitation, we equipped BBlib with the Ghost.of operator, which provide a means to link elements of ghost specifications introduced in different attached specification classes. Fig. 1d shows examples of using Ghost.of to specify the class invariants of ArrayList and LinkedList:
refers to specification predicateis_mutable(), introduced in specification class ListSpec, and evaluated on an instance
of the specified classes ArrayList and LinkedList. During analysis, ByteBack will first weave is_mutable() into List, propagate it to its subtypes ArrayList and LinkedList, and finally rewrite the
annotation so that it correctly refers to this attached method is_mutable().
Fig. 3.
Three classes A, B, and C related by inheritance, and their specifications.
3.4 Specification Inheritance
Behavioral substitutability constrains how the specification of a method can change between classes that are related by inheritance [20]. Consider two classes A and B such that B is a subclass of A; a method m is defined in A and overridden in B; \(P_{\texttt {A}}\) and \(Q_{\texttt {A}}\) denote A.m’s pre- and postcondition.
precondition weakening:B.m’s precondition \(P_{\texttt {B}}\) must be weaker or as strong as \(P_{\texttt {A}}\); in formulas: \(P_{\texttt {A}} \Longrightarrow P_{\texttt {B}}\).
postcondition strengthening:B.m’s postcondition \(Q_{\texttt {B}}\) must be stronger or as strong as \(Q_{\texttt {A}}\); in formulas: \(Q_{\texttt {B}} \Longrightarrow Q_{\texttt {A}}\).
As it is customary in behavioral specification languages [10], ByteBack interprets pre- and postcondition annotations in a way that enforces such overriding constraints. Fig. 3 shows classes A and B as above, whose methods m are annotated with BBlib’s
and
, which define the following pre- and postconditions:
B.m’s precondition \(P_{\texttt {B}}\) is the disjunction \(P_{\texttt {A}} \vee r_{\texttt {B}}\); since \(P_{\texttt {A}} \Longrightarrow P_{\texttt {A}} \vee r_{\texttt {B}}\), this is a weakening of A.m’s precondition.
B.m’s postcondition \(Q_{\texttt {B}}\) is the conjunction \(Q_{\texttt {A}} \wedge e_{\texttt {B}}\); since \(Q_{\texttt {A}} \wedge e_{\texttt {B}} \Longrightarrow Q_{\texttt {A}}\), this is a strengthening of A.m’s postcondition.
When more freedom in the definition of the specification of overridden methods is needed, BBlib offers annotations
and
, also demonstrated in Fig. 3’s class C: C.m’s precondition is just \(P_{\texttt {C}}\), and C.m’s postcondition is just \(Q_{\texttt {C}}\) as declared. When verifying a program annotated with
or
, ByteBack generates additional explicit verification conditions that check that all the
s introduce weaker formulas, and the
s introduce stronger formulas. In Fig. 3’s example, ByteBack would check that formulas \(P_{\texttt {A}} \Longrightarrow P_{\texttt {C}}\) and \(Q_{\texttt {C}} \Longrightarrow Q_{\texttt {A}}\) are valid.
Finally, the inheritance of class invariants is consistent with their semantics (discussed in Sec. 3.2): the class invariant \(I_{\texttt {B}}\) of a class B inheriting from A must be stronger or as strong as A’s class invariant \(I_{\texttt {A}}\). The
annotation enforces this constraint by taking the conjunction of all declared invariants: in Fig. 3, class B’s class invariant \(I_{\texttt {B}}\) is \(I_{\texttt {A}} \wedge j_{\texttt {B}}\), which is a strengthening of \(I_{\texttt {A}}\). Similarly to pre- and postconditions, annotation
declares a full class invariant explicitly, and checks that it is indeed a strengthening during verification. In Fig. 3, the class invariant of class C is literally \(I_{\texttt {C}}\), but ByteBack will check that \(I_{\texttt {C}} \Longrightarrow I_{\texttt {A}}\) holds.
3.5 ByteBack Verification: Overview
ByteBack’s verification process inputs a project’s bytecode, usually packed in a .jar file that includes all compiled source code and BBlib annotations in several classes. ByteBack queries Soot [11, 13]’s scene object to extract static information about the bytecode under analysis, and to ultimately translate the input program’s semantics into the intermediate verification language Boogie [3]. To this end, ByteBack first performs attaching (described in Sec. 3.6): it weaves the specification elements supplied in separate classes into the source code they refer to. Then, as outlined in Sec. 3.7, ByteBack performs a series of incremental, mostly local transformations of each method’s bytecode, which explicitly model the program’s behavior—such as the modular semantics of method calls, or the exceptional control flow. These transformations work on the Vimp intermediate representation: an extension with specification features of Soot’s Jimple readable bytecode representation [22]. Since specifications are provided as BBlib annotations (possibly even in separate classes, using the
mechanism), they are not available, in general, down the inheritance hierarchy, since the compiler is not aware of their intended semantics. Therefore, ByteBack also takes care of explicitly propagating specifications according to inheritance from the Vimp methods where they were explicitly introduced (see Sec. 3.8). After all these transformations, ByteBack finally encodes the ensemble Vimp components into a Boogie program that faithfully encodes the semantics of the input program and its specification. ByteBack’s output Boogie program can be verified with the Boogie intermediate verifier to determine whether the input JVM program is correct.
Fig. 4.
An example of how attaching works in ByteBack. Empty padding added for clarity.
3.6 Attaching
By querying Soot’s scene for the program under analysis, ByteBack retrieves all sorts of information about classes, their inheritance relation, their member declarations and implementations, and so on. ByteBack first processes each class S annotated with
, and copies the specification elements from S to C. If an element specified in S already has a specification in C, the attaching process replaces C’s specification with S’s. Attaching can also be used to replace implementations: if a method is declared as
in C but is given an implementation in S, the attaching process copies this implementation into C. Fig. 4 shows an example of attaching: class A in Fig. 4b includes an abstract method m and a concrete method n; the latter is annotated with a precondition \(P_{\texttt {A}}\). The process of attaching Fig. 4a’s class ASpec to A produces what shown in Fig. 4c: now, A includes a class invariant and a specification predicate f; in contrast, attaching does not modify method n or its specification, since n is not declared in ASpec; finally, method m gets the specification declared in ASpec, as well as its implementation.
Attaching can also target the parts of a program that are only available as external libraries, without access to their implementation. In such cases, attaching equips a library with a specification, which ByteBack then uses to reason about client code that uses that library. For example, Fig. 1d equips library class ArrayList with a class invariant; ByteBack does not have access to ArrayList’s implementation, but can still use this class invariant as a property of every instance of ArrayList used in the program under verification.
Fig. 5.
ByteBack incrementally transform Vimp code to encode the semantics of bytecode instructions and specifications.
3.7 Vimp-level Transformations
After attaching, ByteBack performs a series of transformations to all components of the program under verification, incrementally taking care of modeling a different aspect of a program in a form suitable for verification. For example, there are transformations to model the exceptional control flow, to process specification expressions, to translate bytecode instructions, and to handle loop invariants. Fig. 5 outlines the first two local transformations: \(\mathcal {T}_\textsf{exc}\) expresses the implicit exceptional control flow as an explicit control flow; \(\mathcal {T}_\textsf{exc}\) “aggregates” BBlib specification expressions, so that they can be encoded as pure logic expressions suitable for usage as specification constructs.
All these transformations use the Vimp bytecode representation as an intermediate format, which they use to incrementally encode the semantics of the input program and its specification in a form that is amenable to deductive verification. Vimp was introduced in previous work [22]; in the present paper, we further extended it to accommodate a broader range of features that are needed for verification (in particular, a heap model and background axioms). As a result, the final encoding of Vimp into the Boogie intermediate verification language is even simpler than in previous versions of ByteBack; relying on Vimp even more extensively also has the advantage that if we need to revise or extend the transformations (for example, to support a new construct with a different semantics), retaining a consistent Boogie encoding would be straightforward in many cases. Thus, we expect that our Vimp revision will also be useful to develop future extensions of ByteBack.
Ghost inlining. We introduced two new Vimp transformations to handle some of the features introduced in this paper. One is invariant instantiation, which we describe in Sec. 3.8 because it is applied after specification propagation. The other is ghost inlining, which handles all calls to specification method Ghost.of described in Sec. 3.3. For every call
—where cls is a
object representing the class where the referenced specification element was declared, and obj is a reference to an object to which the specification should be applied—ByteBack first checks that class cls is attached to a class of type compatible with obj’s type. If that’s the case, it simply replaces the whole
with obj. For example, consider again Fig. 1d’s class invariant:
; after attaching, this class invariant annotates class ArrayList. When it processes this annotation, ByteBack checks that ListSpec is attached to (i.e., provides a specification for) List, and
is of type ArrayList—one of List’s subtypes; thus, it simply rewrites the class invariant as
. Writing directly
as class invariant of ArrayList would have been rejected by the compiler: is_mutable() is only available in List and its subclasses after attaching. Thus, ByteBack provides the dummy method Ghost.of, which is accepted by the compiler and then rewritten by ghost inlining.
Algorithm 1 Specification Propagation
3.8 Specification Propagation
The Vimp transformations outlined in Sec. 3.7 are mostly local to each method. Before producing a Boogie program, ByteBack needs to propagate the specification elements of classes (class invariants) and methods (pre- and postconditions) according to the inheritance hierarchy of the program. In fact, ByteBack cannot rely on the compiler to propagate BBlib specifications, because specifications are given as BBlib annotations, whose semantics the compiler ignores. Besides, even if the compiler could propagate specifications given at the source-code level, it would still not be able to process attached specifications, which are declared in a separate class.
Algorithm 1 presents ByteBack’s specification propagation algorithm. The algorithm’s input is a directed acyclic graph (DAG) that represents the overall inheritance hierarchy among classes/types; henceforth,
denotes that class C is a child (heir, direct descendant) subclass of B in such graph. Since Java (as well as other JVM languages) supports a form of multiple inheritance via
s, inheritance is not simply a tree but a DAG, which may have multiple roots (while all classes inherit from java.lang.Object, interfaces can only inherit from other interfaces). First, ByteBack uses topological sorting to produce a total ordering of all classes that respects the partial inheritance order (procedure TopologicalSort in Algorithm 1). Then, the main procedure Propagate goes through the sorted list of classes (from supertypes to subtypes). For every class C, it defines its class invariant as the conjunction of C’s explicitly declared class invariant and the invariants of all direct superclasses of C. Similarly, for every method m overridden in C, it defines m’s precondition (resp. postcondition) as the disjunction (resp. conjunction) of m’s explicitly declared precondition (resp. postcondition) in C and the preconditions (resp. postconditions) of m in all direct superclasses of C. In all these cases, if class C’s declared class invariant uses
, or m’s declared pre-/postcondition in C uses
/
, the specification is not propagated from C’s superclasses. Instead, ByteBack generates additional side verification conditions (not shown in Algorithm 1), checking that the following implications hold:
Invariant instantiation. After specification propagation, ByteBack performs an additional Vimp transformation to express the class invariant semantics described in Sec. 3.2; this transformation has to run after propagation, because it depends on knowing the full, propagated class invariant of every class. First, every method m of class C with propagated invariant \(I_{\texttt {C}}\) is equipped with a “free” precondition (equivalent to an assumption) \(I_{\texttt {C}}\) and (regular) postcondition \(I_{\texttt {C}}\); constructors of C are also equipped with the latter. Second, every method c_in(... C a ...) with an argument a of type C is equipped with a free precondition \(\texttt {a.}{I}_\texttt {C}\) (i.e., C’s invariant holds for a); and every method C c_out(...) that returns an object of type C is equipped with a (regular) postcondition
(i.e., C’s invariant holds for the returned object). With this encoding, ByteBack can reason about every usage of an object of class C according to C’s invariant.
4 Experiments
This section describes several verification experiments that demonstrate ByteBack’s capabilities to reason about substitutability properties of Java data structures used by clients in Java and other JVM languages.
Table 1.
Experiments demonstrating how ByteBack can specify and verify substitutability properties of standard software components. Each row corresponds to an experiment, consisting of several pieces of client code that use library components that we specified using the features presented in this paper. For each experiment, the table reports the language (Java, Scala, and Kotlin) of the client code (all non-Java experiments also use JDK 17 data structures, and hence they are multilingual); the wall-clock time (in seconds) taken by ByteBack to produce a Boogie program, and by boogie to verify it; the size (in non-empty lines of code) of the source program with its annotations, and of the generated boogie program; the number of methods (met) and classes (cls) that make up the program and its specification; the number P of specification predicates (
), and the number A of attached specification classes (
) .
#
experiment
lang
ByteBack
boogie
source
boogie
met
cls
annotations
time [s]
size [LOC]
\(\qquad \ B\)
\(A\ \)
1
Mutable Lists
J 17
0.69
1.20
449
11 374
61
5
33
4
2
Mutable Sets
J 17
0.51
0.89
451
10 193
58
6
30
5
3
Mutable Maps
J 17
0.52
0.88
469
10 430
64
6
31
5
4
Nonnullable Lists
J 17
0.51
0.80
470
9 571
64
6
36
5
5
Nonnullable Sets
J 17
0.50
0.80
405
9 471
54
5
29
4
6
Nonnullable Maps
J 17
0.51
0.89
427
9 551
60
5
30
4
7
Unmodifiable Lists
J 17
0.54
0.77
450
11 399
61
6
35
5
8
Unmodifiable Sets
J 17
0.52
0.76
384
10 554
51
5
28
4
9
Unmodifiable Maps
J 17
0.62
0.87
405
10 632
57
5
29
4
10
Nonresizeable Lists
J 17
0.70
1.11
413
11 826
55
5
32
4
11
Guava Immutable Lists
J 17
0.72
0.96
390
10 004
56
5
31
4
12
Guava Immutable Sets
J 17
0.51
0.72
348
9 471
48
5
25
4
13
Guava Immutable Maps
J 17
0.52
0.73
374
9 375
54
5
26
4
14
Invariant Strenghtening
J 17
0.45
0.63
66
7 592
7
3
4
0
15
Precondition Weakening
J 17
0.53
0.84
87
7 681
15
3
6
0
16
Postcondition Strengthening
J 17
0.46
0.72
91
7 668
15
3
6
0
17
Lists Conversion
S 2.13
0.73
1.37
349
22 564
55
9
23
7
18
Sets Conversion
S 2.13
0.69
1.31
309
20 292
47
9
17
7
19
Maps Conversion
S 2.13
0.70
1.30
331
20 377
53
9
18
7
20
Lists Conversion
K 1.8
0.81
1.15
457
12 187
65
5
37
3
21
Sets Conversion
K 1.8
0.65
1.11
415
12 263
57
5
31
3
22
Maps Conversion
K 1.8
0.53
0.88
413
9 985
59
5
30
3
total
12.90
20.67
7 953
254 460
120
1 116
567
86
average
0.59
0.94
362
11 566
51
5
26
4
4.1 Experiment Description
Each experiment consists of client code that uses data structure libraries, namely implementations of java.util’s List, Set, and Map provided by Java 17’s JDK or by Google’s Guava.6 In each experiments, ByteBack inputs the client code, together with a basic input/output specification of the data structures’ APIs—specified using the
mechanism described in the paper. The verification goal is checking that the client code uses the data structures’ operations consistently with their specified behavior (as well as with the expected substitutability properties).
Tab. 1 gives some details about the experiments: out of 22 experiments, 16 are written in Java 17, 3 in Scala 2.13, and 3 in Kotlin 1.8. These are the languages of the verified client code, which uses data structure libraries written in Java 17; therefore, the Scala and Kotlin experiments are effectively multi-language, as they involve manipulating Java data structures within a different JVM language. Java experiments 14–16 are different than the others: they are simpler, as they focus on demonstrating ByteBack’s support for non-inherited class invariants, pre-, and postconditions defined with
,
, and
(discussed in Sec. 3.4).
Data structure properties. Here is a summary of the data structure behavioral properties that we specified in our experiments.
Mutability. A collection is mutable if it supports adding and removing elements to it, as well as replacing existing elements; LinkedList and ArrayList are examples of mutable collections. Conversely, a collection is immutable if it does not support adding, removing, or replacing its elements; Collections.unmodifiableList is an example of method that returns lists that are immutable. Since adding and removing are optional operations of the various collection interfaces, the implementations of methods such as List.add in an immutable collection simply throw an UnsupportedOperation exception (as demonstrated in Sec. 2’s example).
Resizeability. A collection is nonresizeable if it does not support adding and removing elements to it; conversely, it is resizeable if it does support such operations. A mutable data structure is also resizeable; thus, LinkedList and ArrayList are also examples of resizeable collections. In contrast, there exist collections that are nonresizeable but are still modifiable: method Arrays.asList produces an array-backed list whose elements can be replaced, but not added or removed (because its size is fixed to be that of the backing array).
Nullability. With a little abuse of terminology, we call a collection nullable if it can store null as elements; and nonnullable otherwise. Method List.of produces lists that are immutable and nonnullable: passing a
value to this method is accepted by the Java compiler but results in a NullPointer exception at runtime.
Java experiments. In the experiments, we equipped the various collection classes with specifications that characterize whether they are mutable, resizeable, and nullable; and their operations with pre- and postconditions that express when they are available (for example, add terminates exceptionally in nonresizeable collections) and the properties of the objects they return. These specification rigorously express the information that is available in the natural-language documentation of the corresponding Java libraries, but is not accurately captured by the (public) types in the actual implementations. As we discussed in Sec. 2, equipping these specifications relies on the attach mechanism to annotate libraries whose implementation is not directly available to ByteBack. With these annotations, ByteBack can precisely verify the expected behavior of client code, such as distinguishing between the List instances in Fig. 1a—one of them is mutable, the other is not.
Scala and Kotlin experiments. The experiments with Scala and Kotlin client code demonstrate how these fine-grained properties of collections interact with the conversion mechanisms these other JVM languages provide to reuse Java collections. Scala and Kotlin have their own collections libraries, designed based on a detailed type hierarchy that properly distinguishes between mutable, immutable, and other kinds of collections. When converting a Java data structure, there is the problem of choosing the most suitable corresponding Scala or Kotlin type. For performance reasons, the utilities in Scala’s JavaConverters do not copy the content of a Java data structure into a Scala data structure; instead, they create a mutable Scala collection that wraps the Java collection by delegating operations to it. If the underlying Java collection is actually immutable, some operations of the Scala collection will fail with an exception. Short of performing an expensive data-structure copy, the designers of Scala’s converters had no way of properly handling such scenarios, given that the information about which Java types correspond to immutable collections is simply not available statically (e.g., List.of returns an instance of a private class) and, even if it were, it would be inconsistent with the type hierarchy.
Kotlin’s type system also distinguishes between mutable and immutable collections; thus, if we want to explicitly convert a Java collection to a Kotlin collection, we can choose the most appropriate Kotlin type corresponding to the actual properties of that collection. Even though Kotlin’s List and MutableList types both still represent, at the level of bytecode, objects of type java.util.List, the Kotlin compiler can keep track of which operations are allowed on which variant of list. Nevertheless, Kotlin’s extensive support for Java interoperability still presents other means of introducing inconsistent behavior when Kotlin code interacts with Java code after compilation. Any Java type can seamlessly be used as a Kotlin type; compatibility rules are designed to be as general as possible—but this generality comes at the expense of soundness in some cases. For example, consider a Java method with an argument lst of type java.util.List that modifies lst (e.g., by removing an element). When the method is called from Kotlin, the compiler accepts any instance of Kotlin’s List and MutableList as actual argument; if we pass an instance of immutable List, the method will actually succeed and mutate the list, which is an obvious violation of an immutable list’s contract. In all these cases, using ByteBack’s annotations, we can still reason statically about the precise behavior of different lists or other collections, and hence soundly check that every operation will perform as intended.
4.2 Experiment Results
The experiments ran on a GNU/Linux machine with an Intel Core i9-12950HX CPU (4.9 GHz), running Boogie 2.15.8.0, Z3 4.11.2.0, and Soot 4.3.0. We repeated the execution of the experiments six consecutive times; we report the average wall-clock running time of each experiment over all repetitions except the first one (which we discard to account for possible cold-start delays).
The central columns of Tab. 1 show some statistics about the experiments’ results—all of which verified correctly as expected. The encoding time is usually around 2/3 of a second, and roughly (linearly) proportional to the size of the annotated code; Boogie’s verification time is around 1 second per experiment, and also roughly proportional to the number of methods and classes to be verified. The Boogie code produced by ByteBack is more than twice larger for the Scala examples (64 lines of Boogie code per line of source code) compared to the Java and Kotlin examples (27 lines of Boogie per line of source); the difference is explained by the numerous class definitions that are used by the Scala runtime: even though ByteBack does not process these system classes’ implementations, it still needs to reason about their specifications and signatures, and how they are (indirectly) used by the program under verification. In fact, the Scala examples also required a larger number of
ed classes to annotate the (implicit) classes used by Scala’s converters.
5 Related Work
Empirical evidence of substitutability violations. As mentioned in Sec. 1, substitutability violations in languages like Java are not merely a theoretical possibility. On the one hand, an empirical study of over 200 thousand classes from open-source Java projects found that “almost all” inheritance relations have some subtype use [29]. This evidence confirms that programmers design software that relies on substitutability via subtyping.
On the other hand, there is also abundant, direct or indirect, evidence that substitutability violations occur in practice. An analysis of over 20 million Java classes found that up to 28% of overridden method may introduce exceptional behavior that is incompatible with substitutability [18]; the same study found similar results when investigating other kinds of effects that break substitutability. Applying random testing techniques to detect substitutability violations [27] found that 30% of the analyzed classes (taken from three popular Java libraries) include crashing substitutes, that is subclasses that may lead to a crash (e.g., with an exception) when they replace an instance of the superclass they inherit from. A recent study of exception preconditions (i.e., preconditions that characterize when a method throws an exception) targeting 46 open-source Java projects and several modules of Java 11’s JDK [19] found several instances of methods that unconditionally throw an UnsupportedOperation exception, possibly leading to a violation of substitutability.
Static analysis of substitutability. Extended type checkers are tools that enrich a programming language’s core type checker with annotations that capture more expressive properties as types. The Checker Framework [7, 25]7 augments the Java compiler with several of such extended type annotations, to detect errors such as for null-pointer dereferencing, optional data, out-of-bound index, and so on. While the Checker Framework does not currently include any checker for immutable or nullable collections,8 it is extensible with new annotations (and some third-party checkers support some form of immutability annotations). The Checker Framework also offers stub files9—a mechanism similar to ByteBack’s
—to annotate libraries whose source code is not available. Of course, an extended type checker like the Checker Framework and a deductive verifier like ByteBack have distinct applications: a type checker is a lightweight tool, which statically verifies, with limited annotation effort, specific properties at the public interface of clients and suppliers; in contrast, a deductive verifier can, in principle, verify arbitrarily complex behavioral properties of every code feature, but also usually requires a substantial annotation effort and highly trained users. Besides, the Checker Framework is primarily a source-level tool, and works only for Java code, whereas ByteBack targets bytecode, and supports multi-language programs.
Other forms of static analysis may also support custom annotations that express immutability or similar properties, providing a similar usability as an extended type checker. For example, the Infer analyzer [4]’s impurity plugin includes an @Immutable annotation,10 which can be used to constrain any kind of object to be immutable.
Deductive verification. A comprehensive behavioral specification language such as JML [14] subsumes the specification features that we introduced in this paper. Therefore, deductive verifiers based on JML, such as OpenJML [6] and KeY [2], can fully reason about behavioral substitutability (and its violations) in a similar fashion as ByteBack. As in previous work [22, 23], our version of ByteBack and verifiers such as KeY and OpenJML offer largely complementary strengths and weaknesses: while the latter support a comprehensive set of specification features, and are much more mature tools, ByteBack’s strengths follow from its unique angle of targeting bytecode-level verification: it seamlessly supports recent versions of Java (in contrast, OpenJML supports mostly Java features up to version 8, and KeY mostly targets a subset of Java 6), and it can also verify programs written in (subsets of) other JVM languages such as Scala and Kotlin, as well as multilingual programs made of components written in different languages (such as in Sec. 2’s example). The
mechanism introduced in the present paper supports adding annotations to an existing component without access to the source code; OpenJML’s specification files11provide a similar functionality for a source-level verifier.12 In all, our contributions to ByteBack further demonstrate how bytecode-level deductive verification can be useful, but are not meant as a replacement of the full-fledged deductive verifiers for Java out there.
On a more theoretical level, there has been work on modeling and reasoning about notions of substitutability that are more flexible than Liskov and Wing [17]’s. Examples include lazy behavioral subtyping [8] and behavioral interface subtyping [21]. These contributions are usually only demonstrated on a core object-oriented language with minimal features; mainstream programming languages such as Java are designed based on stricter (and simpler) typing rules, which are more accessible to ordinary programmers.
6 Conclusions
In this paper, we described an extension of our ByteBack technique [22, 23] to reason about behavioral substitutability properties at the level of JVM bytecode. To this end, we equipped ByteBack with capabilities to specify and reason about ghost specification predicates, a simple form of class invariants, specification inheritance, and a mechanism to annotate library components indirectly, without access to their source code. Our experiments demonstrate that this extension can precisely verify programs that use “optional” features of widely used Java libraries (such as immutable vs. mutable collections), even in multi-language program where client code and libraries are written in two different JVM languages.
The most natural continuation of this work would be equipping ByteBack with a more expressive class invariant specification methodology, which would support reasoning about behavioral substitutability for more complex multi-object structures.
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Intuitively, “aggregable” means that it does not translate to branching instructions in bytecode; see previous work on ByteBack for a precise definition [22].
In ByteBack, a class specification can be split into multiple
ed modules, which in turn can augment (or redefine) an existing source-level specification of the same class; furthermore, ByteBack’s attach mechanism can also redefine implementations of a method in another part of the project under analysis. This makes
a somewhat more flexible mechanism than OpenJML’s spec files and the Checker Framework’s aforementioned stub files, which do not support such a piecemeal specification style and cannot replace implementations.
iff the current instance of 
annotation to augment any compiled class in the system with specification elements. Method 
(it is used for behavioral specifications, and hence any of its implementations must be side-effect free) and
(its value does not depend on the current instance of 
of 
methods, we provide a dummy implementation of
method 
annotation instructs ByteBack to effectively ignore it.
: 
(the current instance of 
’s postcondition, it knows that 
) and postconditions (
), as well as annotations to specify exceptional vs. normal behavior:
specifies a method that throws an exception of class E when it is called on an object where condition c holds; conversely,
specifies a method that returns normally when it is called on an object where condition c holds. For example, Fig. 1c specifies that method 
leads to a verification error iff c does not hold when execution reaches it), assumptions (
ignores all executions where c does not hold), and loop invariants (
captures the fundamental inductive property of the loop where it appears).
, which asserts that property c must hold for all instances of the specified class. For instance, Fig. 1d annotates class 
, which every object \(\ell \) of class 
is simply equivalent to annotating every method of C with a “free”4 precondition I and a (regular) postcondition I, and every constructor of C with a postcondition I. This simple class invariant semantics is sufficient for this paper’s purposes, but it falls short of a full-fledged invariant methodology [5, 12, 15, 16, 26, 28], which should support temporary violations of the class invariant (for example, by private methods), as well as expressing invariants that depend on the state of multiple objects.
. ByteBack checks that every method 
, ii) have a signature consistent with 
methods. Annotation
generalizes the
annotation used in previous work [22, 23], since
also allows recursive calls in a behavior method body. Other annotations further constrain what a behavior method can predicate over. By default, a behavior method 
), as well as to the current object’s state (e.g., through its fields). If 
, it cannot depend on the object state directly. Conversely, if 
, it can also access the current object’s pre-state (the state just before executing 
behaviors are used in postconditions, where they relate the post-state to the pre-state. On the other hand,
behaviors are useful to specify properties that hold “absolutely”, such as 
is especially useful for behavioral substitutability properties like those we reason about in this paper; declaring them as
simplifies framing, since ByteBack only needs to check that their definitions do not refer to the object state.
instructs ByteBack to apply all specification features introduced in S to class C. Precisely, the specification of any method 
refers to specification predicate
of the specified classes 
annotation so that it correctly refers to this attached method 
and
, which define the following pre- and postconditions:
and
, also demonstrated in Fig. 3’s class 
or
, ByteBack generates additional explicit verification conditions that check that all the
s introduce weaker formulas, and the
s introduce stronger formulas. In Fig. 3’s example, ByteBack would check that formulas \(P_{\texttt {A}} \Longrightarrow P_{\texttt {C}}\) and \(Q_{\texttt {C}} \Longrightarrow Q_{\texttt {A}}\) are valid.
annotation enforces this constraint by taking the conjunction of all declared invariants: in Fig. 3, class 
declares a full class invariant explicitly, and checks that it is indeed a strengthening during verification. In Fig. 3, the class invariant of class 
mechanism), they are not available, in general, down the inheritance hierarchy, since the compiler is not aware of their intended semantics. Therefore, ByteBack also takes care of explicitly propagating specifications according to inheritance from the Vimp methods where they were explicitly introduced (see Sec. 3.8). After all these transformations, ByteBack finally encodes the ensemble Vimp components into a Boogie program that faithfully encodes the semantics of the input program and its specification. ByteBack’s output Boogie program can be verified with the Boogie intermediate verifier to determine whether the input JVM program is correct.
, and copies the specification elements from S to C. If an element specified in S already has a specification in C, the attaching process replaces C’s specification with S’s. Attaching can also be used to replace implementations: if a method is declared as
in C but is given an implementation in S, the attaching process copies this implementation into C. Fig. 4 shows an example of attaching: class 
—where 
object representing the class where the referenced specification element was declared, and 
with 
; after attaching, this class invariant annotates class 
is of type 
. Writing directly
as class invariant of 
denotes that class C is a child (heir, direct descendant) subclass of B in such graph. Since Java (as well as other JVM languages) supports a form of multiple inheritance via
s, inheritance is not simply a tree but a DAG, which may have multiple roots (while all classes inherit from 
, or m’s declared pre-/postcondition in C uses
/
, the specification is not propagated from C’s superclasses. Instead, ByteBack generates additional side verification conditions (not shown in Algorithm 1), checking that the following implications hold: 
(i.e., 
), and the number A of attached specification classes (
) .
mechanism described in the paper. The verification goal is checking that the client code uses the data structures’ operations consistently with their specified behavior (as well as with the expected substitutability properties).
,
, and
(discussed in Sec. 3.4).
value to this method is accepted by the Java compiler but results in a 
ed classes to annotate the (implicit) classes used by Scala’s converters.
—to annotate libraries whose source code is not available. Of course, an extended type checker like the Checker Framework and a deductive verifier like ByteBack have distinct applications: a type checker is a lightweight tool, which statically verifies, with limited annotation effort, specific properties at the public interface of clients and suppliers; in contrast, a deductive verifier can, in principle, verify arbitrarily complex behavioral properties of every code feature, but also usually requires a substantial annotation effort and highly trained users. Besides, the Checker Framework is primarily a source-level tool, and works only for Java code, whereas ByteBack targets bytecode, and supports multi-language programs.
mechanism introduced in the present paper supports adding annotations to an existing component without access to the source code; OpenJML’s specification files11provide a similar functionality for a source-level verifier.12 In all, our contributions to ByteBack further demonstrate how bytecode-level deductive verification can be useful, but are not meant as a replacement of the full-fledged deductive verifiers for Java out there.
ed modules, which in turn can augment (or redefine) an existing source-level specification of the same class; furthermore, 
a somewhat more flexible mechanism than OpenJML’s spec files and the Checker Framework’s aforementioned stub files, which do not support such a piecemeal specification style and cannot replace implementations.
