- 什么是霍尔逻辑: 霍尔逻辑由三个部分组成:
- ϕ被称为前置条件，
- P是程序片段，
- ψ称为后置条件
相关阅读
- https://arxiv.org/pdf/1211.4470.pdf
- C. A. R. Hoare. Proof of correctness of data representations. Acta Inf., 1:271–281, 1972
- Bertrand Meyer. Object-oriented software construction. Prentice Hall, 2nd edition, 1997. First Ed.: 1988.