| Process Algebra and Hoare's Logic (2007) | |||||||||||||
Abstract | |||||||||||||
| A Hoare-like logic is introduced for deriving `partial correctness assertions ' of the form fffg p ffig, where ff; fi 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 (\Delta). This logic is (relatively) complete if only guarded recursion is considered. | |||||||||||||
Details der Publikation | |||||||||||||
| |||||||||||||