assert - 验证：结合正确性陈述

Question

问题是：

        P1 {C} Q1
-------------------------
   P1 && P2 {C} Q1||Q2

这个规则有效吗？

我将如何处理这样的事情？我所能想到的就是试图找到一个错误的例子。

我一直在尝试想出它，以便 P1 && P2 的组合使 Q1 和 Q2 都为假，但我想不出任何一个。所以我倾向于这是有效的，但我不知道去哪里证明它......这门课的文字绝对是垃圾，我在网上找不到任何资源来组合正确性陈述......

Answer 1

我假设这些是 Hoare 三元组，通常表示为{P} C {Q}; 我也使用维基百科作为参考。

所以你的规则：

      {P1} C {Q1}
-----------------------
{P1 && P2} C {Q1 || Q2}

已验证！

直观上，如果您理解逻辑，就很清楚了：

• {P1} C {Q1}意思是：无论何时P1保持，Q1执行命令后将保持C。
• 你知道，如果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'as P1 && P2，Pas P1，QasQ1和 finally Q'as Q1 || Q2。