程序的一个状态简单地说就是程序变量的一组赋值。我们说过:赋值 a a a(一个状态)满足公式 φ \varphi φ可以记为 M a ( φ ) = TRUE M_a(\varphi) = \text{TRUE} Ma(φ)=TRUE(这里未提及结构 S S S,假设 S S S可由上下文获得),或者记为 a ⊨ S φ a \models_S \varphi a⊨Sφ。程序的执行是一个有限或无限的状态序列,其中第一个状态满足初始条件,其余每个后继状态 b b b都由其前驱状态 a a a按如下方式获得:
- 若 a a a是谓词为 p p p的判定节点入边上的状态, b b b是该节点标记为true的出边上的状态,且 a ⊨ S p a \models_S p a⊨Sp成立,则 b b b与 a a a相同。
- 若 a a a是谓词为 p p p的判定节点入边上的状态, b b b是该节点标记为false的出边上的状态,且 a ⊨ S ¬ p a \models_S \neg p a⊨S¬p成立,则 b b b与 a a a相同。
- 若 a a a是赋值 v : = e v := e v:=e前的状态, b b b是紧跟该赋值后的状态,则 b b b为 a [ T a [ e ] / v ] a[T_a[e]/v] a[Ta[e]/v]。 T a [ e ] T_a[e] Ta[e]是表达式 e e e根据状态 a a a计算而得的值, a [ d / v ] a[d/v] a[d/v]是除了 v v v值被设为 d d d外其余都与 a a a相同的一个赋值。因此,赋值之后的状态 b b b除了 v v v的值以外其余都与 a a a相同,而 v v v的值是表达式 e e e根据之前的状态 a a a计算而得的值。
下面来解释这段文字中的一些概念,更好地理解它的意思。
1. 状态(State)
在程序执行过程中,状态是程序变量的一组赋值。例如,如果有两个变量 x x x和 y y y,一个可能的状态是 x = 1 x=1 x=1, y = 2 y=2 y=2。
2. 公式(Formula)
公式是一个逻辑表达式,可以用来描述某个状态是否满足某种条件。例如,公式 φ \varphi φ可以是 x > 0 x > 0 x>0。如果状态 a a a中的 x x x为1,那么我们可以说 a a a满足公式 φ \varphi φ。
3. 状态序列(State Sequence)
程序的执行可以看作是从一个状态到另一个状态的变化过程。这个过程可以用一个状态序列来表示。初始状态满足初始条件,后续状态由前一个状态通过某些规则转变而来。
4. 状态转移规则(State Transition Rules)
这些规则描述了如何从一个状态 a a a转移到另一个状态 b b b。具体规则如下:
-
判定节点和谓词:
- 若 a a a是谓词 p p p的判定节点入边上的状态, b b b是该节点标记为true的出边上的状态,且 a ⊨ S p a \models_S p a⊨Sp成立,则 b b b与 a a a相同。
- 若 a a a是谓词 p p p的判定节点入边上的状态, b b b是该节点标记为false的出边上的状态,且 a ⊨ S ¬ p a \models_S \neg p a⊨S¬p成立,则 b b b与 a a a相同。
-
赋值操作:
- 若 a a a是赋值 v : = e v := e v:=e前的状态, b b b是紧跟该赋值后的状态,则 b b b为 a [ T a [ e ] / v ] a[T_a[e]/v] a[Ta[e]/v]。 T a [ e ] T_a[e] Ta[e]是表达式 e e e根据状态 a a a计算而得的值, a [ d / v ] a[d/v] a[d/v]是除了 v v v值被设为 d d d外其余都与 a a a相同的一个赋值。因此,赋值之后的状态 b b b除了 v v v的值以外其余都与 a a a相同,而 v v v的值是表达式 e e e根据之前的状态 a a a计算而得的值。
5.结构(Structure)
在程序验证和逻辑表达式的上下文中,"结构"通常指的是定义了一系列逻辑公式如何被解释的系统或框架。在计算机科学中,特别是在形式方法和逻辑编程中,结构不仅仅是数据的组织方式,还包括对这些数据适用的操作和它们之间的关系。
一个结构通常包括:
- 一组基本元素:这些可以是数据类型、对象、变量等。
- 一组操作:这些操作定义了如何在基本元素上执行计算或变换。
- 一组关系:这些关系定义了元素之间的逻辑或数学联系。
在程序的上下文中,结构可能具体指:
- 变量和它们的类型系统
- 函数和方法以及它们的定义
- 类和对象及其继承关系
在程序验证中的角色
在程序验证和模型检验中,结构(Structure)为验证工具提供了必要的上下文,使其能够理解和检查程序状态是否满足特定的逻辑公式。结构定义了这些公式的含义,例如,一个逻辑公式 φ \varphi φ可能表示“所有整数类型的变量都大于0”。结构会明确“整数类型的变量”和“大于”这样的概念在程序中是如何被定义和解释的。
结构的具体例子
假设我们有一个简单的程序,其中包括几个整数变量和布尔变量,结构会包括:
- 变量的类型:整数、布尔等。
- 变量之间的关系:例如,某些变量可能依赖于其他变量的值。
- 操作的定义:如算术运算、逻辑运算等。
具体例子
假设我们有以下代码:
x = 1
if x > 0:y = 2
else:y = 3
- 初始状态 a a a: x = 1 x = 1 x=1
- 判定节点:检查 x > 0 x > 0 x>0, a ⊨ S x > 0 a \models_S x > 0 a⊨Sx>0成立
- 转移到状态 b b b: y = 2 y = 2 y=2
- 最终状态 b b b: x = 1 , y = 2 x = 1, y = 2 x=1,y=2