New paper: Theory of Programs
Programming, wrote Dijkstra many years ago, is a branch of applied mathematics. That is only half of the picture: the other half is engineering, and this dual nature of programming is part of its attraction.
Descriptions of the mathematical side are generally, in my view, too complicated. This article [1] presents a mathematical theory of programs and programming based on concepts taught in high school: elementary set theory. The concepts covered include:
- Programming.
- Specification.
- Refinement.
- Non-determinism.
- Feasibility.
- Correctness.
- Programming languages.
- Kinds of programs: imperative, functional, object-oriented.
- Concurrency (small-step and large-step)
- Control structures (compound, if-then-else and Dijkstra-style conditional, loop).
- State, store and environment.
- Invariants.
- Notational conventions for building specifications and programs incrementally.
- Loop invariants and variants.
One of the principal ideas is that a program is simply the description of a mathematical relation. The program text is a rendering of that relation. As a consequence, one may construct programming languages simply as notations to express certain kinds of mathematics. This approach is the reverse of the usual one, where the program text and its programming languages are the starting point and the center of attention: theoreticians develop techniques to relate them to mathematical concepts. It is more effective to start from the mathematics (“unparsing” rather than parsing).
All the results (74 properties expressed formally, a number of others in the text) are derived as theorems from rules of elementary set theory; there are no new axioms whatsoever.
The paper also has a short version [2], omitting proofs and many details.
References
[1] Theory of Programs, available here.
[2] Theory of Programs, short version of [1] (meant for quick understanding of the ideas, not for publication), available here.
Eiffel Software
Home page at ETH
Informatics Europe
LASER summer school
Propulsion Academy
It seems according to given definitions (page 2) a program p for non-empty set of states S_p will be functional if and only if relation post_p is empty, because we can take S for C in the definition of functional program.
S \intersect post_p(S) = post_p(S) is empty post_p is empty.
If I understand correctly, the intuition was that for functional program we never get the same state again during computation, i.e. for every sequence
s_0, s_1, …, s_n (where n>=1, and for i>=0 (s_i, s_{i+1}) \in post_p
we always have s_0 != s_n.
This could be written post_p^{+} \intersect id_S = \empty, where id_S is identical binary relation on S and post_p^{+} = \union_{i=1}{\infty} post_p^i