使用 Isabelle 证明（命令式）算法的正确性和终止

Question

我是一名本科生，正在尝试证明欧几里德gcd命令式版本和欧几里德扩展gcd算法的正确性和终止性。我用IMP语言实现了第一个，Hoare逻辑证明了正确性和终止：

lemma "⊢{λs. s ''a'' = n ∧ s ''b'' = m ∧ n > 0 ∧ m > 0 ∧ (gcd (s ''a'') (s ''b'') = gcd (n) (m))}
        WHILE (Or (Less (V ''b'') (V ''a'')) (Less (V ''a'') (V ''b'')))
        DO (IF (Less (V ''b'') (V ''a'')) THEN
               (''a'' ::= Sub (V ''a'') (V ''b''))
            ELSE
               (''b'' ::= Sub (V ''b'') (V ''a'')))
        {λs. s ''a'' = gcd (s ''A'') (s ''B'')}"
  apply (rule While'[where P = "λs. s ''a'' = n ∧ s ''b'' = m ∧ 0 < n ∧ 0 < m ∧ gcd (s ''a'') (s ''b'') = gcd n m"])
  apply auto
    apply (rule Assign')
    apply auto
    prefer 2
    apply (rule Assign')
  apply auto

剩余的子目标是：

proof (prove)
goal (3 subgoals):
 1. ⋀s. 0 < s ''a'' ⟹ m = s ''b'' ⟹ n = s ''a'' ⟹ s ''a'' < s ''b'' ⟹ False
 2. ⋀s. 0 < s ''b'' ⟹ m = s ''b'' ⟹ n = s ''a'' ⟹ s ''b'' < s ''a'' ⟹ False
 3. ⋀s. n = s ''a'' ⟹ m = s ''a'' ⟹ 0 < s ''a'' ⟹ s ''b'' = s ''a'' ⟹ s ''a'' = gcd (s ''A'') (s ''B'')

我现在不知道如何完成证明。这里的 gcd 函数是 GCD 库中的默认 gcd。我还尝试了 Arith2 库中的这个定义：

definition cd :: "[nat, nat, nat] ⇒ bool"
  where "cd x m n ⟷ x dvd m ∧ x dvd n"

definition gcd :: "[nat, nat] ⇒ nat"
  where "gcd m n = (SOME x. x>0 ∧ cd x m n & (∀y.(cd y m n) ⟶ y dvd x))"

我写的是否正确，我应该如何继续？我应该改用这些定义还是应该自己编写 gcd 函数的递归版本？这种做法正确吗？

Answer 1

首先，你在一个地方有一个类型，在那里你谈论 s ''A'' 和 s ''B'' 而不是 s ''a'' 和 s ''b''。但这当然不是你问的问题。

这里的问题是前提条件太强而无法使用 WHILE 规则。它包含条件 s ''a'' = n 和 s ''b'' = m，这显然不能用作循环不变量，因为循环修改了变量 a 和 b，因此在一次循环迭代后，一个的条件 s ''a'' = n 和 s ''b'' = m 将不再成立。

你需要找出一个比你现在拥有的更弱的适当不变量。你要做的就是踢出s ''a'' = n和s ''b'' = m。然后你的证明就通过了。

然后您可以使用 strengthen_pre 规则恢复您实际想要显示的语句。

所以你的证明的开头看起来像这样：

lemma "⊢{λs. s ''a'' = n ∧ s ''b'' = m ∧ n ≥ 0 ∧ m ≥ 0 ∧ (gcd (s ''a'') (s ''b'') = gcd (n) (m))}
        WHILE (Or (Less (V ''b'') (V ''a'')) (Less (V ''a'') (V ''b'')))
        DO (IF (Less (V ''b'') (V ''a'')) THEN
               (''a'' ::= Sub (V ''a'') (V ''b''))
            ELSE
               (''b'' ::= Sub (V ''b'') (V ''a'')))
        {λs. s ''a'' = gcd (s ''a'') (s ''b'')}"
  apply (rule strengthen_pre) 
  defer
   apply (rule While'[where P = "λs. s ''a'' ≥ 0 ∧ s ''b'' ≥ 0 ∧ gcd (s ''a'') (s ''b'') = gcd n m"])

为了避免这种笨拙的手动使用strengthen_pre，其他版本的 IMP 允许直接在算法本身中注释 WHILE 循环的不变量，这样 VCG（验证条件生成器）可以自动为您提供所有你必须证明的事情，你不必手动应用霍尔规则。

附录： 但是请注意，您的后置条件也存在问题：

{λs. s ''a'' = gcd (s ''a'') (s ''b'')}

这不是你想展示的！这只是意味着 a 执行后的值是 a 和 b 执行后 的值的 GCD。这也恰好是真的，因为 a 和 b 在算法完成后总是相等的——但你真正想知道的是执行后 a 的值等于a 和 b 在执行之前的 GCD，即等于 gcd n m。因此，您必须将后置条件更改为

{λs. s ''a'' = gcd n m}

使用 Isabelle 证明（命令式）算法的正确性和终止

Proving correctness and termination of an (imperative) algorithm using Isabelle

isabelle

hoare-logic