Open AccessTowards Verified Software: Mirror Theory of Programming
Author(s) -
Zhang Junfu,
Zhao Wen,
Yuan Chongyi
Publication year - 2017
Publication title -
chinese journal of electronics
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.267
H-Index - 25
eISSN - 2075-5597
pISSN - 1022-4653
DOI - 10.1049/cje.2017.01.023
Subject(s) - computer science , software , programming language
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.