在形式规格说明的获取任务中,一个重要问题是验证获取得到的形式规格说明的正确性.即给定一个问题需求P,往往可以获取多种不同形式的规格说明,如何验证这些不同形式的规格说明均正确?问题需求的非(半)形式化与形式规格说明的形式化两者之间差异的本性,使得该问题成为软件需求工程中一个具有挑战性的问题.提出一种基于形式化推导的方法来验证同一问题不同形式规格说明的相对正确性,通过证明不同形式规格说明与问题需求某个最为直截明了的形式规格说明S_i等价来实现,而S_i使用PAR 方法和PAR 平台转换为可执行程序,通过测试已经得到确认.为了支持该方法,进一步提出了扩展的逻辑系统和辅助证明算法.使用Radl 语言作为形式规格说明语言,通过排序搜索、组合优化领域的两个典型实例对该方法进行了详细的阐述.实际使用效果表明,该方法不仅能够有效地验证Radl 形式规格说明的正确性,还具备良好的可扩充性.该方法在规格说明的正确性验证、算法优化、程序等价性证明等研究领域具有潜在的理论意义与应用价值.

During the task of acquiring formal specification, an important problem is verifing the correctness of acquired formal specification. In other words, given a problem requirement P, a variety of formal specifications will be acquired, but how to verify the correctness of them all? The different nature of the non- (semi-) formal of problem requirement and formal of specification makes it a challenging software problem and requirement for engineering. This paper proposes a formal derivation method to verify the relative correctness of different forms of Radl specifications corresponding same problem. It achieves this through a proof of the equivalency among different forms of Radl specifications and a certain formal specification S_i, which is straightforward to the problem requirement. S_i is converted into an execute program using PAR method and PAR platform, and is validated by test. In order to support the method, the study further put forth an extended logic system and aided certified algorithm. This paper uses Radl as formal specification language and elaborates the method using two typical examples in the domains of sort and search, combinational optimization. Practical effects manifest not only can effectively verify relatively correctness of Radl specification, but also has well extendibility. The method has potential theory significance and application value in research areas of formal specifications correctness verification, algorithms optimization and programs equivalency proof.

国家自然科学基金重大国际(地区)合作与交流项目(61020106009); 国家自然科学基金(61272075); 江西省自然科学青年科学基金(201222BAB211030)