毕设（二）形式化相关
涉及的形式化概念
1、函数式语言中的类型
在典型的函数式语言类型系统（以ML和Haskell为代表）中，除基本数据类型（整数、逻辑真值、浮点数等）和简单的复合数据类型（如数组、n元组和记录）外，还存在函数类型、归纳定义的数据类型（或称代数数据类型）等类型，以及参数化多态性、函子（functor）、单子（monad）等应用广泛的概念。
现代函数式语言：最早的函数式语言LISP，现代函数式语言有ML、Haskell、OCaml、Isabelle等，新的函数式语言有基于Java的Scala、F#
（1）Haskell中类型
基本数据类型（整数、逻辑真值、浮点数等）
简单的复合数据类型（如数组、n元组和记录）
函数类型
- 函数的声明：function_name :: argType1 -> argType2 -> ... ->argTypen ->resultType
- 注意，这里的参数用的是->，而你用的是x聚合，这很不一样。
归纳定义的数据类型（或称代数数据类型）
参数化多态性
函子（functor）
单子（monad）
（2）Haskell性质
haskell中，类型的推倒是右结合的，比如：a->a->a代表 a->(a->a)
参考：
https://blog.csdn.net/interhanchi/article/details/83160346
https://www.cnblogs.com/Will-zyq/p/10289352.html【初识Haskell】
https://www.haskell.org/【haskell官网】（首页的“Got 5 minutes?”很棒）
2、两种体系结构形式化验证方法：定理证明和模型检测【不全，缺“专门的程序证明工具”】
其实我们的SAML和SAMM更像是一个统一语言的定理证明，最大的共同点是公式推理。相当于PVS的改进版？？
| 方法 | 原理 | 现状 | 优点 | 缺点 |
|---|---|---|---|---|
| 定理证明 | 主要依靠公理和推理作为证明的手段。 | 定理证明，尤其是基于扩展规则的定理证明，已被应用到多个领域中[34]。 | 定理证明一定程度上可以实现自动验证 | 通常还需要经过一些手动工作才能够进行[35]。 |
| 模型检测 | 将对性质的满足与否问题转化为数学问题，并自动完成验证。 | 最常用的验证方法 | 自动完成验证 | 由于存在状态空间爆炸问题[39]，给模型检测的使用带来了困扰，关于这方面的研究已经取得了一定的进展与效果[40]。 |
（1）定理证明
| 验证工具 | 描述 | 优点 | 缺点 |
|---|---|---|---|
| PVS（Prototype Verification System，原型验证系统） | 包括规范语言及验证工具， 文献[37]进行了对通过定义自动机模型实现UML模型到PVS的转换研究 |
命令集丰富，与用户的交互友好 | 表达能力有待进一步提高[36] |
| Isabelle/HOL | 在通用辅助证明工具Isabelle中实现了HOL | 对大量数学逻辑做了形式化处理，方便验证 | 需要对待验证程序进行转化描述[38] |
（2）模型检测
| 验证工具 | 描述 | 优点 | 缺点 |
|---|---|---|---|
| SPIN[41]，SMV[42] | 已有广泛的应用， 例如文献[43]的模块化模型研究与文献[44]的测试用例研究中均使用了模型检测工具； |
- | 然而采用时态逻辑公式描述待验证性质存在易用性差等不足，使得常规模型检测使用有一定限制。 |
参考：
张论文
3、程序证明（定理证明？）
程序证明工具大致分为两类：证明辅助器（Proof Assistant）和专门的程序证明工具。
- 第一类，证明辅助器实际上是更为通用的定理证明工具，它不只是用来证明程序，而是起源于对数学定理的形式化证明。
- 典型代表是Isabelle/HOL[2]、Coq[3]、HOL[4]、PVS[5]
- 第二类，专门的程序证明工具，它们都提供一种函数式语言和一种描述程序正确性的规约语言，并通过求解器实现自动证明。这两个工具都是近几年刚刚出现的，代表了最新的研究成果。
- 典型的包括Why3[6] 和F*（F Star）[7]。
参考：
[2]isabelle/HOL, http://isabelle.in.tum.de/
[3]Coq, https://coq.inria.fr/
[4]HOL, https://hol-theorem-prover.org/
[5]PVS, https://pvs.csl.sri.com/
[6]Why3, http://why3.lri.fr/
[7]F*, https://fstar-lang.org/
4、程序证明工具 vs 定理证明器
根据定理证明器的逻辑可以分为：高阶逻辑定理证明器、一阶逻辑定理证明器、模态逻辑定理证明器、逻辑框架式定理证明器。
根据自动化程度可将定理证明器主要分为：交互式定理证明器（也成为证明辅助器）和自动化定理证明器。
- 交互式定理证明器：Isabelle、Coq、HOL常用。
- 自动化定理证明器：E、SPASS、Vampire等。自动化定理证明器一般限于带等式的一阶逻辑。
对比结论：
| 证明器类型 | 特点+应用场景 | 缺点 |
|---|---|---|
| 完全自动的定理证明器 | 一般没有类型理论，不能用于验证大的系统； | |
| 交互式定理证明器 | 有复杂的类型理论，支持复杂的定义和规范，如类型、函数和关系的递归定义。 | 只是证明过程需要人工交互，每一个证明步骤所采用的公理或推理规则，都是由用户来指定的，计算机只是完成具体的推理工作，因此对用户的要求非常高，自动化程度比较低。 |
为了充分利用两种证明器的优点，通常情况下交互式定理证明器都会引入自动化证明的工具，从而减少交互次数，提高交互式定理证明的自动化程度，增加系统的证明能力。
10、赵永望老师的程序证明方法
HACMS项目采用了全新的系统开发方法，即本书所述的程序证明的方法，旨在开发一套开源的、高安全确保的操作系统和控制系统组件，以构建高安全网络化军用飞机平台，能够防止黑客攻击，最终以四轴垂直起降无人机做验证平台。
HACMS项目通过程序证明等方法构造了安全的软硬件系统，并基于此开发出一个黑客无法入侵的无人机控制软件。
下表是形式化的发展史：
参考：
https://www.yuque.com/zhaoyongwang/fpp/xgpzo6【赵永望书-程序证明】