在先前介绍的swap函数中包含两个整数指针类型的形参px和py，它们在函数体中也可以被用作局部变量：
void swap(int * px, int * py)
{
}
那么就有以下几种方式可以用断言表述“地址px上存储的值是x”（其中x是一个逻辑变量）：
* px == x
store_int(px, x)
exists px_37, store_ptr(&px, px_37) * store_int(px_37, x)
尽管这三条断言表示同样的意思，但是我们推荐用户特别是QCP工具的初学者使用这三条断言中的最后一条。这三条断言中，只有最后一条可以被称为“QCP基本分离逻辑断言”。QCP基本分离逻辑断言要求以下形式的断言中，P1、P2等都是与内存无关的子句，并且P1、P2...Pn以及Q1、Q2...Qm（n与m都可以为0）中的表达式都是内存无关表达式：
(P1 && P2 && ... && Pn) && (Q1 * Q2 * ... * Qm)
QCP基本分离逻辑断言是将形如上面的命题用exists或||连接起来得到的命题（也可以没有exists或||）。
这一语法规定中，要求子句中的表达式中使用“内存无关表达式”是关键。这里，所谓“内存无关表达式”指的是计算相关表达式的值时，不涉及内存读取。在前面的例子中，px是一个程序变量，x是一个逻辑变量，因此px是内存相关表达式，而&px与x都是内存无关表达式，除此之外，px + 8与* px都是内存相关表达式，而x + 1与&px + 8这些都是内存无关表达式。
基本分离逻辑断言与内存读写的符号执行1
为什么我们推荐用户使用QCP基本分离逻辑断言呢？特别是为什么要在子句中使用内存无关表达式呢？主要是对于初学者来说，使用基本分离逻辑断言往往更容易写出正确的断言（特别是循环不变式），同时基于QCP基本分离逻辑断言也更容易理解QCP的符号执行过程。
下面考虑一个更复杂的性质：px与py相等，并且* px的值（同样也是* py的值）为零。这可以写作以下三种断言：
px == py && * px == 0
px == py && store_int(px, 0)
exists p, store_ptr(&px, p) * store_ptr(&py, p) * store_int(p, 0)
现在我们已经知道，这三条断言尽管表示同样的意思，但是其中只有第三条是基本分离逻辑断言。现在考虑考虑执行程序语句px = 0之后的结果。如果执行之前的程序状态满足上述性质，那么执行该语句后的程序状态所满足性质就可以用以下三条断言之一描述：
px == 0 && * py == 0
px == 0 && store_int(py, int, 0)
exists p, store_ptr(&px, 0) * store_ptr(&py, p) * store_int(p, 0)
可以看到，如果采取前两种断言，那么符号执行时除了需要将px == py改为px == 0之外，其他的子句（如* px == 0以及store_int(px, 0)）也会受到影响。然而，如果使用第三种断言，即基本分离逻辑断言，那么分离合取（即星号“*”）就保证了其他子句不会受到影响。
基本分离逻辑断言与内存读写的符号执行2
下面再考虑在前面三条断言后符号执行* py = 1的结果。
px == py && * px == 0之后符号执行* py = 1可能会得到px == py && * px == 1；px == py && store_int(px, 0)之后符号执行* py = 1可能会得到px == py && store_int(px, 1)；exists p, store_ptr(&px, p) * store_ptr(&py, p) * store_int(p, 0)之后符号执行* py = 1会得到exists p, store_ptr(&px, p) * store_ptr(&py, p) * store_int(p, 1)。
同样可以看到，在前两条断言的基础上进行符号执行，要正确找到应当修改的子句是不简单的。而在基本分离逻辑的基础上则很明确：要给* py写入新值，就先要得到py的值，也就是在&py地址上读取一个值，这个值是p（从子句store_ptr(&py, p)可以得到）；再修改地址p上的值，也就是要修改子句store_int(p, 1)。
在简单情况下使用简明分离逻辑断言
在一些简单的情况下，C程序可能不涉及的结构体等数据结构，也不涉及取地址操作或者指针的解引用。这时候，哪怕不使用QCP基本分离逻辑断言，也可以准确无歧义的描述程序状态所应当满足的性质。
以add函数为例（如下）
int add(int x, int y)
/*@ Require
0 <= x && x <= 100 &&
0 <= y && y <= 100
Ensure
__return == x + y
*/
{
int z = x + y;
return z;
}
进入函数体后，系统将为形参x与y分配内存空间，如果使用基本分离逻辑断言表述，那就是：
exists x_33 y_30,
0 <= x_33 && x_33 <= 100 && 0 <= y_30 && y_30 <= 100 &&
store_int(&x, x_33) * store_int(&y, y_30)
这段程序中不涉及指针操作，也不涉及结构体等复杂C语言数据结构，将上面这一条基本分离逻辑断言如下简化并不会带来歧义：
0 <= x && x <= 100 && 0 <= y && y <= 100
值得一提的是，尽管这一断言从字面上看与add函数的Require条件完全相同，但是现在x与y已经是分配有内存空间的C语言变量了，所以它作为函数体内部断言与它作为Require条件表示的意思有着细微的不同。
下一步，在声明变量z并对其初始化之后，符号执行得到的基本分离逻辑断言应当是：
exists x_33 y_30, 0 <= x_33 && x_33 <= 100 && 0 <= y_30 && y_30 <= 100 &&
store_int(&x, x_33) * store_int(&y, y_30) *
store_int(&z, x_33 + y_30)
这又可以简写成为：
0 <= x && x <= 100 && 0 <= y && y <= 100 && z == x + y
QCP既可以接受用户使用基本分离逻辑断言，也可以接受这样的“简明”分离逻辑断言并在工具内部将其转化为基本分离逻辑断言。我们推荐QCP的用户在大多数情况下还是尽量使用基本分离逻辑断言，当然，在相关C程序确实比较简单的情况下，使用简明分离逻辑也无妨。