Prove it! Inferring Formal Proof Scripts from CafeOBJ Proof Scores

摘要

CafeOBJ is a language for writing formal specifications for a wide variety of software and hardware systems and for verifying their properties. CafeOBJ makes it possible to verify properties by using either proof scores, which consists of reducing goal-related terms in user-defined modules, or by using theorem proving. While the former is more flexible, it lacks the formal support to ensure that a property has been really proven. On the other hand, theorem proving might be too strict, since only a predefined set of commands can be applied to the current goal; hence, it hardens the verification of properties.In order to take advantage of the benefits of both techniques, we have extended CafelnMaude, a CafeOBJ interpreter implemented in Maude, with the CafelnMaude Proof Assistant (CiMPA) and the CafelnMaude Proof Generator (CiMPG). CiMPA is a proof assistant for proving inductive properties on CafeOBJ specifications that uses Maude metalevel features to allow programmers to create and manipulate CiMPA proofs. On the other hand, CiMPG provides a minimal set of annotations for identifying proof scores and generating CiMPA scripts for these proof scores. In this article, we present the CiMPA and CLMPG, detailing the behavior of the CiMPA and the algorithm underlying the CiMPG and illustrating the power of the approach by using the QLOCK protocol. Finally, we present some benchmarks that give us confidence in the matureness and usefulness of these tools.