Wings 的博客
归档 系列 分类 标签 关于 友链 开往
Wings 的博客

「笔记」形式化方法

Wings  收录于  类别 期末速通
     约 3727 字  预计阅读 8 分钟    次阅读     条评论  

都研究生了还在期末速通.

对于一段程序:

  • 前断言precondition: 入口, 输入一定满足的条件
  • 后断言postcondition: 出口, 输出一定满足的条件
  • 循环不变式loop invariance: 循环入口, 循环涉及到的变量 (输入和中间变量) 一定满足的条件
  1. 建立断言: 输入, 中间变量, 输出分别为 $X, Y, Z$. 前断言 $\phi(X)$, 后断言 $\psi(X, Z)$, 循环不变式 $P(X, Y)$
  2. 建立检验条件: 一条路径 $j$ 连接两个断点 $i, k$, $R_j(X, Y)$ 为程序走路径 $j$, $X, Y$ 需要满足的条件. $r_j(X, Y)$ 为经过 $j$ 后 $Y$ 的值. 则检验条件为: $P(X, Y) \land R_j(X, Y) \rightarrow \psi(X, r_j(X, Y))$
  3. 证明所有检验条件, 若都为真, 则程序是部分正确的

对每个循环设一个计数器变量 $C_i$, 循环入口处建立一个 $C_i$ 有固定上界的断言, 然后证明程序部分正确.

谓词变换函数 $wp(S, R)$, 是程序 $S$ 能够终止并且后置条件 $R$ (后断言) 成立的最弱前置条件. $wp(S, true)$ 表示程序一定终止的前断言.

  • $wp(S, false) = false$
  • $wp(x:=e, R)$ = $R[e/x]$ (用 $e$ 替换 $x$)
  • $R_1 \rightarrrow R_2 \Rightarrow wp(S, R_1) \rightarrow wp(s, R_2)$ (if 条件里会用到)
  • $wp(S, R1) \land wp(S, R2) = wp(S, R1 \land R2)$
  • $wp(S, R1 \lor R2) = wp(S, R1) \lor wp(S, R2)$
  • $wp(S_1 ; S_2, R) = wp(S, wp(S2, R))$ (从后往前推)

前断言 $P -> wp(S, R)$ 则程序 $S$ 完全正确.

  • 有限状态机: 有终止节点集
  • Moore 有限状态机: 没有终止节点集, 每个节点有一个输出
  • Mealy 有限状态机: 没有终止节点集, 每条边有一个输出

模式Schema包含名称 (S), 声明 (D), 断言/谓词 (P)

D P S

D 可以声明变量 (members: $\mathbb P$ Person) 和关系 (hasphone: Person $\leftrightarrow$ Phone), P 中限制断言 (dom hasphone $\subseteq$ members)

关系的特殊运算 (这里把关系当成 map<key, value>):

  • 定义域限制: $D \lhd R$ = R.iter().filter(|(k, _)| D.contains(k)), $D \unlhd R$ = R.iter().filter(|(k, _)| !D.contains(k))
  • 值域限制: $R \rhd V$ = R.iter().filter(|(_, v)| V.contains(v)), $A \unrhd B$ = R.iter().filter(|(_, v)| !V.contains(v))
  • 关系的像: $R[D]$ = R.iter().filter(|(k, _)| D.contains(k)).map(|(_, v)| v)
  • 重载: $R_1 \oplus R_2$ = for (k, v) in R2.iter() { R1.insert(k, v) } R1

模式的状态变化, 后状态在每个字段之后加上 ' 即可. 可以用 $\Delta S$ 表示 S 的前后状态放在一起的声明 (如修改操作 (操作也是一种模式) 将会改变状态). 对于不改变状态的操作, 用 $\Xi S$ 来表示. 声明字段后加上 ? 表示是输入, ! 表示是输出.

比如:

[ U s p r a L p a Ξ u i u i e L a e c I o a c i L ? s ? s r o s g t n g s t s o : L L , g s , i i S s i L g o ∈ o S w v t y w v o S U g g W y o a e L s o e g y s g r g o s r c o ' r ' g s e e e e r d t ⊆ g d e r d g d d : i S ' = d I I ] v r y I n n U e e s = r n ! ! ( s : g e : 类 e { g = r P ⊆ } ' b 型 o u ↔ U d = o ? 要 s o l W e m { ∈ 在 o r } r p a 开 d a c s t 头 s i w v 说 o e r 明 d Δ u p a r R L ? a c e ) e o : s t g g g s i ' i s U w v s y s o e = t s e r ' e r d r r ; ' = e L L g Δ o o p = a L g g ? c ∪ o S S : p t g y y a i { S s s W s v u y ' o s e ? s r w } d o r d ∪ { ( u ? , p ? ) } Δ r p Ξ L e a L o g s o g ' s g S w S y = o Δ u u p p a r y s r L L ? ? ? a c e s r d o o : s t g e ' g g ∉ = s i ' g I S U w v ; = n y s a p o e = s e c a r ' a p r t s d r c a ; i s ' = e t s v w g i s p e o = a v w ? r c e o : d p t ' r ( a i d W u s v = o ? s e r ) w a d o ∪ c r t d { i u v ? e }

线性时间序列/路径 $\sigma = \{s_0, s_1, \cdots \}$, 谓词/公式 $p$ 在时间点 $j$ 为真, 则记为 $(\sigma, j) \models p$

j 0 1 2 3 …
x 1 2 3 4 …
y 5 4 3 2 …
x=y F F T F …

$$(\sigma, 2) \models (x=y)$$

  • Next Operator $\bigcirc$ (X): $(\sigma, j) \models \bigcirc p \Leftrightarrow (\sigma, j+1) \models p$
  • Always Operator $\Box$ (G): $(\sigma, j) \models \Box p \Leftrightarrow \forall k \geq j, (\sigma, k) \models p$ ($j$ 及之后每个时间都满足 $p$)
  • Eventually Operator $\Diamond$ (F): $(\sigma, j) \models \Diamond p \Leftrightarrow \exists k \geq j, (\sigma, k) \models p$ ($j$ 后续存在某一时刻满足 $p$)
  • Until Operator $\mathrm{U}$: $(\sigma, j) \models p \mathrm{U} q \Leftrightarrow \exists k \geq j, \forall j \leq i \le k, (\sigma, k) \models q \land (\sigma, i) \models p$ ($p$ 一直满足, 直到后续一个 $q$ 满足, 注意当 $p$ 不满足但是 $q$ 满足时, 也算满足)
$p$ F T T F …
$q$ F F F T …
$p \mathrm{U} q$ F T T T …

如果程序(状态机, 每个点上有若干谓词) $M$, 从 $s$ 开始的每一条路径都满足公式(谓词) $\Phi$, 则说 $M, s \models \Phi$

LTL 只考虑一条路径, 而 CTL 考虑所有路径, 有函数 AG, EG, AF, EF, AU, EU. 其中 G(lobal), F(uture), (ne)X(t), U(ntil) 和上述相同, A 表示 All, E 表示 Exists

首先定义两个函数

  1. $pre_{\exists}(Y)$ 中的点存在一条边到 $Y$ 中的点, 可以认为是 $Y$ 中所有点的前驱集合的并集
  2. $pre_{\forall}(Y)$ 中的点所有边都到 $Y$ 中的点, 可以认为是 $Y$ 中所有点的前驱集合的交集

首先很容易可以看出满足 $\Phi$ 的所有状态的集合 $[\Phi]$. 下面将要求各种东西.

存在下一个点满足 $\Phi$, 那就是满足 $\Phi$ 的上一个, 也就是 $pre_{\exists}([\Phi])$

所有路径都有存在满足 $\Phi$ 的点. 可以按照树形 dp 的方法来考虑 (虽然这是个图, 但是可以转换成无限深度的树), $[\Phi]$. 中的点对于的子树首先满足条件. 往上推, 所有路径都得满足, 所以前驱应该是 $pre_{\forall}([\Phi])$. 加入结果. 直到结果不再变化 (到达不动点). 有 $X := X \cup pre_{\forall}(X)$

(ppt 上没有, 但是我觉得可以举一反三, 不过好像一看图就知道了, 所有可达节都满足 $\Phi$, 则这个点满足 $AG(\Phi)$, 不写了

存在一条路径, 上面的点都满足 $\Phi$. 那么不在 $[\Phi]$ 中的点一定不满足, 所有点的前驱 $pre_{\exists}([\Phi])$, 如果不在 $[\Phi]$ 中, 就不满足. 所以这里可以从 $[\Phi]$ 开始做差, 换成公式就是 $X := X \cap pre_{\exists}(X)$, 从 $[\Phi]$ 开始迭代, 直到不动点.

根据前面说的, 首先满足 $\Psi$ 的点一定满足, 所以开始找一直满足 $\Phi$ 的前驱. 也就是 $X := X \cup ([\Phi] \cap pre_{\exists}(X))$.

可以转成 $E(true \mathrm{U} \Phi)$. 不转的话也很好理解, $[\Phi]$ 一定满足, 所以从这里开始找还有什么满足的前驱. 存在一条路径到 $[\Phi]$ 中的点就可以, 那么所有前驱都满足. $X := X \cup pre_{\exists}(X)$

可以看到上述转移方程都是形如 $X := X (\cup / \cap) Expr$ 的形式, 把右边第一个的 $X$ 换成 $[\Phi]$, 右边就构造出了一个函数 $F(X)$ (实际上写的时候是 $F(X)$)

  1. 当满足 $\Phi$ 的点都满足 $XX(\Phi)$ 的时候是 $\cup$, $F^1(\emptyset)$ 是我们上述算法考虑的第一层, 所以结果是 $F(X)$ 的最小不动点 $F^{n+1}(\emptyset)$.
  2. 当满足 $\Phi$ 的点不一定满足 $XX(\Phi)$ 时是 $\cap$, $F^1(S)$ 是我们上述算法 (EG) 考虑的第一层, 所以结果是 $F(X)$ 的最大不动点 $F^{n+1}(S)$. 构造结果是最大不动点的函数时, 经常写成 $G(X)$.

联想一下, 最大是 Greatest, 和公式名中的 G(lobal) 一样, 所以求 Global 就是最大, 就是交集. 剩下的 F 和 U 都是最小. 而 A 是所有都得满足, 所以前驱是 forAll, 而 E 是存在一条即可, 所以前驱是 Exists. 这样就很好记忆了, 然后碰到什么就推一推转移, 就可以构造出函数了.

一个系统 $M, s0$ 是否满足 $\Phi$ (这个 $\Phi$ 可以是任意公式, 比如 $EF(p)$, $p$ 是原子谓词), 只需要用不动点求 $[\Phi]$, 然后判断看 $s_0 \in [\Phi]$ 的话就满足.

一些概念:

  • 小写字符串表示事件

  • 大写字符串表示进程

  • $x, y, z$ 表示事件变量

  • $A, B, C$ 表示事件集合

  • $X, Y$ 表示进程变量

  • 进程 $P$ 涉及到的事件集合叫字母表 $\alpha P$

  • 以 $A$ 为字母表但是不执行 $A$ 中事件的进程叫 $STOP_A$, 也就是事件无法继续下去了, 进程卡死了

  • 前缀 $x \to P$ 表示先执行事件 $x$, 然后执行进程 $P$ 的进程

  • 选择 $x \to P | y \to Q$ 表示当事件 $x$ 发生时执行进程 $P$, 当事件 $y$ 发生时执行进程 $Q$ 的进程

  • 进程可以递归定义, 比如 $P = \{x \to P | y \to STOP_{\alpha P}\}$

  • 通信 $c?v$ 表示来自通道 $c$ 上输入到进程的消息 $v$, $c!v$ 表示从进程输出到通道 $c$ 上的消息 $v$.

  • 进程的迹 Trace 是指进程执行过程中发生的事件序列, 用 $\langle x, y, \cdots \rangle$ 这样来表示. 连接操作 $\langle x \rangle ^ \langle y \rangle$ 表示将两个迹连接起来, 得到 $\langle x, y \rangle$, 全迹 Traces 是所有可能的迹的集合. 比如进程 $P = \{ ready \to exec \to P \}$ 的全迹 Traces($P$) = $\{ \langle \rangle, \langle ready \rangle, \langle ready, exec \rangle, \langle ready, exec, ready \rangle, \cdots \}$

$P \Vert Q$ 也是一个进程, 且有如下法则

字母表相同时

  • $P \Vert STOP = STOP$ (一个进程死锁导致系统死锁)
  • $(c \to P) \Vert (c \to Q) = (c \to (P \Vert Q))$
  • $(c \to P) \Vert (d \to Q) = STOP$ 执行不同动作死锁
  • $(x:A \to P(x)) \Vert (y:B \to Q(y)) = (z:(A \cup B) \to (P(z) \Vert Q(z)))$ 公共选择才能保留 (可以从上面一个推出, 非公共的都 STOP 了)

字母表不同时, 若 $a \in \alpha P - \alpha Q, b \in \alpha Q - \alpha P, c \in \alpha P \cap \alpha Q$, 有

  • $(a \to P) \Vert (c \to Q) = a \to (P \Vert (c \to Q))$ (因为 $a$ 和 $Q$ 无关, 所以 $a$ 需要先执行, 之后的部分才依然可以并发)
  • $(a \to) \Vert (b \to Q) = (a \to (P \Vert (b \to Q)) | b \to ((a \to P) \Vert Q))$ (可以按照任意顺序执行. 带入上一个看可以发现, 如果 $b$ 是 $c$, 那么先执行 $c$ 会导致 $a \to P$ 死锁)

例子: $\alpha P = \{a, c\}, \alpha Q = \{b, c\}, P = (a \to c \to P), Q = (c \to b \to Q)$, 求 $P \Vert Q$

$$ \begin{aligned} P \Vert Q &= (a \to c \to P) \Vert (c \to b \to Q) \newline &= \color{red}{a \to c \to \underline{(P \Vert (b \to Q))}} \newline &= a \to c \to ((a \to c \to P) \Vert (b \to Q)) \newline &= a \to c \to (a \to b \to ((c \to P) \Vert Q) | b \to (P \Vert Q)) \newline &= a \to c \to (a \to b \to c \to (P \Vert (b \to Q)) | b \to \color{red}{(P \Vert Q)}) \newline &= a \to c \to \underline{(a \to b \to c \to (P \Vert (b \to Q)) | b \to a \to c \to (P \Vert (b \to Q)))} \newline &= a \to c \to \mu X. (a \to b \to c \to X | b \to a \to c \to X) \newline \end{aligned} $$

上述的意思是定义进程 $X$, 然后 $P \Vert Q = a \to c \to x$

并发的迹:

  • $\alpha P \cap \alpha Q = \emptyset$ 时, $(P \Vert Q)$ 的迹是事件的穿插, 即两个进程的事件可以任意顺序发生 (单个进程的事件相对顺序不变)
  • $\alpha P = \alpha Q$ 时, $traces(P \Vert Q) = traces(P) \cap traces(Q)$
  • 其他情况求一下 $P \Vert Q$, 然后求迹.

构造一个进程 $R_Z$ 使得 $P_X \Vert_Y Q$ 没有死锁, 先求 $(P_X \Vert_Y Q)$, 然后找到不死锁的选择路径, 把在 $Z$ 中的事件按顺序提出来即可.

比如 $X = \{a, b, c, d\}, Y = \{c, d\}, P = a \to c \to P | b \to d \to P, Q = c \to d \to Q$, 计算可得 $P_X \Vert_Y Q = a \to c \to a \to STOP | a \to c \to b \to d \to (P \vert Q) | b \to STOP$, 要求一个 $R_Z$, 其中 $Z = \{a, b\}$, 使得 $R_Z \Vert_X (P_X \Vert_Y Q)$ 无死锁, 可以看到 $P \Vert Q$ 只有一条选择 $a \to c \to b \to d \to (P \Vert Q)$ 无死锁, 所以把在 $Z$ 中的事件按顺序提出来, 得到 $R = a \to b \to R$, 即确保整个系统按 $a, b$ 事件相对顺序执行. 可以看另外两条路, 都不符合先 $a$ 后 $b$ 的事件顺序.

用 CSP 描述 AB 协议

S A a C H R B b

$$ \begin{aligned} \alpha S_0 &= \{A?m_0, A?m_1, a!m_0, a!m_1, timeout, a?ack_0, a?ack_1 \} \newline S_0 &= A?m_0 \to a!m0 \to S_1 \newline S_1 &= a?ack_0 \to S_2 | timeout \to a!m_0 to S_1 \newline S_2 &= A?m_1 \to a!m_1 to S_3 \newline S_3 &= a?ack_1 \to S_0 | timeout \to a!m_1 \to S_3 \newline \newline \alpha R_0 &= \{ b?m_0, b?m_1, drop, b!ack_0, b!ack_1 \} \newline R_0 &= b?m_0 \to R_1 \newline R_1 &= drop \to R_0 | b!ack_0 \to R_2 \newline R_2 &= b?m_1 \to R_3 \newline R_3 &= drop \to R_2 | b!ack1 \to R_0 \newline \newline P &= S_0 \Vert R_0 \end{aligned} $$

这里只考虑 S 和 R, 没有考虑 CH. A, B 是用户端点, a, b 是通道端点

更新于 2024-12-24
 形式化
返回 | 主页