---
# System prepended metadata

title: 项目文档

---

# 项目文档

[返回主页面](https://hackmd.io/@LVcpSNoxQAim3tB5Xaj-gg/H1IpnzxAU)

### 概述

此软件是一款用于 <span style="color:red">形式符号验证的</span> （Formal Verification Language）设计语言。下文将此项目简称为 **形式验证语言**。

### 目的
本项目的目的在于提出一种形式验证语言的规范和标准。这套标准需要具有可读性、可执行性和易写性。项目在开发过程中要采取世界上现有的优秀编程语言的书写习惯，并再此基础上进行完善和具有针对性的开发。

### 关键定义

我们设计的形式验证语言包含如下定义。

#### 量词

一个量词是一个用于<span style="color:red">引进新变量</span>的符号。在形式验证语言中，所有的变量都必须通过量词引进。量词在使用时，必须声明要引入的变量的变量类型以及字句

```
量词的使用必备三要素：声明量词，声明变量类型，声明子句
```

注意，我们并没有声明变量名，原因是在形式验证中，变量名均是可以进行整体替换的。变量名只是为了人类区分不同变量，其名称并不影响形式验证。
#### 变量类型

在量词引入变量时，必须声明变量类型。变量类型是**一个具有一个自由参数的逻辑表达式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)$。注意，虽然这些函数分别是二元和三元函数，但是我们仍然在符号上将它理解成一元运算符。

要让任何一个一元运算符听起来有道理，都必须声明它的输入和输出变量类型。

- 任何变量都是一个一元运算符(<span style="color:red">这个规定会不会引起麻烦？</span>)

#### 二元运算符

一个二元运算符，是一个符号比如$*$， 这个符号可以将其两侧的变量作为输入，并且输出一个新的变量或表达式。比如 $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 }\}$的集合。

因此我们在设计中必须考虑逻辑的阶

