Question

我想问是否有人能帮我回答这个问题。这是以前一份考试论文的答案,我可以知道这个年度考试的答案。

这个问题似乎如此简单,以至于我完全迷失了方向,到底要问什么?

考虑以下涉及整数变量的代码部分:
if (i < j) {
    m = i;
} else {
    m = j;
}
By stating an appropriate output condition and then verifying the correctness of the piece of code, prove that after execution, m is equal to the minimum of i and j.

I have got the post condition as: {m = i ∧ i < j ∨ m = j ∧ j < i}

这是正确的吗?你如何核实这一点?

Answer 1

您的邮政条件是正确的。我个人认为以下的变体( 相当于) 比较自然 :

(i<j → m=i) ∧ (i≥j → m=j)

为证明此程序符合邮寄条件,您可做以下工作:

请注意,要确定程序 ways 符合您应该使用 true 作为您预设条件的邮政条件。

所以,你有以下的Haare三重:

{true}
if (i < j) {


    m = i;

} else {


    m = j;

}
{(i < j → m = i) ∧ (i ≥ j → m = j)}

条件必须维持在两个分支的尽头,因此(根据标准最弱的有条件先决条件规则)我们有:

{true}
if (i < j) {


    m = i;
    {(i < j → m = i) ∧ (i ≥ j → m = j)}     <--.
} else {                                       |
                                               |
                                               |
    m = j;                                     |   copy
    {(i < j → m = i) ∧ (i ≥ j → m = j)}     <--|
}                                              |
{(i < j → m = i) ∧ (i ≥ j → m = j)}  ----------

根据分配产量最薄弱的先决条件,进一步推进公式

{true}
if (i < j) {

    {(i < j → i = i) ∧ (i ≥ j → i = j)}   <---.
    m = i;                                    | m replaced by i
    {(i < j → m = i) ∧ (i ≥ j → m = j)}   ---- 
} else {

    {(i < j → j = i) ∧ (i ≥ j → j = j)}   <---.
    m = j;                                    | m replaced by j
    {(i < j → m = i) ∧ (i ≥ j → m = j)}   ---- 
}
{(i < j → m = i) ∧ (i ≥ j → m = j)}

在真实分支的顶端,我们知道 i< j , 在其它分支的顶端,我们知道 :

{true}
if (i < j) {
    {i < j}                               (1)  <--- added
    {(i < j → i = i) ∧ (i ≥ j → i = j)}   (2)
    m = i;
    {(i < j → m = i) ∧ (i ≥ j → m = j)}
} else {
    {¬(i < j)}                            (3)  <--- added
    {(i < j → j = i) ∧ (i ≥ j → j = j)}   (4)
    m = j;
    {(i < j → m = i) ∧ (i ≥ j → m = j)}
}
{(i < j → m = i) ∧ (i ≥ j → m = j)}

对于任何连续两个说法,第一种说法就意味着第二种说法。 (这些说法通常被称为“补充义务”。 )我们有两种这类义务: < code>(1) 应该意味着 < code > (2) , < code > (3) 应该意味着 < code > (4) 。情况显然如此。

- "qed": -)

友情链接