A practical theory of programming (Q808685)

The authors propose the new theory of programming, in which programs are predicates, programming is proving and termination is timing. The specification of computer behavior to be a predicate in the initial (input) and final (output) values is considered. All well understood predicates are allowed as predicates. Some useful notation from the application area may be defined (for example, if-then-else construction, sequential composition and so on). A program in this theory is a predicate. This is simpler than \textit{Dijkstra}'s \(wp\) and \textit{Jones}' \({\mathcal V}{\mathcal D}{\mathcal M}\). The notion of refinement is also simpler: universaly quantified implication. The problems of sequential and concurrent computations, communicating processes, infinite interactive computations are solved in the frames of this theory.