Part 1
规约标注入门
从函数前后条件、循环不变量和 IDE 调试反馈入手。
Tutorials
使用教程
教程页面由原始 markdown 文档生成，延续 QCP 首页与 About 页的学术排版风格， 覆盖规约标注、内存断言、符号执行与断言扩展四组内容。
Part 2
内存与断言
梳理 store、has_permission 与分离合取的常见写法。
Part 3
符号执行
结合验证条件、控制流、断言标注与循环理解 QCP 的执行过程。
Part 4
断言扩展与自动变换
介绍数学函数谓词、自定义分离逻辑谓词与自动断言变换。
规约标注入门
T1-1
描述C函数安全性的规约标注
在验证一个C函数时，我们需要在这个C函数的开头以标注的形式说明该函数的规约，即它的安全性或功能正确性描述。一个C函数的规约包括一个逻辑参数列表（With）和该函数对应的分离逻辑的前后条件（Require、Ensure）。在一些简单的情况中，规约可以不包含With列表。
阅读教程T1-2
用断言标注辅助验证
如果程序比较简单，并且待验证的性质也比较简单，那么QCP往往就可以自动完成验证。T1-1中列举的add等例子都属于这一类。然而，当程序复杂一些，哪怕只是包含循环结构时，QCP就无法自动完成验证。用户可以使用断言标注辅助QCP完成验证。在所有断言标注中，最主要的就是循环不变量标注。
阅读教程T1-3
查看符号执行结果与调试纠错的方法
在开发程序与验证程序的过程中，人们通常很难一次就将程序写对，有时也很难一次就通过标注完成验证。QCP提供了配套的VSCode插件与网页版IDE支持，供用户实时看到验证的中间结果。
阅读教程内存与断言
T2-1
内存操作有关的规约标注
C语言程序的一大特点是它可以直接通过内存地址对内存进行读写。例如，下面C程序交换了两个地址上的值。
阅读教程T2-2
断言常见形式和分离合取的常用性质
从前面的例子中已经可以看到，QCP的断言语言中可以使用逻辑连接词&&与*，前者表示通常意义上的“且”，而后者是分离合取，具体而言，“P * Q”表示当前内存可以分为互不相交的两部分，其中一部分满足P另一部分满足Q。我们可以用这些逻辑连接词将多个子句连接起来，从而表述一些复杂的概念。
阅读教程T2-3
全局有关的规约标注
如果C程序中a与b是两个有符号整数类型的全局变量，那么下面三种swap_ab函数都可以实现交换它们数值的效果。
阅读教程T2-4
结构体操作有关的规约标注
如果C程序中定义以下结构体struct int_pair，那么很自然就可以用先前定义的swap函数交换它两个域的值。
阅读教程符号执行
T3-1
简单符号执行
前面已经介绍过，符号执行就是根据先前的断言计算程序语句执行之后的断言。符号执行是QCP工具的核心模块之一。下面通过swap函数介绍QCP中各种程序语句的符号执行结果。以下是之前介绍过的swap函数及其规约。QCP工具可以自动检查并确认swap函数确实实现了该规约描述的功能。
阅读教程T3-2
基本分离逻辑断言
在先前介绍的swap函数中包含两个整数指针类型的形参px和py，它们在函数体中也可以被用作局部变量：
阅读教程T3-3
符号执行生成验证条件
QCP工具在符号执行的过程中会生成验证条件（verification condition，VC）。所有验证条件都是断言之间的推导（|--左边的断言推出|--右边的断言，形如P |-- Q），实质上，符号执行就是将程序的安全性和功能正确性检查归结为检查这些断言推导是否成立。这里先介绍两类先前关于符号执行的章节中已经遇到过的典型验证条件，之后的章节还会介绍其他生成验证条件的情况。
阅读教程T3-4
条件分支语句与控制流相关的符号执行
以下三个C函数都是取绝对值的潜在实现方法。这里我们仅仅举例说明验证它们的一个简单性质：如果调用它们时的参数不为INT_MIN，那么它们就能安全运行，并且其返回值非负。
阅读教程T3-5
符号执行遇到断言标注的情况
QCP工具允许用户在程序语句间添加断言标注辅助验证的完成。前面曾经提到的循环不变量就是一种这样的断言标注。当QCP符号执行器遇到断言标注时，就会检查先前由符号执行得到的最强后条件是否可以推出用户手动输入的断言。
阅读教程T3-6
循环语句的符号执行
前面已经介绍，赋值语句、if语句以及控制流语句如break/continue/return等的符号执行都与实际程序执行的流程大致相似。但是循环语句的符号执行并不会反复符号执行循环体直至跳出循环。
阅读教程断言扩展与自动变换
T4-1
在规约或断言中使用数学函数和谓词
当程序及其实现的功能较为复杂的时候，可能用简单的算数运算无法准确表述程序的预期功能或者关键断言。此时就需要使用额外的数学概念（包括谓词和函数）来更清晰地表达程序的意图和逻辑。这些数学概念可以帮助开发者和读者更好地理解代码的目的和行为。当然，使用这些数学概念往往意味着验证无法由QCP的符号执行器和求解器全自动完成，此时就需要用户在定理证明器Rocq中手动完成一些证明。
阅读教程T4-2
在规约或断言中使用新定义的分离逻辑谓词
有时，将一个数据结构占据的全部内存看作一个证明可以方便我们完成验证。例如，C语言中可以用这样的一个struct表示两个整数的有序对。
阅读教程T4-3
符号执行中自动的按需断言变换
前面我们介绍了在处理struct int_pair这样的结构体时，可以定义一个分离逻辑谓词store_int_pair，将这个结构体占据的内存权限看作一个整体。
阅读教程T4-4
符号执行中的其他自动断言变换
前面我们提到，在验证struct int_pair这一结构体操作时，我们可以让QCP符号执行器按需展开store_int_pair谓词。
阅读教程