Product Lines of Theorems

Benjamin Delaware, William R. Cook, Don Batory

abstract

Mechanized proof assistants are powerful verification tools, but proof development can be difficult and time-consuming. When verifying a family of related programs, the effort can be reduced by proof reuse. In this paper, we show how to engineer product lines with theorems and proofs built from feature modules. Each module contains proof fragments which are composed together to build a complete proof of correctness for each product. We consider a product line of programming languages, where each variant includes metatheory proofs verifying the correctness of its semantic definitions. This approach has been realized in the Coq proof assistant, with the proofs of each feature independently certifiable by Coq. These proofs are composed for each language variant, with Coq mechanically verifying that the composite proofs are correct. As validation, we formalize a core calculus for Java in Coq which can be extended with any combination of casts, interfaces, or generics.

Feature Modules
cFJ.v Extensible syntax and semantics for core Featherweight Java.
Cast.v Extensions for casts.
Interface.v Extensions for interfaces.
Generic.v Extensions for generics.
Generic_Interface.v Extensions for generic interfaces.
Generic_Cast.v Extensions for generic casts.
Additional Files
Makefile Makefile to build all the above languages.
FJ_tactics.v Custom tactics used in the case study.
Composed Language Source Files
    uFJ.v Syntax and semantics of core Featherweight Java.
        FJ.v Syntax and semantics of core Featherweight Java + Casts (FJ).
        uIFJ.v Syntax and semantics of core Featherweight Java + Interfaces.
            iFJ.v Syntax and semantics of Featherweight Java + Interfaces.
        GFJ.v Syntax and semantics of core Featherweight Java + Generics.
                GiFJ.v Syntax and semantics of core Featherweight Java + Generics + Interfaces.
                FGJ.v Syntax and semantics of Generic Featherweight Java.
                            GiFJ.v Syntax and semantics of Generic Featherweight Java + Interfaces.