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

is saying that "P is a precondition for a program Q to produce result R"

于 2012-02-10T21:35:52.440 に答える