A Tutorial Introduction to CSP in Unifying Theories of Programming

摘要

We have presented two UTP theories of programming: one for pre-post specifications (designs), and one for reactive processes. They have been brought together to form a theory of CSP processes. This is the starting point for the unification of the two theories, whose logical conclusion is a theory of state-rich CSP processes. This is the basis for the semantics of a new notation called Circus [255,51], which combines Z and CSP. The theory of designs was only briefly discussed. It is the subject of a companion tutorial [256], where through a series of examples, we have presented the alphabetised relational calculus and its sub-theory of designs. In that paper, we have presented the formalisation of four different techniques for reasoning about program correctness. Even though this is a tutorial introduction to part of the contents of [117], it contains many novel laws and proofs. Notably, the recasting of external choice as a reactive design can be illuminating. Also, the relationship with the failures-divergences model is original.