Towards Verified Software：Mirror Theory of Programming  

作　　者：ZHANG Junfu ZHAO Wen YUAN Chongyi 

机构地区：[1]School of Software & Microelectronics, Peking University, Beijing 100871, China [2]National Engineering Research Center for Software Engineering, Peking University, Beijing 100871, China

出　　处：《Chinese Journal of Electronics》2017年第2期279-284,共6页电子学报（英文版）

基　　金：supported by National Grand Fundamental Research 973 Program of China(No.2009CB320706,No.2010CB32813);National Core-Hightech-Basic Project(No.2010ZX01045-001-008);the National Nature Science Foundation of China(No.61170001)

摘　　要：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.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 

分 类 号：TP311.1[自动化与计算机技术—计算机软件与理论]