================================================================================
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).