操作系统形式化验证实践教程(7) - C代码的自动验证（转载）

操作系统形式化验证实践教程(7) - C代码的自动验证
上一节教程不知道大家看晕了没有，其实虽然细节很多还没有讲清楚，但是从结构上大家可以看到，其实是很模式化的工作。
那么能不能让这个模式化的工作自动化起来，也能降低一点入门的学习门槛？这时就该AutoCorres工具出马了。

AutoCorres
既然回到人间，不用再看着一排的simp, vcg之类的，咱们的难度又回到第一讲加减法的时代。

先实现一个C语言实现加法的函数：

unsigned int plus(unsigned int a, unsigned int b)
{
return a + b;
}
1
2
3
4
下面开始写HOL，先引入AutoCorres：

imports
“AutoCorres.AutoCorres”
1
2
然后还是把C源文件读进来，并且install了：

external_file “plus.c”
install_C_file “plus.c”
1
2
然后给c文件autocorres一下：

autocorres “plus.c”
1
按照惯例locale一下：

context plus begin
1
实际上执行的是：

locale Plus.plus
fixes symbol_table :: “char list ⇒ 32 word”
1
2
万事俱备，我们现在已经能读懂C代码了。

通过by eval验证具体例子
先写个case验证下：

lemma “plus’ 128 127 = 255”
1
C代码既然懂了，就直接unfold一下：

unfolding plus’_def
1
验证对不对，执行一下by eval，完整代码如下：

lemma “plus’ 128 127 = 255”
unfolding plus’_def
by eval
1
2
3
演绎验证
例子只能证明在这一种情况下是正确的，但无法证明在所有情况下都正确。我们有没有办法证明所有情况下都正确呢？
可以的，我们不用by eval了，换个apply的规则就好了：

lemma plus_correct: “plus’ a b = a + b”
unfolding plus’_def
apply (rule refl)
done

我们来看下目标：

proof (prove)
goal (1 subgoal):

a + b = a + b

这真的也没啥可以证的了。。。

自动生成定理和证明
我们乘胜追击，再来搞个最大值的：

unsigned max(unsigned a, unsigned b)
{
if (a <= b) {
return b;
}
return a;
}

后面没啥惊喜的，一条龙：imports AutoCorres, external_file, install_C_file, autocorres, unfolding:

imports
“AutoCorres.AutoCorres”
begin

external_file “simple.c”

install_C_file “simple.c”

autocorres “simple.c”

context simple begin

lemma “max’ a b = max a b”
unfolding max’_def max_def
by (rule refl)

下面我们来个更强大的，自动生成定理和证明：

thm simple.max’_def simple.max’_ac_corres
1
生成的结果如下：

simple.max’ ?a ?b ≡ if ?a ≤ ?b then ?b else ?a
ac_corres (simple.lift_global_heap ∘ globals) True
simple_global_addresses.Γ ret__unsigned_’
((λs. a_’ s = ?a’) and (λs. b_’ s = ?b’) and
(λx. abs_var ?a id ?a’ ∧ abs_var ?b id ?b’) ∘
simple.lift_global_heap ∘
globals)
(L2_gets (λ_. simple.max’ ?a ?b) [’‘ret’’])
(Call max_'proc)

虽然autocorres不会知道max跟库中的max有啥关系，但是可以生成if ?a ≤ ?b then ?b else ?a这样的定理。

验证并非是重复代码逻辑
刚才我们看到加法还有最大值，已经都被autocorres轻松消解掉了，连定理和证明都可以自动生成了。
但是，实际上，形式化验证并没有这么简单。
我们看个求最大公约数的例子：

unsigned gcd(unsigned a, unsigned b)
{
unsigned c;
while (a != 0) {
c = a;
a = b % a;
b = c;
}
return b;
}

这个如何验证？

自动生成下：

thm simple.gcd’_def simple.gcd’_ac_corres
1
结果如下：

simple.gcd’ ?a ?b ≡
do (a, b) <- whileLoop (λ(a, b) b. a ≠ 0)
(λ(a, b). return (b mod a, a))
(?a, ?b);
return b
od
ac_corres (simple.lift_global_heap ∘ globals) True
simple_global_addresses.Γ (unat ∘ ret__unsigned_’)
((λs. a_’ s = ?a’) and (λs. b_’ s = ?b’) and
(λx. abs_var ?a unat ?a’ ∧ abs_var ?b unat ?b’) ∘
simple.lift_global_heap ∘
globals)
(liftE (simple.gcd’ ?a ?b)) (Call gcd_'proc)

这重复了下实现逻辑没错，但是没有体验中最大公约数的本质。

我们来看下seL4中的实现吧：

lemma gcd_to_return [simp]:
“gcd’ a b = return (gcd a b)”
apply (subst monad_to_gets [where v=“λ_. gcd a b”])
apply (wp gcd_wp)
apply simp
apply (clarsimp simp: gcd’_def)
apply (rule empty_fail_bind)
apply (rule empty_fail_whileLoop)
apply (clarsimp simp: split_def)
apply (clarsimp simp: split_def)
apply (clarsimp simp: split_def)
done

其中，monad_to_gets是一个辅助定理：

lemma monad_to_gets:
“⟦ ⋀P. ⦃ P ⦄ f ⦃ λr s. P s ∧ r = v s ⦄!; empty_fail f ⟧ ⟹ f = gets v”
apply atomize
apply (monad_eq simp: validNF_def valid_def no_fail_def empty_fail_def)
apply (rule conjI)
apply clarsimp
apply (drule_tac x=“λs’. s = s’” in spec)
apply clarsimp
apply force
apply clarsimp
apply (drule_tac x=“λs’. s’ = t” in spec)
apply clarsimp
apply force
done

求最弱前置条件gcd_wp为：

lemma gcd_wp [wp]:
“⦃ P (gcd a b) ⦄ gcd’ a b ⦃ P ⦄!”
(* Unfold definition of “gcd’”. *)
apply (unfold gcd’_def)

(* Annoate the loop with an invariant and measure. *)
apply (subst whileLoop_add_inv [where
I=“λ(a’, b’) s. gcd a b = gcd a’ b’ ∧ P (gcd a b) s”
and M=“λ((a’, b’), s). a’”])

(* Solve using weakest-precondition. *)
apply (wp; clarsimp)
apply (metis gcd.commute gcd_red_nat)
using gt_or_eq_0 by fastforce

这种水平的验证我们暂时还写不出来，大家只要有个概念就好，后面针对常见算法的验证方法我们用到再讲。

原文链接：https://blog.csdn.net/lusing/article/details/107943362?utm_medium=distribute.pc_feed.none-task-blog-personrec_tag-8.nonecase&depth_1-utm_source=distribute.pc_feed.none-task-blog-personrec_tag-8.nonecase&request_id=5f3387ec8c9fb674c6724168

操作系统形式化验证实践教程(7) - C代码的自动验证（转载）相关推荐

操作系统形式化验证实践教程(7) - C代码的自动验证
操作系统形式化验证实践教程(7) - C代码的自动验证上一节教程不知道大家看晕了没有,其实虽然细节很多还没有讲清楚,但是从结构上大家可以看到,其实是很模式化的工作. 那么能不能让这个模式化的工作自动 ...
操作系统形式化验证实践教程(10) - 一阶直觉逻辑
操作系统形式化验证实践教程(10) - 一阶直觉逻辑前面我们用了九讲的篇幅把seL4验证操作系统的地图给大家迅速过了一遍,基础好的同学已经可以基于前面的知识开始自己的工作了. 对于只学过离散数学,而 ...
操作系统形式化验证实践教程(11) - 结构化证明语言Isar（转载）
操作系统形式化验证实践教程(11) - 结构化证明语言Isar 结构化证明语言Isar基本语法 apply方法和by方法虽然可以完成功能,但是看起来更像是命令式语言.使用Isar语言,还可以写得更加形 ...
操作系统形式化验证实践教程(11) - 结构化证明语言Isar
操作系统形式化验证实践教程(11) - 结构化证明语言Isar 结构化证明语言Isar基本语法 apply方法和by方法虽然可以完成功能,但是看起来更像是命令式语言.使用Isar语言,还可以写得更加形 ...
网页图表Highcharts实践教程之图表代码构成
网页图表Highcharts实践教程之图表代码构成 Highcharts第一个实例下面我们来实现本书的第一个Highcharts实例. [实例1-1]下面来制作北京连续一周最高温度折线图.操作过程 ...
网页图表Highcharts实践教程之图表代码构成
网页图表Highcharts实践教程之图表代码构成 Highcharts第一个实例下面我们来实现本书的第一个Highcharts实例. [实例1-1]下面来制作北京连续一周最高温度折线图.操作过程如 ...
java jwt 验证_教程：用Java创建和验证JWT
java jwt 验证 "我喜欢编写身份验证和授权代码." 〜从来没有Java开发人员. 厌倦了一次又一次地建立相同的登录屏幕? 尝试使用Okta API进行托管身份验证,授权和多 ...
php 自动验证表单类,thinkPHP 表单自动验证功能
昨天晚上我们老大叫我弄表单自动验证功能,愁了半天借鉴了好多官网的知识,才出来,诶,总之分享一下我自己的成果吧! thinkphp 在Model基类为我们定义了自动验证的函数和正则表达式,我们只需要在对 ...
Playmaker全面实践教程之简单的使用Playmaker示例
Playmaker全面实践教程之简单的使用Playmaker示例简单的使用Playmaker示例通过本章前面部分的学习,相信读者已经对Playmaker有了一个整体的认识和印象了.在本章的最后,我 ...

操作系统形式化验证实践教程(7) - C代码的自动验证（转载）

操作系统形式化验证实践教程(7) - C代码的自动验证（转载）相关推荐

最新文章

热门文章