A practical theory of programming

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.

Recommendations

Cited in

(12)

This page was built for publication: A practical theory of programming

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q808685)