面向软件产品线的按构造正确的产品变体：GFML，特征模块的形式语言
Towards correct-by-construction product variants of a software product line: GFML, a formal language for feature modules
摘要：
软件产品线工程（SPLE）是一个软件工程范例，重点是重用和可变性。虽然面向特征的程序设计（FOP）可以有效地实现软件产品线，我们仍然需要一种方法来生成和证明所有的产品变体的正确性更有效和自动。在这种情况下，我们建议操纵功能模块，其中包含三种工件：规范，代码和正确性证明。我们描述了一种方法和一个平台，帮助用户自动生成正确的结构产品的相关功能模块的变体。作为这个项目的第一步，我们首先提出一种语言，GFML，允许开发人员编写这样的功能模块。这种语言的设计是为了使工件可以很容易地重用和组合。GFML文件包含上面提到的不同工件。我们的想法是将它们编译成FoCaLiZe，一种具有面向对象风格的规范，实现和形式证明语言。在本文中，我们定义和说明这种语言。并结合实例介绍了一种功能模块的组合方法。
英文摘要：
Software Product Line Engineering (SPLE) is a software engineering paradigm that focuses on reuse and variability. Although feature-oriented programming (FOP) can implement software product line efficiently, we still need a method to generate and prove correctness of all product variants more efficiently and automatically. In this context, we propose to manipulate feature modules which contain three kinds of artifacts: specification, code and correctness proof. We depict a methodology and a platform that help the user to automatically produce correct-by-construction product variants from the related feature modules. As a first step of this project, we begin by proposing a language, GFML, allowing the developer to write such feature modules. This language is designed so that the artifacts can be easily reused and composed. GFML files contain the different artifacts mentioned above.The idea is to compile them into FoCaLiZe, a language for specification, implementation and formal proof with some object-oriented flavor. In this paper, we define and illustrate this language. We also introduce a way to compose the feature modules on some examples.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
