项目文档 - HackMD

# 项目文档 [返回主页面](https://hackmd.io/@LVcpSNoxQAim3tB5Xaj-gg/H1IpnzxAU) ### 概述此软件是一款用于 形式符号验证的 （Formal Verification Language）设计语言。下文将此项目简称为 **形式验证语言**。 ### 目的本项目的目的在于提出一种形式验证语言的规范和标准。这套标准需要具有可读性、可执行性和易写性。项目在开发过程中要采取世界上现有的优秀编程语言的书写习惯，并再此基础上进行完善和具有针对性的开发。 ### 关键定义我们设计的形式验证语言包含如下定义。 #### 量词一个量词是一个用于引进新变量的符号。在形式验证语言中，所有的变量都必须通过量词引进。量词在使用时，必须声明要引入的变量的变量类型以及字句 ``` 量词的使用必备三要素：声明量词，声明变量类型，声明子句 ``` 注意，我们并没有声明变量名，原因是在形式验证中，变量名均是可以进行整体替换的。变量名只是为了人类区分不同变量，其名称并不影响形式验证。 #### 变量类型在量词引入变量时，必须声明变量类型。变量类型是**一个具有一个自由参数的逻辑表达式p(x)**。一个变量$y$ 具有类型$p$ 当且仅当我们可以从现有命题形式的推导出 $p(y)$ 成立。有两种变量类型值得注意：True 类型，即任何变量都是此类型的。False 类型：任何变量都不是此类型。 **注意**：我们规定只能验证一个变量是否具有该类型，但不能直接读取变量的类型。毕竟，读取变量类型是无意义的。(如typeof 这种函数我们不会开发) #### 子句一个量词必须具有子句来完成一个包含量词的语句块。由于这一部分过于抽象，我们举个具体例子。在如下的数学表达式中 $$ \sum_{x\in\mathbb Z} \frac1x $$ 在如下表达式中 $\sum$ 是量词，$x\in\mathbb Z$ 是一个具有自由变量$x$ 的逻辑表达式，用于声明变量类型，而$\frac1x$是子句。例子：下面的表达式 $$ z=\sum_{x\in A} \left(x+\sum_{y\in B}f(x,y)\right) $$ 形式验证语言 ``` z=sum x. x in A: x+sum y. y in B: f(x,y) ``` 例子：集合的定义 $$ \text{Let }A=\{x\in\mathbb Z: x^2=1\} $$ ``` Let A. x in A iff x^2=1 and x is integer: [缩进]子句(需要用A做的事情) ``` 这里，A的变量类型本身就是A的定义 ## 二元运算符并列句 #### claim 关键字当一个二元运算符并列句开始时，以 claim 作为起始声明，然后以缩进去书写每个子块和子块的内部运算推倒 ## 子程序 #### Lemma 子程序在书写证明中，一个只需要验证其内部来验证子块成立的表达式。类似子程序的概念。 ``` lemma Lemma名称: 推理表达式 ``` 子程序的调用： ``` by Lemma 名称, 推理 ``` #### 一元运算符(函数符号) 一个一元运算符，是一个符号$f$，这个符号可以与紧贴其后的一个括号的内容作为一个整体，当成一个新的变量或表达式。比如 $f(x,y)$, $f(x,y,z)$。注意，虽然这些函数分别是二元和三元函数，但是我们仍然在符号上将它理解成一元运算符。要让任何一个一元运算符听起来有道理，都必须声明它的输入和输出变量类型。 - 任何变量都是一个一元运算符(这个规定会不会引起麻烦？) #### 二元运算符一个二元运算符，是一个符号比如$*$，这个符号可以将其两侧的变量作为输入，并且输出一个新的变量或表达式。比如 $x+y$, $x*y$。要让一个二元运算符听起来有道理，我们也必须规定它的输入类型和输出类型。注意，二元运算符可以不必加括号。而且二元运算符不能独立存在，它必须左右有可以另其运算的输入的符号。 #### 二元运算符--优先级在处理二元运算符时，必须决定先后顺序。优先级高的二元运算符先得到执行。优先级低的二元运算符放在最后执行。 ### 现有设计 ## 设计1：Python 类型缩进式语言 [用缩进式语言书写证明的例子](/d5PIkec0S1m6lDs52AWrUQ) **量词语句设计**： ``` 量词 [空格] 变量名 .[点] 变量类型(以此变量名为自由变量的逻辑表达式): [缩进] 子句 ```` **一元运算符语句设计** ``` f(x,y,z,...) ``` **二元运算符语句设计** ``` [符号语句块] 二元运算符 [符号语句块] ``` 注意到二元运算符的优先级法则可以自动区分其需要运行的语句块 **Lemma 子句设计** ``` lemma 命题: [缩进]命题的证明 ``` ## 潜在问题 #### 高阶逻辑比如 ``` Let A. x in A iff x^2=1 and x is integer: [缩进]子句 ``` 这里，要验证 A is a set 需要用到二阶逻辑。即 $$ A \text{ is a set}\iff (x\in A\iff p(x)) \text{ for some }p $$ 注意二阶逻辑的意思是 for some 后面可以加入一阶逻辑的命题。注意，这本身也是无法回避的问题，is a set 确实是二阶逻辑的表达式。因为，我们不能考虑类似$\{A:A\text{ is a set }\}$的集合。因此我们在设计中必须考虑逻辑的阶