Porting the Software Product Line Refinement Theory to the Coq Proof Assistant

Software product lines are an engineering approach to systematically build similar software products from a common asset base. When evolving such systems, it is important to have assurance that we are not introducing errors or changing the behavior of existing products. The product line refinement theory establishes the necessary conditions for such assurance. This theory has been specified and proved using the PVS proof assistant. However, the Coq proof assistant is increasingly popular among researchers and practitioners, and, given that some programming languages are already formalized into such tool, the refinement theory might benefit from the potential integration. Therefore, in this work we present a case study on porting the PVS specification of the refinement theory to Coq. We compare the proof assistants 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. According 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.