管程的验证和Hoare系统的不完全性

本文讨论管程(Monitor)的验证技术。指出了Howard的证明规则是不一致的,并证明了不存在验证管程的一致和完全的正规Hoare系统。Ciarke证明了,对于功能很强的语句——递归过程,Hoare系统是不完全的;本文的结果表明Hoare系统对并发现象中复杂的控制转移结构也是不完全的。