Part 1
规约标注入门
从函数前后条件、循环不变量和 IDE 调试反馈入手。
Tutorials
使用教程
教程页面由原始 markdown 文档生成，延续 QCP 首页与 About 页的学术排版风格， 覆盖规约标注、内存断言与符号执行三组内容。
Part 2
内存与断言
梳理 store、has_permission 与分离合取的常见写法。
Part 3
符号执行
结合控制流、报错告警与断言标注理解 QCP 的执行过程。
规约标注入门
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
条件分支语句与控制流相关的符号执行
以下三个C函数都是取绝对值的潜在实现方法。这里我们仅仅举例说明验证它们的一个简单性质：如果调用它们时的参数不为INT_MIN，那么它们就能安全运行，并且其返回值非负。
阅读教程T3-4
符号执行遇到断言标注的情况
QCP工具允许用户在程序语句间添加断言标注辅助验证的完成。前面曾经提到的循环不变量就是一种这样的断言标注。当QCP符号执行器遇到断言标注时，就会检查先前由符号执行得到的最强后条件是否可以推出用户手动输入的断言。以前面曾经介绍过的swap函数为例。
阅读教程