Safety of a smart classes-used regression test selection algorithm.

*(English)*Zbl 07313965
Nalon, ClĂˇudia (ed.) et al., Proceedings of the 15th international workshop on logical and semantic frameworks, with applications, LSFA 2020, virtual workshop, August 27–28, 2020. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 351, 51-73 (2020).

Summary: 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. In this paper, we present a formal proof of safety of an RTS algorithm based on that used by Ekstazi [Gligoric, M., L. Eloussi and D. Marinov, Practical regression test selection with dynamic file dependencies, in: Proceedings of the 2015 International Symposium on Software Testing and Analysis, ISSTA 2015 (2015), p. 211-222. URL https://doi.org/10.1145/2771783.2771784], a Java library for regression testing. Ekstazi’s 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. The algorithm we formally define and prove safe here uses an instrumented semantics to collect touched classes in an even smaller set of locations. We identify problems with Ekstazi’s current collection location set that make it not safe, then present a modified set that will make it equivalent to our safe set. The theorems given in this paper have been formalized in the theorem prover Isabelle over JinjaDCI [Mansky, S. and E. L. Gunter, Dynamic class initialization semantics: A jinja extension, in: Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019 (2019), p. 209-221. URL https://doi.org/10.1145/3293880.3294104], a semantics for a subset of Java and JVM including dynamic class initialization and static field and methods. We instrumented JinjaDCI’s JVM semantics by giving a general definition for Collection Semantics, small-step semantics instrumented to collect information during execution. We also give a formal general definition of RTS algorithms, including a definition of safety.

For the entire collection see [Zbl 1451.68025].

For the entire collection see [Zbl 1451.68025].

##### MSC:

03B70 | Logic in computer science |

68Q55 | Semantics in the theory of computing |

68T27 | Logic in artificial intelligence |

PDF
BibTeX
XML
Cite

\textit{S. Mansky} and \textit{E. L. Gunter}, Electron. Notes Theor. Comput. Sci. 351, 51--73 (2020; Zbl 07313965)

Full Text:
DOI

##### References:

[1] | Biswas, S.; Mall, R.; Satpathy, M.; Sukumaran, S., Regression test selection techniques: A survey, Informatica (Slovenia), 35, 289-321 (2011) |

[2] | Gadducci, F.; Santini, F.; Pino, L. F.; Valencia, F. D., A labelled semantics for soft concurrent constraint programming, (Holvoet, T.; Viroli, M., Coordination Models and Languages (2015)), 133-149 |

[3] | Gligoric, M.; Eloussi, L.; Marinov, D., Practical regression test selection with dynamic file dependencies, (Proceedings of the 2015 International Symposium on Software Testing and Analysis. Proceedings of the 2015 International Symposium on Software Testing and Analysis, ISSTA 2015 (2015)), 211-222 |

[4] | Klein, G.; Nipkow, T., A machine-checked model for a java-like language, virtual machine, and compiler, ACM Trans. Program. Lang. Syst., 28, 619-695 (2006) |

[5] | Lindholm, T.; Yellin, F.; Bracha, G.; Buckley, A., The Java Virtual Machine Specification: Java SE 8 Edition (2015) |

[6] | Lochbihler, A., Jinja with threads, The Archive of Formal Proofs (2007) |

[7] | Mansky, S.; Gunter, E. L., Dynamic class initialization semantics: A jinja extension, (Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs. Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019 (2019)), 209-221 |

[8] | Mansky, W.; Peng, Y.; Zdancewic, S.; Devietti, J., Verifying dynamic race detection, (Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs. Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017 (2017)), 151-163 |

[9] | Nagarakatte, S.; Zhao, J.; Martin, M. M.; Zdancewic, S., Softbound: Highly compatible and complete spatial memory safety for c, (Proceedings of the 30th ACM SIGPLAN Conference on Programming Language Design and Implementation. Proceedings of the 30th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’09 (2009)), 245-258 |

[10] | Rothermel, G.; Harrold, M. J., Analyzing regression test selection techniques, IEEE Transactions on software engineering, 22, 529-551 (1996) |

[11] | Skoglund, M.; Runeson, P., Improving class firewall regression test selection by removing the class firewall, International Journal of Software Engineering and Knowledge Engineering, 17, 359-378 (2007) |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.