Process Algebra with Guards: Combining Hoare Logic with Process Algebra

摘要

Process algebra with guards, comparable to the guards in guarded commands ofconditions in common programming constructs such as if, then, else, fi and while, do, of are extended. The extended language is provided with an operational semantics based on transitions between pairs of a process and a (data) state. The data states are given by a data environment that also defines in which data states guards hold and how actions (nondeterministically) transform these states. The operational semantics studied is modulo strong bisimulation equivalence. For basic process algebra (without operators for parallelism) a small axiom system that is complete with respect to a general class of data environments is presented. Given a particular data environment S, three axioms are added to this system, which is then again complete, provided weakest preconditions are expressible and S is sufficiently deterministic. Process algebra with parallelism and guards is studied. A two phase calculus is provided that makes it possible to prove identities between parallel processes. This calculus is also complete. It is shown that partial correctness formulas can easily be expressed in this setting. Process algebra with guards is used to prove the soundness of a Hoare logic for linear processes by translating proofs in Hoare logic into proofs in process algebra.