的问题是：验证：合并报表的正确性
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。