Abstract:

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

Key words: limit; two-thirds bi-simulation; correctness; formalization