Coq Implementation of OO Verification Framework VeriJ

We implement an OO specification and verification framework VeriJ in the proof assistant Coq. This framework covers the main OO features like encapsulation, inheritance and polymorphism. It can modularly specify and verify programs, while only one specification per method is necessary. In this paper, we introduce the framework VeriJ, our tool in Coq, and an example to illustrate how to specify/verify the program in a modular and abstract way.EICPCI-S(ISTP)zksms@pku.edu.cn; qzy@math.pku.edu.cn270-276976