的問題是：驗證：合併報表的正確性
P1 {C} Q1
-------------------------
P1 && P2 {C} Q1||Q2
是此規則是否有效？
我該如何解決這類問題？我能想到的就是試圖找到一個假的例子。
我一直在想它，所以P1 & & P2的組合使Q1和Q2都是假的，但我不能想到任何。所以我傾向於這是有效的，但我不知道該怎麼去證明它...這個類的文本是絕對垃圾，我不能找到任何資源在線的正確性陳述的組合...
我假設這些是Hoare三元組，通常表示爲{P} C {Q};我也使用Wikipedia作爲參考。
所以您的規則：
{P1} C {Q1}
-----------------------
{P1 && P2} C {Q1 || Q2}
是有效的！
{P1} C {Q1}意味着：每當P1成立，Q1將執行命令後C持有 直覺，如果你unterstand邏輯是很清楚的。
P1 && P2成立，P1成立。Q1成立，Q1 || Q2成立。可以拼湊這些語句一起看，爲什麼你的規則必須是有效的：P1 && P2意味着P1，所以當你執行C，您可以通過假設Q1，這意味着Q1 || Q2得到。
因此{P1 && P2} C {Q1 || Q2}，只要你認爲{P1} C {Q1}，這正是你的規則說明。
形式上可以使用下面的規則（摘自維基百科）：
後果規則
P' -> P, {P} C {Q}, Q -> Q'
---------------------------
{P'} C {Q'}
，你只需設置P'爲P1 && P2，P爲P1，Q作爲Q1終於Q'作爲Q1 || Q2。