2022Fall_FormalMethod Review

  • 课程主页: 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


例子:

决策过程优化方法:

  • 纯变量

  • 内存分区

    例子:

理论结合

  • 例子

    不同理论分开求解


C++的调试技巧

在开发C++程序的过程中，当遇到需要调试程序的场景，优秀的调试器例如GDB等可以使调试的过程变得更有效率，使程序的运行更加透明，但总有不能使用调试器的场景例如嵌入式开发不存在显示屏等情况，这时可以利用一些调试技巧对程序进行调试

调试标记

当进行程序开发时，可能会在源程序中添加一些调试的代码方便测试，但是后来程序完成的时候需要找到这些代码一一进行删除，在程序运行的过程中可能有会发现需要这些代码。这些麻烦可以利用调试标记解决。

通过预处理器调试标记

可以利用预处理器标记来分离出用于调试的代码和确保程序正常工作的代码，通过预处理器定义#define FOOBAR(一般用DEBUG，但不能用NDEBUG)和ifdef ifndef 等预处理语句可以实现这个目的，当认为调试完成了，可以利用undef来表示调试已经完成，例如如下的代码片段。

#define DEBUG 
#undef DEBUG
//***
#ifdef DEBUG
//***
#endif

运行期调试标记

某些情况下，运行期打开调试标记会更加方便（例如每次定义预处理标记都会导致程序的重新编译），为了实现打开或关闭调试，可以定义一个bool型数据变量

//****
bool debug = false;

int main(int argc, char* argv[]){
    if(string(argv[i])== "--debug=on") debug = true;
//****
}

将变量和表达式表示为字符串

若在编写程序的时候可以将字符串和变量名与其内容一一用输出打印函数组成打印表达式，但这样的话工作量非常的大，可以通过宏定义和字符串化运算符 # 来将变量转化为一个字符数组。在预处理语句中的参数前使用#来标记就可以实现这个功能：

#define PR(x) cout << #x << " = " << endl;

它与如下语句具有同样的效果：

cout << "a = " << a  << endl;

在实际使用的时候也可以使用ifdef来使得P(A) 不起作用

C语言assert()宏

头文件<cassert>中，有assert()方便的调试宏。当使用assert时，参数为一个表示为真的表达式，预处理器产生测试断言的代码，若测试结果不为真，则发生一个错误信息，返回错误信息并终止程序运行。

#include <cassert>
using namespace std;

int main(){
    int i=100;
    assert(i!=100);//fails
}

在完成调试后，可以通过编译器参数命令行或者在#include<cassert> 前定义 #define NDEBUG 来消除宏产生的测试代码。