J4 ›› 2011, Vol. 46 ›› Issue (9): 22-27.

• Articles • Previous Articles     Next Articles

The formal description of software correctness based on environment

MA Yan-fang1, ZHANG Min2,3, CHEN Yi-xiang2,3   

  1. 1. School of Computer Science and Technology, Huaibei Normal University, Huaibei 235000, Anhui, Chian;
    2. Institue of Theoretical Computing of East China Normal University, Shanghai 200062, China;
    3. Shanghai Key Laboratory of Trustworthy Computing, Shanghai 200062, China
  • Received:2011-06-16 Online:2011-09-20 Published:2011-09-08


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

No related articles found!
Full text



No Suggested Reading articles found!