1

我正在阅读“计算机编程的公理基础”。他们在公理中使用可证明符号⊢,例如

⊢P {Q} R

维基百科将该符号的使用描述为“x ⊢ y 表示 y 可以从 x 证明(在某些指定的形式系统中)”,但这似乎不适合这里。符号是什么意思?

该论文可以在这里找到:http ://www.cs.ucsb.edu/~kemm/courses/cs266/acmhoare69.pdf

4

2 回答 2

6
于 2012-02-10T22:03:40.587 回答
0
⊢P {Q} R

是说“P是程序Q产生结果R的先决条件”

于 2012-02-10T21:35:52.440 回答