Skip to main content

霍尔逻辑_从快排开始

· One min read
  • 什么是霍尔逻辑: 霍尔逻辑由三个部分组成:
  • ϕ被称为前置条件,
  • 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.