软件动态正确性的形式化描述

软件正确性是一个逐渐改进的过程.通过不断地修改,软件越来越接近于正确.同时软件的执行依赖于环境.为了刻画软件的动态正确性并考虑环境的因素,以参数化互模拟为基础,利用极限的观点,建立软件动态正确性的形式化描述.首先建立参数化互模拟的无限演化理论,给出参数化极限互模拟的定义,并给出几个特殊的参数化极限互模拟实例.其次,建立参数化互模拟极限，给出参数化互模拟极限的规约刻画. 最后,证明参数化互模拟极限的唯一性、与参数化互模拟的相容性等代数性质.

Formal Description of Software Dynamic Correctness

Correctness is a key attribute of software trustworthiness. Abstractly, software correctness can be represented as whether or not the implementation of software satisfies its specification. However, in the real world, it is difficult to get the satisfaction absolutely. In the course of developing and designing software, implementation is often modified in order to satisfy its specification. This means that the software is more and more close to correctness, i.e. software correctness is a dynamic course. In order to describe the dynamic correctness of software, in this paper, the abstract characterization and the limit theory of dynamic correctness based on parameterized bisimulation are proposed. Firstly, the infinite evolution mechanism of parameterized bisimulation is established. Parameterized limit bisimulation is defined in order to characterize the relation between a series of software implementations obtained in the real design and its specification, and some special examples are shown. Secondly, parameterized bisimulation limit is given, and the recursive characterization of parameterized bisimulation limit is stated. Finally, some algebraic properties are proved, such as the uniqueness of parameterized bisimulation limit and the consistence between parameterized bisimulation limit and parameterized bisimulation.