通信进程的最弱前置条件语义

A weakest precondition semantics for communicating processes