有些问题不好解决，但可能绕过

给出任意一个并发程序，形式上证明其正确性是一个很难的问题。但可不可以这样：抽象出一些常用结构，“预证明”其性质，且保证这个结构有足够的表达力，能较高效率的解决大多数并发编程问题。在构建程序的过程中，每一步我们都可以掌握这个程序的一些性质，只要到最后程序的性质能成为specification的充分条件，就得到一个正确的并发程序了，从而绕过了证明的问题。