Verified collection-based regression test selection via an extended Jinja semantics

The Java Virtual Machine (JVM) postpones running class initialization methods until their classes are first referenced, such as by a new or static instruction. This process is called dynamic class initialization. Jinja is a semantic framework for Java and JVM developed in the theorem prover Isabelle that includes several semantics: Java-level big-step and small-step semantics, JVM-level small-step semantics, and an intermediate compilation step, J1, between these two levels. Regression Test Selection (RTS) algorithms select which tests to rerun on revised code, reducing the time required to check for newly introduced errors. An RTS algorithm is considered safe if and only if all deselected tests would have unchanged results. Ekstazi [1] is a Java library for regression testing. Its algorithm adds print statements to JVM code in order to collect the names of classes used by a test during its execution on a program. When the program is changed, tests are only rerun if a class they used changed. The main insight in their algorithm is that not all uses of classes must be noted, as many necessarily require previous uses, such as when using an object previously created. This thesis presents JinjaDCI, which extends Klein and Nipkow's Jinja [2] to include support for static instructions and dynamic class initialization. Related proofs are extended and updated, including Java-level and JVM-level type safety, equivalence between Java-level big-step and small-step semantics, and the correctness of a compilation from the Java level to the JVM level through J1. The semantics of this extension are based on the Java SE 8 specification. This extension is then used in a formal proof of safety of an RTS algorithm based on that used by Ekstazi. The algorithm formally defined and proved safe here uses an instrumented semantics to collect touched classes in an even smaller set of locations. Problems with Ekstazi's current collection location set that make it not safe are identified, and a modified set that will make it equivalent to the safe set is presented. The theorems given in this thesis have been formalized in the theorem prover Isabelle. The RTS algorithms were modeled via instrumentation of JinjaDCI's JVM semantics. These instrumentations are given via a general definition for Collection Semantics, small-step semantics instrumented to collect information during execution. A formal general definition of RTS algorithms, including a definition of safety, is also given.

Name thesis:degree_name

Ph.D.

Level thesis:degree_level

Dissertation

Discipline thesis:degree_discipline

Computer Science

Grantor

University of Illinois at Urbana-Champaign

Year dc:date

2021

Author dc:creator

• Mansky, Susannah Elizabeth

Contributors dc:contributor

• Gunter, Elsa L
• Rosu, Grigore
• Marinov, Darko
• Lochbihler, Andreas

• interactive theorem proving
• regression test selection
• small-step semantics
• Java
• formal methods
• Isabelle
• Jinja

Statement dc:rights

• Copyright 2020 Susannah Mansky

Language dc:language

en

Handle dc:identifier

http://hdl.handle.net/2142/109396

OAI identifier oai:identifier

oai:www.ideals.illinois.edu:2142/109396