操作系统形式化验证实践教程(11) - 结构化证明语言Isar
操作系统形式化验证实践教程(11) - 结构化证明语言Isar
结构化证明语言Isar基本语法
apply方法和by方法虽然可以完成功能,但是看起来更像是命令式语言。使用Isar语言,还可以写得更加形式化一点。
Isar的格式看起来像这样:
proofassume "公式1"from “公式1" have "公式2" by 方法...from "公式n" show "结论" by 方法
qed
虽然换了种写法,但是其实核心内容并没有变。
直接proof指定方法
最简单的写法,就是把by的内容放到proof语句之后,然后就直接qed了。
我们看7个例子:
lemma A1: "A ⟹ (B⟹A)"
proof(erule thin_rl,Pure.assumption)
qedlemma A2 : "(A ⟹ (B⟹C)) ⟹ ((A⟹B) ⟹ (A⟹C))"
proof(erule meta_impE,assumption,assumption)
qedlemma A3: "(A∧B) ⟹ A"
proof(erule conjunct1)
qedlemma A4: "(A∧B) ⟹ B"
proof(erule conjunct2)
qedlemma A5: "A ⟹ (B ⟹ (A∧B))"
proof(erule conjI,assumption)
qedlemma A6: "A ⟹ (A ∨ B)"
proof(erule disjI1)
qedlemma A7: "B ⟹ (A ∨ B)"
proof(erule disjI2)
qed
assume have show
下面我们尝试用assume…have…show的方法改写一下。proof语句的参数我们给个"-",表示空值:
lemma "(A ⟹ (B⟹C)) ⟹ ((A⟹B) ⟹ (A⟹C))"
proof -assume Fact0: "(A ⟹ (B⟹C))"from Fact0 show "((A⟹B) ⟹ (A⟹C))" by (rule meta_impE)
qed
this
上一节我们在assume和show中使用了标签,但是Isar认为使用标签是不好的,容易给词法分析造成困扰。
如果使用上一条中的公式,我们就直接使用this来指代,上一节的例子就变成这样:
lemma "(A ⟹ (B⟹C)) ⟹ ((A⟹B) ⟹ (A⟹C))"
proof -assume "(A ⟹ (B⟹C))"from this show "((A⟹B) ⟹ (A⟹C))" by (rule meta_impE)
qed
then
尽可能使用this之后,我们发现from this用的很广泛,于是我们可以给from this起一个别名叫then。于是上节的例子可以写成下面这样:
lemma "(A ⟹ (B⟹C)) ⟹ ((A⟹B) ⟹ (A⟹C))"
proof -assume "(A ⟹ (B⟹C))"then show "((A⟹B) ⟹ (A⟹C))" by (rule meta_impE)
qed
thus和hence
换成then之后,我们发现from this终于被隐藏起来了。但是,大量的then have和then show又出来了。于是我们可以再简化一下,给then have起个别名hence,给then show起个别名thus。
于是上节的例子可以写成这样:
lemma "(A ⟹ (B⟹C)) ⟹ ((A⟹B) ⟹ (A⟹C))"
proof -assume "(A ⟹ (B⟹C))"thus "((A⟹B) ⟹ (A⟹C))" by (rule meta_impE)
qed
假设拆分
当lemma比较长时,可以将其拆分成几个独立的假设,然后在proof中使用。
我们来看个例子:
lemma impE_2:assumes 1:‹P⟶Q›and 2: ‹Q⟹R›and 3: ‹P⟶Q ⟹ P›shows ‹R›
proof -from 3 and 1 have ‹P› by simpwith 1 have ‹Q› by (rule impE)with 2 show ‹R› by simp
qed
这里我们又使用了一个新的缩写with,with xxx等于from xxx this,是from的一个语法糖。
其中的"‹",写作<open>。同样“›”写作<close>. 也可以通过"来输入,然后IDE中会提示。
我们来看ASCII源码:
lemma impE_2:assumes 1:\<open>P\<longrightarrow>Q\<close>and 2: \<open>Q\<Longrightarrow>R\<close>and 3: \<open>P\<longrightarrow>Q \<Longrightarrow> P\<close>shows \<open>R\<close>
proof -from 3 and 1 have \<open>P\<close> by simpwith 1 have \<open>Q\<close> by (rule impE)with 2 show \<open>R\<close> by simp
qed
对了,针对这样分立条件的,不使用Isar的情况下该如何写呢?我们可以使用using来使用假设们然后再用by来引用证明方法,来看个例子:
lemma impE_3:assumes 1:‹P⟶Q›and 2: ‹Q⟹R›and 3: ‹P⟶Q ⟹ P›
shows ‹R›using "1" "2" "3" by blast
巩固下,再来个例子:
lemma notE_2:assumes 1: ‹¬P›
and 2:‹¬P ⟹ P›
shows ‹R›using "1" "2" by auto
小结
Isar语言的出现,是希望能够能通过一些语法糖,让证明看起来更像是用自然语言书写,提升可读性。
但是其基本原理跟没有Isar语言框架是一致的。数理逻辑知识目前仍然是主要要攻克的点,而非语言和框架。
操作系统形式化验证实践教程(11) - 结构化证明语言Isar相关推荐
- 操作系统形式化验证实践教程(11) - 结构化证明语言Isar(转载)
操作系统形式化验证实践教程(11) - 结构化证明语言Isar 结构化证明语言Isar基本语法 apply方法和by方法虽然可以完成功能,但是看起来更像是命令式语言.使用Isar语言,还可以写得更加形 ...
- 操作系统形式化验证实践教程(10) - 一阶直觉逻辑
操作系统形式化验证实践教程(10) - 一阶直觉逻辑 前面我们用了九讲的篇幅把seL4验证操作系统的地图给大家迅速过了一遍,基础好的同学已经可以基于前面的知识开始自己的工作了. 对于只学过离散数学,而 ...
- 操作系统形式化验证实践教程(7) - C代码的自动验证
操作系统形式化验证实践教程(7) - C代码的自动验证 上一节教程不知道大家看晕了没有,其实虽然细节很多还没有讲清楚,但是从结构上大家可以看到,其实是很模式化的工作. 那么能不能让这个模式化的工作自动 ...
- 操作系统形式化验证实践教程(7) - C代码的自动验证(转载)
操作系统形式化验证实践教程(7) - C代码的自动验证 上一节教程不知道大家看晕了没有,其实虽然细节很多还没有讲清楚,但是从结构上大家可以看到,其实是很模式化的工作. 那么能不能让这个模式化的工作自动 ...
- linux内核形式化验证,聪明人的笨功夫 -- MesaTEE安全形式化验证实践
各类TEE(例如TPM和Intel SGX)提供了强大的可信计算硬件基础,但他们并不直接保证软件的安全性.诸如缓冲区溢出等内存安全问题为攻击者提供了侵入TEE的可乘之机.因此,软件内存安全保护极其重要 ...
- 数据科学 IPython 笔记本 9.11 结构化数据:NumPy 的结构化数组
9.11 结构化数据:NumPy 的结构化数组 本节是<Python 数据科学手册>(Python Data Science Handbook)的摘录. 译者:飞龙 协议:CC BY-NC ...
- Rockwell 罗克韦尔AB Logix 5000控制器 结构化文本语言(ST) 梯形图(LD)顺序功能图(SFC)功能块图(FBD) IEC 61131-3 手册
Logix 5000 Controllers IEC 61131-3 Compliance 1756 ControlLogix, 1756 GuardLogix, 1769 CompactLogix, ...
- st计算机编程语言,ST(结构化文本语言(ST))_百度百科
ST (结构化文本语言(ST)) 语音 编辑 锁定 讨论 上传视频 本词条缺少概述图,补充相关内容使词条更完整,还能快速升级,赶紧来编辑吧! 结构化文本/结构式文件编程语言(英语:Structured ...
- 1-1 结构化数据建模流程范例
一.准备数据 titanic数据集(下载链接:https://www.kaggle.com/c/titanic/data)的目标是根据乘客信息预测他们在Titanic号撞击冰山沉没后能否生存. 结构化 ...
最新文章
- vs如何设置对话框显示在最前面_【另存为】对话框的使用
- 想学科大讯飞成为下一个业界黑马?这些项目了解一下
- mybatis 一二事(1) - 简单介绍
- 在linux下python爬虫进程发生异常时自动重启直至正常结束的方法
- Kooboo CMS - Html.FrontHtml.Position 详解
- 【整理】SAP货币汇率转换
- mysql 数据复制停止工作_linux – Mysql GTID复制停止工作
- 六、区块链主流共识算法浅析
- PSD分层电商促销模板|换季大促销,不怕老板催你做海报了
- python - 列表
- iOS:NAV+TABLE结合
- python在数字后添加字符_用python生成数字、字母和特殊字符混合的字符串
- 数据建模讲解和案例分析
- 场景法测试用例设计详解
- linux gt240驱动下载,NVIDIA官方发布Linux 256.53正式版驱动
- 天池大数据竞赛平台-东电网智慧现场作业挑战赛:识别高空作业及安全带佩戴Baseline(非官方)
- 树莓派+L9110S电机模块
- Vue实现一个长方形少一个三角形的样式(类似两个直角梯形摞在一起的样式)
- 掌握最新网管技术 做悠闲网管员
- The request was rejected because the URL contained a potentially malicious String “%2e“