Abstract
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.
Cite
CITATION STYLE
Zhang, K., & Qiu, Z. (2016). Coq implementation of OO verification framework veriJ. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9763, pp. 270–276). Springer Verlag. https://doi.org/10.1007/978-3-319-41591-8_18
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
