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

Mansky, Susannah Elizabeth

Permalink

https://hdl.handle.net/2142/109396 Copy

Description

Title

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

Author(s)

Mansky, Susannah Elizabeth

Issue Date

2020-11-30

Director of Research (if dissertation) or Advisor (if thesis)

Gunter, Elsa L

Doctoral Committee Chair(s)

Gunter, Elsa L

Committee Member(s)

• Rosu, Grigore
• Marinov, Darko
• Lochbihler, Andreas

Department of Study

Computer Science

Discipline

Computer Science

Degree Granting Institution

University of Illinois at Urbana-Champaign

Degree Name

Ph.D.

Degree Level

Dissertation

Keyword(s)

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

Abstract

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.

Graduation Semester

2020-12

Type of Resource

Thesis

Permalink

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

Copyright and License Information

Copyright 2020 Susannah Mansky

Owning Collections