ZHANG Junfu, ZHAO Wen, YUAN Chongyi. Towards Verified Software: Mirror Theory of Programming[J]. Chinese Journal of Electronics, 2017, 26(2): 279-284. doi: 10.1049/cje.2017.01.023
Citation: ZHANG Junfu, ZHAO Wen, YUAN Chongyi. Towards Verified Software: Mirror Theory of Programming[J]. Chinese Journal of Electronics, 2017, 26(2): 279-284. doi: 10.1049/cje.2017.01.023

Towards Verified Software: Mirror Theory of Programming

doi: 10.1049/cje.2017.01.023
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
  • 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.
  • loading
  • 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.
  • 加载中

Catalog

    通讯作者: 陈斌, bchen63@163.com
    • 1. 

      沈阳化工大学材料科学与工程学院 沈阳 110142

    1. 本站搜索
    2. 百度学术搜索
    3. 万方数据库搜索
    4. CNKI搜索

    Article Metrics

    Article views (135) PDF downloads(721) Cited by()
    Proportional views
    Related

    /

    DownLoad:  Full-Size Img  PowerPoint
    Return
    Return