================================================================================
CS-N8802 A. Ponse
"Process algebra and Hoare's logic."
A Hoare-like logic is introduced for deriving `partial correctness
assertions' of the form {A}P{B}, where A, B are unary predicates over
some state space S and P is an expression over a recursive, non-uniform
language containing global nondeterminism and sequential composition.
This logic is (relatively) complete if only guarded recursion is
considered.
Key Words & Phrases: process algebra, side-effects,
Hoare's logic, partial correctness assertions.
1985 Mathematical Subject Classification: 68Q55, 68Q60.
1980 Mathematical Subject Classification: 68B10, 68F20.
1982 CR Categories: D.3.1, F.3.1, F.3.2.
Note: The author received full support from the European Communities
under ESPRIT project no. 432, An Integrated Formal Approach to
Industrial Software Development (METEOR).