守卫命令语言 编辑
守卫命令语言是艾兹赫尔·戴克斯特拉为谓词变换语义定义的一门语言。它以精简方式组合了编程概念，它们处在以某种实际的编程语言书写程序之前。它的简单性使得采用霍尔逻辑证明程序的正确性更加容易。
1