Porting the software product line refinement theory to the coq proof assistant : a case study

Abstract

Proofs are not a simple task to be performed. Some barriers are also put in place when it comes to checking them, as there are proofs that are so specialized that few people can even understand them or so long that few have time to check them. Computers have been an ally in this sense, as they support those who deal with it, automating all or part of the process, in addition to performing the verification of the proof steps. In this context, we have proofs as sistants that are capable of generating some proof steps automatically, but that still need the collaboration of a user to conduct the process. There are a variety of proof assistants, how ever, with different purposes. A better understanding of strengths and weaknesses regarding these systems can lead to a choice that means less effort for formalization and proof, for instance. In this work, we codified a specification of the software product line refinement theory in the Coq proof assistant. This theory guarantees that we are not introducing errors or changing the behavior of existing products in a product line during an evolution, ensuring a safe evolution. This theory has been specified and proved using the Prototype Verification System (PVS) proof assistant. Nevertheless, the Coq proof assistant is increasingly popular among researchers and practitioners, and, given that some programming languages are al ready formalized into such tool, the refinement theory might benefit from the potential in tegration. Therefore, in this work we present a case study on porting the PVS specification of the refinement theory to Coq. This specification includes specific models such as Feature Model, Asset Mapping, and Configuration Knowledge, as well as instantiation using Type classes and formalizing templates that can be used in SPL evolution scenarios. Moreover, due to the fact that this theory has already been formalized in the PVS, we compare the proof as sistants based on the noted differences between the specifications and proofs of this theory, providing some reflections on the tactics and strategies used to compose the proofs. Accord ing to our study, PVS provided more succinct definitions than Coq, in several cases, as well as a greater number of successful automatic commands that resulted in shorter proofs. Despite that, Coq also brought facilities in definitions such as enumerated and recursive types, and features that support developers in their proofs.