迈向软件产品族的构造正确产品变体：GFML，一种用于特征模块的形式化语言

软件产品族工程（SPLE）是一种侧重于复用和可变性的软件工程范式。虽然面向特征的编程（FOP）可以高效实现软件产品族，但我们仍需一种更高效且自动化的方法来生成并证明所有产品变体的正确性。在此背景下，我们提出操作包含三种工件的特征模块：规约、代码和正确性证明。我们描绘了一种方法论和一个平台，帮助用户从相关特征模块自动生成构造正确的产品变体。作为该项目的第一步，我们提出了一种语言 GFML，允许开发者编写此类特征模块。该语言的设计旨在使工件易于复用和组合。GFML 文件包含上述不同工件。其思想是将它们编译为 FoCaLiZe，一种具有面向对象风格的形式化规约、实现和证明语言。在本文中，我们定义并展示了该语言，并通过若干示例介绍了组合特征模块的方法。