Unifying Theories of ProgrammingThis book provides a synthesis of the theory of programming. It aims to use mathematical theory of programming to provide a similar basis for specification, design and implementation of programs. It is wide ranging both in its subject matter and also in its approach and style. The first five chapters justify and introduce the main concepts and methods to be used within the text, relating the goal of unification to the achievements of other branches of science and mathematics. The remaining chapters introduce more advanced programming language features one by one. The main methods of programming are summarised and concluded in a manner suitable for those already familiar with programming semantics. Definitions are accompanied by examples and the theorems by meticulous proof. |
Contents
The Challenge of Unification 135 | 1 |
vi | 13 |
The Logic of Engineering Design | 22 |
Copyright | |
12 other sections not shown
Common terms and phrases
abstract ACP processes action algebraic laws alphabet assignment behaviour bisimilarity bisimulation buffer C.A.R. Hoare calculation choice clock Communicating Sequential Processes complete lattice components Computer Science concurrent conjunction CSP3 data flow process declarative defined definition denotational semantics disjoint disjunction engineering equations event example execution expressed false final value finite fixed point free variables function Galois connection global variables healthiness conditions idempotent implementation inequations initial value input channel interleaving jump label Lemma logic logic programming machine code mathematical monotonic non-determinism non-deterministic normal form notation observation operands operational semantics output channel P₁ parallel composition parameter possible postcondition predicates describing procedure programming language Proof properties prove reactive process reasoning recursion relation result satisfies Section sequence sequential composition shared variables SKIP specification step subset synchronisation terminate Theorem theory of programming tion true wait weakest fixed point