基于环境的软件正确性形式化描述

The formal description of software correctness based on the environment

软件的运行依赖于环境,在考察软件正确性时需要考虑环境的因素。软件在开发和设计过程中,其正确性是一个逐渐改进的过程,也就是说,通过不断地修改,软件越来越接近于正确。为了刻画软件的这种动态正确性并考虑环境的因素,本文将以三分之二互模拟为基础,利用网极限的观点,建立软件动态正确性的形式化描述。首先建立三分之二互模拟的无限演化理论,给出三分之二极限互模拟的定义。其次建立三分之二互模拟极限,这个极限在一定程度上反映软件规范是其实现的极限形式。最后证明三分之二互模拟极限与三分之二互模拟的相容性等性质。

Correctness is a key attribution for software trustworthiness.Abstractly,it can be represented by whether or not the implementations of the software satisfy its specification.Also,the correctness is related to its execution environment.On the other hand,the correctness is a course of modifying implementation,i.e.,the software is closer and closer to correctness.In order to describe the dynamic correctness of software,the abstract characterization of dynamic correctness is proposed based on two-third bi-simulation.First,two-thirds limit bi-simulation is defined which reflects the course of modification implementation.Second,the two-third bi-simulation limit is presented which means that the specification of the software is the limit of its implementations.Finally,some algebraic properties are proved.