zbMATH — the first resource for mathematics

Proof theory for \(\mu\)CRL: A language for processes with data. (English) Zbl 0813.68135
Andrews, Derek J. (ed.) et al., Semantics of specification languages (SoSL). Proceedings of the International Workshop, Utrecht, the Netherlands, 25-27 October 1993. Berlin: Springer-Verlag. Workshops in Computing. 232-251 (1994).
Summary: A simple specification language, called \(\mu\text{CRL}\) (micro Common Representation Language), is introduced. It consists of process algebra extended with abstract data types. The language \(\mu\text{CRL}\) is designed such that it contains only basic constructs with a straightforward semantics. It has been developed under the assumption that an extensive and mathematically precise study of these constructs and their interaction will yield fundamental insights that are essential to an analytical approach of well-known and much richer specification languages. To this end, a simple property language is defined in which basic properties of processes, data and the process/data relationship can be expressed in a formal way. Next a proof system is defined for this property language, comprising a rule for induction, the Recursive Specification Principle, and process algebra axioms. The proof theory thus obtained is designed such that automatic proof checking is feasible. It is illustrated with a case study of a counter.
For the entire collection see [Zbl 0918.00035].

68Q60 Specification and verification (program logics, model checking, etc.)
68Q65 Abstract data types; algebraic specification
68N15 Theory of programming languages