• Provide an axiomatic approach to dealing with the operations in Java packages to enhance the capability of Testing-Based Formal Verification (TBFV)　
• Establish axioms to define the formal semantics of the most commonly used operations (methods) in the Vector, ArrayList, and LinkdList classes.
• Discuss the effectiveness and limitations of TBFV through examples and small experiments.

　Software testing can detect bugs in programs but cannot tell their absence. Deductive formal verification based on predicate logic and formal semantics of programming languages can tell whether a program is correct but faces considerable difficulties in application. How testing can be combined with formal verification to allow us to take their advantages and avoid their disadvantages is an interesting but challenging problem for research. Aiming to provide a solution to this problem, we proposed Testing-Based Formal Verification (TBFV) in our previous research project to explore how formal specification-based testing and Hoare logic can be integrated to allow automatic formal verification of the correctness of program paths.

　TBFV is characterized by automatically generating test cases from a functional scenario defined in a formal specification, forming the theorem for the correctness of the traversed program path in the testing, and proving the theorem to determine whether the path is correct with respect to the corresponding functional scenario. Despite the promising new direction in software verification indicated by TBFV, applying TBFV to practical software systems still faces several challenges. One important challenge is how to deal with operations defined in software packages since the present TBFV technique does not provide available axioms to allow the reasoning about the operations.

　To enhance the capability of TBFV, in this paper we provide an axiomatic approach to dealing with this problem. After briefly introducing the overall idea of TBFV and the related element techniques, such as test case generation and path theorem formation, we focus on the Vector, ArrayList, and LinkedList classes in Java and present a set of axioms defining the correctness of the major operations offered by these classes. We use examples to illustrate how the axioms can be used for formal verification and analyze their effectiveness and limitations through small experiments.

　Despite the progress we have made about TBFV, our study has also found some challenges for our approach. In theory, our approach could be automatically applied to derive the precondition of a traversed path from a postcondition (defining condition in the corresponding functional scenario) with the defined axioms. The verification of the validity of the formed theorems can also be automatically performed using the automatic predicate-based testing method developed previously. However, to make the automatic testing technique effective, the implemented program must preserve the signature of its specification (e.g., the names of variables). One way to ensure this 1:1 relation is through automatic signature preserving transformation from specifications to programs, but practitioners may not apply this kind of transformation when constructing programs in practice. Another challenge is the lack of a tool support for our approach. This would make our approach rather difficult to apply efficiently to large-scale programs. These problems need to be addressed in our future research projects.

Reference
A. Liu and S. Liu, "Enhancing the Capability of Testing-Based Formal Verification by Handling Operations in Software Packages," in IEEE Transactions on Software Engineering, vol. 49, no. 1, pp. 304-324, 1 Jan. 2023, doi: 10.1109/TSE.2022.3150333.