Towards Verified Software: Mirror Theory of Programming

摘要

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.