- 课程主页: Formal Methods Foundation (csslab-ustc.github.io)
- 课程逻辑
- 课程大纲
- 考试内容: 开卷
- 命题逻辑(证明树推导, 规则使用)
- 构造逻辑(与命题逻辑区别)
- SAT(是命题逻辑部分的可满足性问题)
- Theory(谓词逻辑满足性定理)
- 符号执行/混合执行
_数学基础
计算复杂性理论
上下文无关文法
具体例子:
- 上述推导 _存在二义性:
结构化归纳法
例子:
命题逻辑
证明系统: 自然演绎(经典命题逻辑)
基本概念
环境: 一组命题 假定是真的
断言:
( |- 的意思是 等价 )
证明规则
合取(Conjunction理解为And)
析取(Disjunction理解为Or)
蕴含
否定
证明–历年考题(证明规则的运用)
推导的循序是自下往上
历史考题1
考试题型: 证明题
构造逻辑
- 不能使用反证法
SAT(布尔可满足性)问题/DPLL算法
SAT是针对命题逻辑的可满足性问题
例:
穷举法
但时间增长速度快(指数级)
提出了DPLL
DPLL算法的输入必须是合取范式CNF
CNF(合取范式)
合取范式中:
- 最外层的符号都是合取
- 否定符号一定出现在原子命题前
- 不能有蕴含(->)符号
转换命题为CNF范式:
增加了优先级
例子:
可能会考到
_解析和传播
不做过多解释
CNF不可解–解析推出矛盾
CNF解析不冲突–传播
DPLL
- bcp(P)
单元解析: 两个子句之间必须有一个是原子命题
bcp通俗来说: 两个命题中有一个是原子命题(p), 另一个是含有p析取(~/否定)的复合命题, 传播得出等价的不含原子命题的新命题(q)
例子
上面的过程完成了一次布尔约束传播(bcp)_选择变量(递归地)
SAT vs. valid
SAT基于的是命题逻辑(不接受排中律, 可以用反证法)
谓词逻辑
谓词逻辑是命题逻辑的细化
- 增加了原子逻辑上更细化的定义
- 引入了一些量词(全称, 存在)
新增(相对命题逻辑)的概念:
x是自由变量, y是绑定变量, 替换操作只能针对自由变量. α重命名不能让变量名冲突
计算绑定变量
输入: 谓词逻辑命题
输出: 绑定变量集合
例子:
计算自由变量
例子:
一个变量有可能同时是绑定变量和自由变量(例子中的y)
替换规则
输入: 命题
输出: 命题
只替换自由变量, 替换前要求解绑定/自由变量, 自由变量替换前要进行α重命名
例子:
证明系统: 自然演绎
原先的命题逻辑规则和推导方法证明系统: 自然演绎(经典命题逻辑) 在这里也适用, 这里只列出了新增的四条规则
- 全称量词的引入
- 存在量词的引入
- 全称量词的消去
- 存在量词的消去
例题:
SMT可满足性模理论
求解谓词逻辑可满足性求解
理论是谓词逻辑语法的子集
等式理论/EUF理论
- 未解释函数定义
- EUF(等式与未解释函数定义)
- 全等定理
用于证明函数之间等价
例子1: 证明两个程序等价
改写为静态单赋值(SSA)形式
把乘法(*)抽象为抽象函数
例子2: 编译
线性算数(LA)理论
消元法
做题中
- 右边改成0
- 符号改成一样
例子 : (考试要考消元法)
往上代入, 有一组解
说明这一组约束是可满足的
_单纯形法
不考
…
_分支定界
不考
…
比特向量理论
语法
语义
把bit向量映射到正数域:
- 有符号
- 无符号
bitBlast()比特爆炸
递归生成树:genCons()生成限制
数组理论
数组读写的消去
例子:
分类讨论: z<i / z=i / z>i
指针理论: 内存模型
地址T 值类型E 关系R 复合命题P
例子:
决策过程优化方法:
纯变量
内存分区
例子:
理论结合
- 例子
不同理论分开求解