Program Verification 01 - Basic Logic
# 前置知识
在阅读本文档前,请先阅读程序验证的整体介绍文档,详见 Program Verification 知识板块中的 00 - Introduction 文档。
# 命题逻辑
命题变量 (proposition variables) 是取值可以为 真 (true) 或 假 (false) 的变量,而 命题逻辑 (propositional logic) 就是有关命题变量的逻辑规则。
# 命题运算符
下列术语中出现的运算符统称为 命题运算符 (propositional operators) 。
表示命题或命题变量, 或 表示真和假。
表示 和 的 合取 (conjunction) 或 逻辑与 (logic and) 。
表示 和 的 析取 (disjunction) 或 逻辑或 (logic or) 。
表示 蕴涵 (implication) 或 条件 (conditional) ,其中 是 前提 (antecedent) 或 假设 (hypothesis) , 是 结果 (consequent) 或 结论 (conclusion) 。
蕴涵 的等价表示包括:若 则 , 是 的充分条件, 是 的必要条件,等等。
。
表示 等价 (equivalance) 或 双向条件 (biconditional) 。
注意命题逻辑中的等价与数学中的等价不同,例如不具备传递性, 不能推导出 。
。
# 运算符属性
命题运算符按 优先级 (precedence) 从高到低依次为 。
- 有些地方认为 和 的优先级相同,因此将 写作 是更合适的。
命题运算符 和 具有结合律,并且规定它们是 左结合 (left associative) 的。
命题运算符 和 不满足结合律,并且规定它们是 右结合 (right associative) 的。
# 真值表
从数学的角度,可以把 蕴涵 视为 “小于等于” ,例如 即为 ,而 即为 。
# 语义等价和句法等价
# 基本概念
语义等价 (semantic equality) 是意义或结果上的等价,用 表示,例如 。
语义等价类似于我们在数学算术中使用的 等于 (equal) ,例如 在形式化验证的上下文中表示为 。
语义等价意味着 当且仅当 (if and only if) ,也经常写作 。
语义等价关系 和双向条件等价关系 有本质上的不同:
前者是语义上的符号,后者是句法上的符号。
前者具有传递性,后者不具有传递性。
句法等价 (syntactic equality) 是移除冗余括号后的结构化文本的等价,用 表示。语法等价与句法等价是本质不同的,例如 。
句法等价考虑如下三种冗余:
优先级,例如 。
结合性,例如 , 。
结合律,例如 。
句法等价不考虑交换律,例如 ,这是出于判定简便的考虑。如果考虑交换律,要判定诸如两个 个数相加的表达式是否句法等价将变得复杂,不考虑交换律使我们可以直接按文本顺序判定。
parenthesization 是为便于描述而引入的形式化概念:
minimal parenthesization 指的是在保证句法等价的前提下使括号尽可能少,例如 的 minimal parenthesization 为 。
full parenthesization 指的是在保证句法等价的前提下为每个二元表达式加上括号,例如 的 full parenthesization 为 。
对于具有结合律的左结合运算符,同样需要加上括号,例如 的 full parenthesization 为 。
是否在整个表达式周围加上括号是可选的,即 可以简写为 。
# 深入理解
通常情况下,我们更希望知道两个程序在语义上是否等价,然而在使用谓词时,判定语义等价可能是 impractical 的、甚至是不可能的。相比之下,句法等价要容易判定得多,我们可以使用句法等价来近似语义等价。
具体地讲,如果我们恰当地定义句法等价的判定规则,就可以保证句法等价蕴涵语义等价,即 。同样地,有逆否命题 成立,即语义不等价意味着句法不等价。
这种近似是很不精确的。一方面,语义等价的程序未必是句法等价的,例如 ;另一方面,句法不等价的程序经常是语义等价的,例如 。
现在我们考虑一个棘手的问题:如果命题(或表达式)同时涉及了两个优先级相同且都具有结合律的运算符,例如 和 ,以及 和 ,它们是否在句法上等价?
我们先考虑表达式 和 在语义上是否等价。显然,这取决于 的类型:如果是整数运算,则二者语义不等价;如果是高精度实数运算,则二者语义等价。
在这种情况下,如果确定表达式在句法上是否等价还需要考虑操作数的类型,将会使判定变得复杂,违背了我们进行近似的初衷,因此将其视为句法不等价是更合适的。
# 状态
# 基本概念
状态 (state) 是一系列命题变量与其真值的 绑定 (binding) ,记为 或 。若不含任何绑定,则称为空状态,记为 。
well-formed state :状态中出现的每个命题变量只有一个绑定,例如 。
ill-formed state :状态中有某个命题变量存在多个绑定,或存在非单变量的命题表达式,则为不正确的状态,例如 或 。
用 表示状态 中对变量 绑定的取值,例如对于 有 。
- 对于 为命题表达式的情况,可将 视为具有分配律的运算符进行拆解,例如 。
如果命题 在状态 下的演算结果为真,则称状态 满足 (satisfy) 命题 ,或命题 在状态 下被满足,记为 。
下面是几个命题满足的例子:
当我们表述状态对命题的满足性时,状态中可以有未被使用的绑定,但不能有缺失的绑定,哪怕已有的绑定已经足以对命题给出演算结果。例如,我们可以说 ,但我们不能说 。
- 如果状态 至少包含命题 中出现的所有命题变量的绑定,则称状态 适用于 (proper for) 命题 。
除非特殊说明,当我们在讨论命题和状态时,总是在讨论 well-formed 的状态 proper for 命题的情况,不考虑 ill-formed 的状态和 improper for 命题的情况。
# 基本性质
状态对命题的满足性具有分配律,例如:
对于任意的状态 和命题 ,若 ,则 。
# 命题分类
设 是一个命题,则:
若 ,则称 是 永真式 (tautology) 或 重言式 ,记为 。
若 ,则称 是 矛盾式 (contradiction) 。
若 ,即 ,则称 是 contingency 。
对于任意一个命题 ,其必为永真式、矛盾式或 contingency 三者之一。
可将语义等价 写成状态满足形式的永真式 。
# 谓词逻辑
# 基本概念
命题逻辑是对布尔表达式的真假断言,而 谓词逻辑 (predicate logic) 是对多个不同域的表达式取值的断言。可以认为,谓词逻辑是由命题逻辑扩展了域和量词的概念后形成的。
域 (domain) 表示一类取值的集合,例如整数域、实数域等。称定义在域上的变量为 域变量 (domain variables) 。
谓词 (predicate) 是描述取值的某些属性的逻辑断言。为了描述有关取值的属性,谓词逻辑在值域上追加了其它基本关系(例如小于等于)和规则(例如算术加减乘除)。
在谓词逻辑中,我们仍沿用在命题逻辑中使用的术语,例如 表示谓词, 或 表示真和假, 表示状态, 表示满足,等等。
在谓词逻辑中,状态中还可以有域变量的取值的绑定,例如 。
# 状态更新
设状态 中包含对变量 的绑定,用 表示将 中 所绑定的取值更新为 :
特别地,若 中没有对变量 的绑定,则 。
下面是两个状态取值更新的例子:
# 量词
我们用 量词 (quantifier) 来描述能使谓词为真的变量取值范围:是每个值,还是某个值?
设变量取值 , 是一个涉及变量 的谓词,则:
全称量词 (universal quantifier) 的形式是 ,例如 。
存在量词 (existential quantifier) 的形式是 ,例如 。
有界量词 (bounded quantifier) 是量词的另一种等价表示方式,其形式为 或 ,例如 。设 涉及 ,若我们希望量化 ,则有如下语义等价转换规则:
量化不同变量的量词在句法上是不同的,但在语义上是等价的,即:
量词 和 的优先级被视为最低,例如 语义等价于 。
量词有如下德摩根律:
- 01
- Reading Papers - Kernel Concurrency06-01
- 02
- Linux Kernel - Source Code Overview05-01
- 03
- Linux Kernel - Per-CPU Storage05-01