Towards Verified Software: Mirror Theory of Programming

ZHANG Junfu; ZHAO Wen; YUAN Chongyi

doi:10.1049/cje.2017.01.023

Volume 26 Issue 2

Turn off MathJax

Article Contents

Article Navigation > Chinese Journal of Electronics > 2017 > 26(2): 279-284

ZHANG Junfu, ZHAO Wen, YUAN Chongyi, “Towards Verified Software: Mirror Theory of Programming,” Chinese Journal of Electronics, vol. 26, no. 2, pp. 279-284, 2017, doi: 10.1049/cje.2017.01.023

Citation:

ZHANG Junfu, ZHAO Wen, YUAN Chongyi, “Towards Verified Software: Mirror Theory of Programming,” Chinese Journal of Electronics, vol. 26, no. 2, pp. 279-284, 2017, doi: 10.1049/cje.2017.01.023

ZHANG Junfu, ZHAO Wen, YUAN Chongyi, “Towards Verified Software: Mirror Theory of Programming,” Chinese Journal of Electronics, vol. 26, no. 2, pp. 279-284, 2017, doi: 10.1049/cje.2017.01.023

Citation:

ZHANG Junfu, ZHAO Wen, YUAN Chongyi, “Towards Verified Software: Mirror Theory of Programming,” Chinese Journal of Electronics, vol. 26, no. 2, pp. 279-284, 2017, doi: 10.1049/cje.2017.01.023

PDF( 865 KB)

Towards Verified Software: Mirror Theory of Programming

doi: 10.1049/cje.2017.01.023

1.
School of Software & Microelectronics, Peking University, Beijing 100871, China;
2.
National Engineering Research Center for Software Engineering, Peking University, Beijing 100871, China

Funds: This work is supported by National Grand Fundamental Research 973 Program of China (No.2009CB320706, No.2010CB32813), National Core-Hightech-Basic Project (No.2010ZX01045-001-008), and the National Nature Science Foundation of China (No.61170001).

Received Date: 2014-09-18
Rev Recd Date: 2015-07-21
Publish Date: 2017-03-10

Abstract

Abstract

A program, when being executed, acts like a mirror that produces mirror images for objects in front of it. A mirror distinguishes itself from others by the way how it changes the shape of an object. A program can be characterized by the way how the final values of variables (the mirror images) are related to the initial values of variables (the objects). Axioms that specify relationships between final values and initial values of variables in a program are proposed. The logic to be discussed in this paper serves to prove and to deduce properties based on given axioms. Both the axioms and the logic belong to a theory, namely the mirror theory of programming, in which a program appears as an operation expression set. It is a step forward towards verified software.
- Operation expression,
- Semantic axiom,
- Programming logic,
- Theory of programming,
- Verified software

FullText(HTML)

References(8)

References

C.A.R. Hoare, He Jifeng, Unifying Theories of Programming, Prentice Hall International Series in Computer Science, 1998.

Yuan Chongyi, Zhao Wen and Huang Yu. "Operation expression:A way to verified software", Proceedings of International Conference on Foundations of Computer Science, Las Vegas, Nevada, USA, pp.91-98, 2010.

Judith Crow, "Formal Methods Specification and Analysis Guidebook for the Verification of Software and Computer Systems", Vol II:A Practitioner's Companion, NASA Office of Safety and Mission Assurance, Washington D.C., USA, 1997.

Lüttgen, G., Muñoz, C., Butler, R., et al., "Towards a customizable PVS", Technical Report ICASE 2000-4, CR-2000-209851, NASA Langley, USA, 2000.

Yuan Chongyi, "Assignment:Operation on a physical object",Journal of Frontiers of Computer Science and Technology, Vol.2, No.5, pp.487-499, 2008.

Yuan Chongyi, Huang Yu and Zhao Wen, "Program:Expressions of operations on physical objects", Journal of Frontiers of Computer Science and Technology, Vol.3, No.2, pp.144-153, 2009.

Yuan Chongyi, Zhao Wen, Gao Xin, et al., "Definitions and Specifications of O-expression properties", Journal of Frontiers of Computer Science and Technology, Vol.4, No.1, pp.20-28, 2010.

Yuan Chongyi, Zhao Wen and Huang Yu, "O-expressions:A petri net representation", Journal of Frontiers of Computer Science and Technology, Vol.4, No.11, pp.961-976, 2010.

Relative Articles

Supplements(0)

Cited By

Proportional views