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

Question

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

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值的GCDafter执行。这也恰好是正确的，因为 a 和 b 在算法完成后始终相等 - 但您真正想知道的是 a< 的值/code>执行后等于a和b执行前的GCD，即等于gcd n m.因此，您必须将后置条件更改为

{λs. s ''a'' = gcd nm}