A Framework for the Interoperable Specification and Verification of Encapsulated Data Structures

Abstract Well-designed data structures are fundamental to the construction of robust programs, particularly when their correctness can be established using formal methods. Currently, various successful deductive verification techniques exist but necessitate distinct and non-interoperable specifications and verification methods for data structure implementations. This paper presents a technique enabling cross-paradigm interoperable specification and verification of encapsulated data structures. The novel approach builds on the shared mathematical foundations of algebraic data types (ADTs) across these diverse methodologies. The technique enables the coherent integration of components that have been verified using different deductive program verification approaches within a single project, provided that a regime of encapsulation is followed, which is slightly stricter than those originally imposed by the verification techniques. We formally introduce and discuss the encapsulation principle using a simplified conceptual object-oriented language and subsequently instantiate it for the Java programming language. This integrates the approaches of KeY, VeriFast, and Universe Types, thereby enabling heterogeneous verification projects in Java that encompass Dynamic Frames, Separation Logic, and Ownership Types. We demonstrate the applicability of our approach by conducting a cooperative verification of a client with three different data structures, each of which is verified with one of the aforementioned techniques.