软件可靠性 - 结构以及赋值等概念的理解

程序的一个状态简单地说就是程序变量的一组赋值。我们说过：赋值$a$（一个状态）满足公式$\phi$可以记为$M_a(\phi )=\text{TRUE}$（这里未提及结构$S$，假设$S$可由上下文获得），或者记为$a{\models }_S\phi$。程序的执行是一个有限或无限的状态序列，其中第一个状态满足初始条件，其余每个后继状态$b$都由其前驱状态$a$按如下方式获得：

• 若$a$是谓词为$p$的判定节点入边上的状态，$b$是该节点标记为true的出边上的状态，且$a{\models }_{S}p$成立，则$b$与$a$相同。
• 若$a$是谓词为$p$的判定节点入边上的状态，$b$是该节点标记为false的出边上的状态，且$a{\models }_S\neg p$成立，则$b$与$a$相同。
• 若$a$是赋值$v:=e$前的状态，$b$是紧跟该赋值后的状态，则$b$为$a[T_a[e]/v]$。$T_a[e]$是表达式$e$根据状态$a$计算而得的值，$a[d/v]$是除了$v$值被设为$d$外其余都与$a$相同的一个赋值。因此，赋值之后的状态$b$除了$v$的值以外其余都与$a$相同，而$v$的值是表达式$e$根据之前的状态$a$计算而得的值。

下面来解释这段文字中的一些概念，更好地理解它的意思。

1. 状态（State）

在程序执行过程中，状态是程序变量的一组赋值。例如，如果有两个变量$x$和$y$，一个可能的状态是$x=1$，$y=2$。

2. 公式（Formula）

公式是一个逻辑表达式，可以用来描述某个状态是否满足某种条件。例如，公式$\phi$可以是$x>0$。如果状态$a$中的$x$为1，那么我们可以说$a$满足公式$\phi$。

3. 状态序列（State Sequence）

程序的执行可以看作是从一个状态到另一个状态的变化过程。这个过程可以用一个状态序列来表示。初始状态满足初始条件，后续状态由前一个状态通过某些规则转变而来。

4. 状态转移规则（State Transition Rules）

这些规则描述了如何从一个状态$a$转移到另一个状态$b$。具体规则如下：

• 判定节点和谓词：

  • 若$a$是谓词$p$的判定节点入边上的状态，$b$是该节点标记为true的出边上的状态，且$a{\models }_{S}p$成立，则$b$与$a$相同。
  • 若$a$是谓词$p$的判定节点入边上的状态，$b$是该节点标记为false的出边上的状态，且$a{\models }_S\neg p$成立，则$b$与$a$相同。

• 赋值操作：

  • 若$a$是赋值$v:=e$前的状态，$b$是紧跟该赋值后的状态，则$b$为$a[T_a[e]/v]$。$T_a[e]$是表达式$e$根据状态$a$计算而得的值，$a[d/v]$是除了$v$值被设为$d$外其余都与$a$相同的一个赋值。因此，赋值之后的状态$b$除了$v$的值以外其余都与$a$相同，而$v$的值是表达式$e$根据之前的状态$a$计算而得的值。

5.结构（Structure）

在程序验证和逻辑表达式的上下文中，"结构"通常指的是定义了一系列逻辑公式如何被解释的系统或框架。在计算机科学中，特别是在形式方法和逻辑编程中，结构不仅仅是数据的组织方式，还包括对这些数据适用的操作和它们之间的关系。

一个结构通常包括：

1. 一组基本元素：这些可以是数据类型、对象、变量等。
2. 一组操作：这些操作定义了如何在基本元素上执行计算或变换。
3. 一组关系：这些关系定义了元素之间的逻辑或数学联系。

在程序的上下文中，结构可能具体指：

• 变量和它们的类型系统
• 函数和方法以及它们的定义
• 类和对象及其继承关系

在程序验证中的角色

在程序验证和模型检验中，结构（Structure）为验证工具提供了必要的上下文，使其能够理解和检查程序状态是否满足特定的逻辑公式。结构定义了这些公式的含义，例如，一个逻辑公式$\phi$可能表示“所有整数类型的变量都大于0”。结构会明确“整数类型的变量”和“大于”这样的概念在程序中是如何被定义和解释的。

结构的具体例子

假设我们有一个简单的程序，其中包括几个整数变量和布尔变量，结构会包括：

• 变量的类型：整数、布尔等。
• 变量之间的关系：例如，某些变量可能依赖于其他变量的值。
• 操作的定义：如算术运算、逻辑运算等。

具体例子

假设我们有以下代码：

x = 1
if x > 0:y = 2
else:y = 3

• 初始状态$a$: $x=1$
• 判定节点：检查$x>0$，$a{\models }_{S}x>0$成立
  • 转移到状态$b$: $y=2$
  • 最终状态$b$: $x=1,y=2$