Modular verification of OO programs with interfaces

Interface types in OO languages support polymorphism, abstraction and information hiding by separating interfaces from their implementations. The separation enhances modularity of programs, however, it causes also challenges to the formal verification. Here we present a study on interface types, and develop a specification and verification theory based on our former veriJ framework. We support multi-specifications for classes inherited from interfaces and the superclass, and keep the verification modularly without re-touching the verified code. The concepts developed in veriJ, namely the abstract specification and specification predicate, play important roles in this extension, and thus are proved widely useful and very natural in the formal proofs of OO programs. ? 2012 Springer-Verlag.EI