Overview：
这节课整体是一个熟能生巧的课，动上几次手写题找到感觉之后就清楚很多了，比光看老师的ppt要舒服很多。
Week 1
Hoare triples 和 Weakest precondition
为了验证代码的正确性，需要一个方法来验证 Hoare 引入了 Hoare triple model： {P} Precondition S {Q} Postcondition 如果系统P经过S之后系统到达了postcondition Q，那么就说这个系统是正确的 这个想法很朴素，但是太过于笼统，不好系统化验证。
Dijkstra improvement
Dijkstra 引入了Weakest precondition这个概念，也就是在经过S能够到达Q的最弱的前提。 记作：WP.(x := x + 1).(5 <= x) 在这里是
NOTE
这个weakest precondition 是一个在系统验证领域中很重要的概念，但是在当前<截至week7>的学习内容中用处不是很大，我们在无意识的用它，但是不知道这个概念也无妨。这里仅作描述。 WP的强大之处在于将程序转化为了可以计算的数学逻辑：{P} S {Q} ->
为了记述这个记号，Dijkstra 引入了Guarded command language用来描述算法（相对严格的伪代码）
Guarded Command Language
这是一个最小化的，过程性的语言。 首先先定义这个语言中的基本操作 0. Skip WP.skip.Q ≡ Q
这里的意思是skip的定义就是由WP.skip.Q ≡ Q这个现象定义出的，读法应该是Weakest precondition of Skip to Q is Q,也就是通过weakest precondition这个东西来定义全部的操作，这里的WP其实都是倒推出来的
Concatenation WP.(R;S).Q ≡ WP.R.(WP.S.Q) 这式子表示：要让 R;S 执行后满足 Q 等价于先算执行 S 之前必须满足什么，再算执行 R 之前必须满足什么
Assignment WP.(x := E).Q ≡ Q(all x replaced by E) 执行将x赋值成E之后符合Q，那么执行前WP需要符合用 E 代替 x 后的 Q 成立 这个定义有点别扭（因为实际上是根据effect反向定义出来的），但是这个看一个例子可以好懂一点
S : x = x + 1 Q : x > 5 那么WP(x = x + 1, x > 5) = -> x + 1 > 5 -> x > 4 通过反向代入可以算出WPSelection(if..fi)
{P}
if B0 -> S0
[] B1 -> S1
fi
{Q}表示
P => B0 v B1
^
{P ^ B0} S0 {Q} ^ {P ^ B1} S1 {Q}- Repetition
{R}
do B -> S od
{Q}表示
R ⇒ P
∧
{P ∧ B ∧ vf = VF} S {P ∧ vf < VF}
∧
P ∧ B ⇒ 0 < vf
∧
P ∧ ¬B ⇒ QWeek 2
符号
j.0 x j.1 x ... j.N-1 = <1. (x j) : 2. ( 0<= j < N) : 3. (f.j) > 其中后面的形式叫做quantified form
1代表连接各个元素的符号 2代表筛选出的元素集合 3代表元素的形式
对于quantified form可用的laws：
- empty range law: 存在identity element. 〈 ⊕ j : 0 <= j < 0 : f.j 〉 {empty range} = ID⊕
- one-point: 〈 ⊕ j : j = i : f.j 〉 {one-point} = f.i
- The split off a term law (展开) 〈 ⊕ j : 0 <= j < i+1 : f.j 〉 where 0<= i < N {split off j = i term} =〈 ⊕ j : 0 <= j < i : f.j 〉 ⊕ f.i
- Strengthening 〈 ⊕ j : 0 <= j < i : f.j 〉 ∧ i = N ⇒ {Leibniz} 〈 ⊕ j : 0 <= j < N : f.j 〉
构建程序
接下来就是构建程序的过程，构建程序是一个公式化过程，用牢亨利的话来说就是"no, don't think, you are trying to think again, don't think."只要跟随着步骤就能写出一个程序，甚至它的表现一般都相当不错。 构建程序的步骤：
| Step | Derivation |
|---|---|
| 列出precondition/postcondition | pre = <sth> pro = <sth> |
| 首先建立domain model，将postcondition转化为quantified expression | (0) C.n = <转写postcondition> |
| 根据C.n 推导出C.0 和 C.(n+1) | (0) C.n = <sth> C.i = (1) C.0 (2) C.n+1 |
| 重写postcondition为C.N 形式，并引入变量r | post: r = C.N |
| 强化表述 (这一步引入 | r =C.n |
| 确定不变量 | P0 : r = C.n P1 : 0 <= n ∧ n <= N （只是示例） |
| establish invariant 的意思是建立不变关系，也就是设立让之前的所有关系成立的最小值，这一步其实就是初始化 | n,r = ID,ID(ID代表identity element,零元素) |
| 建立Guard，确定这个程序在得到我们的想要的结果时停下 | Guard: n != N |
| 建立vf，确定这个程序有一个在持续下降的变量使程序最终停下 | vf = N-n |
| 构建循环体，这个也就是程序的主体 | <Loop body> |
| 最终程序结构: |
n,r = ID,ID;
\<loop body\>
-> {postcondition}最终得到我们想要的postcondition。
NOTE
确立不变量的三个原则： 首先可以简单的判断是否为真 在循环中可以尽量简单的保持true 可以得出最终结果
## 构建循环(loopbody)
这个构建loopbody的过程就像是最开始学解一元一次方程，我们先把所有的东西列出来，然后通过简单代换得到一个式子的解。
以解简单累加为例子：(n, r := n+1, E). (r = C.n) //E 代表未知变化量，其实也就是函数的因变量一样的感觉，我们的最终目标其实就是求出E，这一步有点像把程序领域的东西带入数学计算领域 = { text substitution } // 这一步将n的变化引入r的式子 E = C.(n+1) = { (2) from model } //这时我们就能通过C.n+1 做分解了，得出一个前后的关系史 E = C.n + f.n = { P0 binds C.n to a variable } //最终我们把原式子代回就能得到一个只有函数中变量的关系式，我们将数学领域的变化带回了程序里 E = r + f.n
## 简单通用形式
因为形似 < sth.j : a<=j< b : f.j >这种形式的其实都一个样子，所以可以直接推导出类似这种的标准形式的程序
```text
post: < ⊕.j : a<=j< b : f.j > // ⊕代表任意计算符
首先先rewrite post 将其转化为
< ⊕.j : a<=j< n : f.j > and a <= n <= b
Domain model
(0)C.n. = < ⊕.j : a<=j< n : f.j > a <= n <= b
(1)C.a = $ID_⊕$
(2)C.(n+1) = C.n ⊕ f.n ,α <= n <= β
Rewrite post
r = C.b
Strengthen post
r = C.n ∧ n = b
Choose invariant
P0 : r = C.n
P1 : a <= n <= b
Guard
n != b
Establish invariant
n , r = a, $ID_⊕$
variant
b-n
Loop body:
(n , r := n+1,E).P0
{text substitution}
E = C.(n+1)
{(2)}
E = C.n ⊕ f.n
{P0}
E = r ⊕ f.n
Program:
n, r := α, Id⊕
;do n ≠ β →
n, r := n+1, r ⊕ f.n
od对于需要筛选的式子，比如所有even number 我们通过新加一个函数的方式实现：
R = <f.j : 0<= j < n: g.(f.j)>
g.x = 1 <= even.x
g.x = 0 <= odd.x其中 => imply <= if
对于这种问题，我们在构建loopbody时要分类讨论一下
符合条件的case
(n, r := n+1, E).P0
= { Textual Substitution }
E = C.(n+1)
= { Case Q.(f.n) (4) }
E = C.n ⊕ h.(f.n)
= { P0 }
E = r ⊕ h.(f.n)
other case:
(n, r := n+1, E).P0
= { Textual Substitution }
E = C.(n+1)
= { Case ¬Q.(f.n) (5) }
E = C.n ⊕ Id⊕
= { P0 }
E = r ⊕ Id⊕最后在构建program的时候加上IF就行
n, r := α, Id⊕
; do n ≠ β →
if Q.(f.n) → n, r := n+1, r ⊕ h.(f.n)
[] ¬Q.(f.n) → n, r := n+1, r ⊕ Id⊕
fi
odSearch
Linear search:
线性搜索是一个很简单的程序，核心思想就是在list中从头往后找，找到第一个符合要求的位置，这里我们要求这个元素必须存在 这个要求转写成postcondition的话就是找到一个位置，使得前面的所有位置都不符合要求，且这个位置符合要求，这里我就直接写generic 线性搜索了
post = <∀ j : α <= j < i : ¬ Q.(f.j) > ∧ Q.(f.i) // 对于所有前面的元素都不符合要求Q，且i符合
建立Domain model
(0) C.i ≡ <∀ j : α <= j < i : ¬ Q.(f.j)> , α <= i <= β
(1) C. α ≡ True
(2) C.(i+1) ≡ C.i ∧ ¬Q.(f.i) , α <= i < β
这里的目标是先把<∀ j : α <= j < i : ¬ Q.(f.j) >凑齐
转写post
Post: C.i ∧ Q.(f.i)
Choose invariants.
P0: C.i
P1: α <= i <= β
Guard.
¬Q.(f.i)
Establish invariants.
i := α
vf
K - i
其中K代表确定存在的那个我们要找的东西的index，尽管我们不知道它的位置，但是总归小于β
loop body省了
最终程序：
i := 0
;do ¬Q.(f.i) →
i := i+1
odbounded linear search
一个很明显的改进就是如果这个元素不存在呢？ 那么我们首先就要改进post： post : <∀ j : α <= j < i : ¬ Q.(f.j) > ∧ (Q.(f.i) ∨ i = β-1) 代表在i之前没有符合条件的，同时要么找到i符合条件,要么i = n-1(这里面蕴含了Q.(f.i)). 也就是现在停止条件有两个了。 中间过程全省，跟之前基本一模一样 Guard 变成 f.i ≠ X ∧ i ≠ N-1 vf 变成 (K ↓ N-1) - i 最后程序变成:
i := 0
;do f.i ≠ X ∧ i ≠ N-1 →
i := i+1
od
;if f.i = X → “found case”
[] f.i ≠ X ∧ i = N-1 → “not found case”
fiBinary chop
讲述了一个post condition没法简单的用一个式子列出来的情况 也就是找一个i位置小于X下一位大于X的式子
这里引入了一个新的概念：Binary chop 二分切割 Binary chop 是Binary search 的超集。如果Binary chop作用在一个有序list上，那就是binary search
它的基本思想是这样的： 首先这个关系必须是一个二元的关系，比如x = 0 和 y != 0
然后在集合上开始进行二分查找：每次设h为x+y/2，如果h符合x的关系那就x := h, y符合就 y:=h直到找到关系的转折点也就是y = x+1。
这个Binary chop相比于普通二分查找的改进是它可以在无序列表中使用了，并且支持的操作也更多一点。本质上它是找一个分割点，也就是某一个性质的转变点。
这里也是直接写generic form了
Pre : Q.α ∧ ¬Q.β
Post : Q.i ∧ ¬Q.(i+1) ∧ α <= i < β
strengthen post
Post : Q.i ∧ ¬Q.j ∧ j = i+1 ∧ α <= i < β. //拎出来一个j，使得可以开始从两边逼近
选invariant:
P0 : Q.i ∧ ¬Q.j
P1 : α <= i < j <= β
establish invar
i, j := α, β
Guard.
j ≠ i+1
Vf
j-i
接下来就是建立loop body的过程了，这个过程中我们要保证在循环的过程中不变量关系依然保持不变，因此我们需要确定的是在什么情况下我们可以赋值h给i，什么情况下我们赋值h给j
步骤；
Case i := h
(i := h).P0
= {text Sub.}
Q.h ∧ ¬Q.j
= { P0 } //因为P0告诉我们的不变的关系中有¬Q.j这一条，因此这个可以去掉
Q.h
最终得出 if Q.h → i := h
反之 if ¬Q.h → j := h
程序：
i, j := α, β
;do j ≠ i+1 →
h := (i+j) div 2
;if Q.h → i := h
[] ¬Q.h → j := h
fi
odSegment Sum
对于一个数列f[i..j) ,我们求出其中的一个区间，使得那个区间和是最小的。 这节课的新东西是通过引入新的model 式子来推进计算，最终得到一个优化了的，可用的程序。
求一个最小区间和
Pre: f[0.N)
Post: r = <↓i,j : 0 <= i <= j<= N: SS.i.j>
Domain model
(0) SS.i.j = <+ k : i <= k < j : f.k>. //这里先列出区间和函数的性质
(1) SS.i.i = 0 //略了
(2) SS.i.(j+1) = SS.i.j + f.j
(3) C.n = < ↓ i, j : 0 <= i <= j <= n : SS.i.j > , 0 <= n <= N //这里开始是常规的C.n步骤了
(4) C.0 = 0 //考试上记得把步骤写明白了，什么{one-point}啊，调用前面的东西啊，还有后面的范围啊
(5) C.(n+1) = C.n ↓ D.(n+1) , 0 <= n < N
这里是推导C.(n+1)的步骤
C.(n+1)
= {(3)}
〈 ↓ i, j : 0 <= i <= j <= n+1 : SS.i.j 〉
= { Split off j=n+1 term } //这里为了得出老C.n的形式要对区间进行拆分，我们固定j为n+1，得到了两个部分： j <= n和j = n+1，那么代回去得到了下面的两个式子
〈 ↓ i, j : 0 <= i <= j <= n : SS.i.j 〉 ↓ 〈 ↓ i : 0 <= i <= n+1 : SS.i.(n+1) 〉
= {(3)} //这个地方我们得到了一个跟我们之前的表达式有些不同的形式的表达式，那么我们就可以开始拆分了。
C.n ↓ 〈 ↓ i : 0 <= i <= n+1 : SS.i.(n+1) 〉
= {(6) below }
C.n ↓ D.(n+1)
(6) D.n = 〈 ↓ i : 0 <= i <= n : SS.i.n 〉 , 0 <= n <= N
接下来开始推导D.n的性质
(7) D.0 = 0 //省略
D.(n+1)
= {(6)}
〈 ↓ i : 0 <= i <= n+1 : SS.i.(n+1) 〉
= { Split off i=n+1 term }
〈 ↓ i : 0 <= i <= n : SS.i.(n+1) 〉 ↓ SS.(n+1).(n+1)
= {(1)}
〈 ↓ i : 0 <= i <= n : SS.i.(n+1) 〉 ↓ 0
= {(2)}
〈 ↓ i : 0 <= i <= n : SS.i.n + f.n 〉 ↓ 0
= { 把+f.n拆出来 }
(〈 ↓ i : 0 <= i <= n : SS.i.n 〉 + f.n) ↓ 0
= {(6)}
(D.n + f.n) ↓ 0
得到
(8) D.(n+1) = (D.n + f.n) ↓ 0 , 0 <= n < N
domain model就列完了
Rewrite postcondition.
Post : r = C.n ∧ n=N
Choose invariants.
P0: r = C.n ∧ d = D.n
P1: 0 <= n <= N
Guard.
n ≠ N
Establish invariants.
现在我们有两个model了，因此也就有两个变量
n, r, d := 0, 0, 0
Vf.
N-n
Loop body.
(n, r, d := n+1, E, E’).P0 两个变量自然也就是两个变化的参数
= { Text substitution }
E = C.(n+1) ∧ E’ = D.(n+1)
= {(5)}
E = C.n ↓ D.(n+1) ∧ E’ = D.(n+1)
= {(8) twice }
E = C.n ↓ (D.n + f.n) ↓ 0 ∧ E’ = (D.n + f.n) ↓ 0
= { P0 }
E = r ↓ (d + f.n) ↓ 0 ∧ E’ = (d + f.n) ↓ 0
最终程序
n, r, d := 0, 0, 0
; do n ≠ N →
n, r, d := n+1, r ↓ (d + f.n) ↓ 0, (d + f.n) ↓ 0
od
一个O(N)的程序构造好了。还有一个变种就是符合某种性质的区间和，比如奇数区间和。
这个相比于之前简单的加起来多了一个判断条件： OS.i.j ≡ 〈∀ k : i <= k < j : odd.(f.k)〉，代表这个区间全部符合这个性质 这个时候我们的domain model 就变成了： C.n = 〈↑ i, j : 0 <= i <= j <= n ∧ OS.i.j : SS.i.j 〉 ,0 <= i <= N
其他的全部都是没有变化的，直到我们需要求出D.(n+1)的性质时 D.n = 〈↑ i : 0 <= i <= n ∧ OS.i.n : SS.i.n 〉 ,0 <= n <= N
D.(n+1)
= { (9) }
〈↑ i : 0 <= i <= n+1 ∧ OS.i.(n+1) : SS.i.(n+1) 〉
= { split off i = n+1 }
〈↑ i : 0 <= i <= n ∧ OS.i.(n+1) : SS.i.(n+1) 〉 ↑ SS.(n+1).(n+1) //在分拆前面OS.i.(n+1)，我们可以拆出来一个OS.i.n以及一个odd.f.n
这时候就需要我们分类讨论了。
如果f.n是奇数，那么我们就需要加上，此刻
上式 = 〈↑ i : 0 <= i <= n ∧ OS.i.n : SS.i.(n+1) 〉 ↑ 0
最终 D.(n+1) = (f.n+D.n)↑0 ⇐ odd.(f.n) ,0 <= n < N
如果是偶数呢？
那么∧就不成立，此时左边就是false，也就是empty
ID ↑ 0 = 0
也就是 D.(n+1) = 0 ⇐ even.(f.n) ,0 <= n < N
省略构建loopbody
最终程序其实也就是加了个if而已
n, r, d := 0, 0, 0
;do n≠N →
if odd.(f.n) → n. r. d := n+1, r ↑ (f.n+d) ↑ 0, (f.n+d) ↑ 0
[] even.(f.n) → n. r. d := n+1, r ↑ 0, 0
fi
odSegment length
目标是在一个数列中找到最长的某个区间的区间长度，。
Segment property
这里的判断条件是单点的性质，比如找到全部都是0的区间的长度
这个某种意义上可以看作对于第六周的最小奇数区间和的变种。
我们同样要加入类似的判断条件 AQ.i.j ≡ 〈∀ k : i <= k < j : Q.(f.k)〉 ,0 <= i <= j <= N
Pre f[0..N)
Post r = 〈↑ i, j : 0 <= i <= j <= N ∧ AQ.i.j : j-i 〉
(0) AQ.i.j ≡ 〈∀ k : i <= k < j : Q.(f.k)〉 ,0 <= i <= j <= N
(1) AQ.i.i true
(2) AQ.i.(j+1) ≡ AQ.i.j ∧ Q.(f.j) ,0 <= i <= j < N
(3) C.n = 〈↑ i, j : 0 <= i <= j <= n ∧ AQ.i.j : j-i 〉 ,0 <= n <= N
(4) C.0 = 0
(5) C.(n+1) = C.n ↑ D.(n+1) ,0 <= n < N
(6) D.n = 〈↑ i : 1 <= i <= n ∧ AQ.i.n : n-i 〉 ,1 <= n <= N
(7) D.1 = 1
(8) D.(n+1) = (1+D.n)↑0 ⇐ Q.(f.n) ,0 <= n < N
(9) D.(n+1) = 0 ⇐ ¬(Q.(f.n)) ,0 <= n < N
以上都是公式化东西，本质上呢把上一章的+ f.n 变成 + 1 就从找最大区间和改成找最大区间长度了。
从后面的程序也能看出一二
n, r, d := 0, 0, 0
;do n≠N →
if Q.(f.n) → n. r. d := n+1, r ↑ (1+d)↑0, (1+d)↑0
[] ¬Q.(f.n) → n. r. d := n+1, r ↑ 0, 0
fi
odPair property
找有最长pair property的区间，比如f(n+1) >= f(n)递增序列。 写成general case就可以是具有P(f.n,f.(n+1))性质的数列
Pre f[0..N)
Post r = 〈↑ i, j : 0 <= i <= j <= N-1 ∧ APP.i.j : j-i 〉+ 1
//这里为什么要用1到N的区间，最后再+1呢？
//首先我们要检查所有的pair，而N个数共有N-1个pair。
//我们设定检查 pair 条件是（n,n+1），也就是说n为N-1时所有的数就都检查过了
//同理可得如果pair是(n-1,n)这么设定的，那么就要将区间改成[1,N]
//+1则是因为上面的出来的不过是符合设定的pair数量，也就是n数量，而区间长度则是n+1个，因此需要+1
(0) APP.i.j ≡ 〈∀ k : i <= k < j : PP.(f.(k)).(f.k+1)〉 ,0 <= i <= j <= N-1
(1) APP.i.i true
(2) APP.i.(j+1) ≡ AQ.i.l ∧ PP.(f.(j)).(f.j+1)) ,0 <= i <= j < N-1
(3) C.n = 〈 ↑ i, j : 0 ≤ i ≤ j ≤ n ∧ APP.i.j : j-i 〉 ,0 <= n <= N-1
(4) C.0 = 0
(5) C.(n+1) = C.n ↑ D.(n+1) ,0 <= n < N-1
(6) D.n = 〈↑ i : 0 ≤ i ≤ n ∧ APP.i.n: n-i 〉 ,0 <= n <= N-1
(7) D.0 = 0
(8) D.(n+1) = (1+D.n) ↑ 0 <= PP.(f.(n)).(f.n+1)) ,0 <= n < N-1
(9) D.(n+1) = 0 ⇐ PP.(f.(n)).(f.n+1)) ,0 <= n < N-1
以上也都是公式化东西，把找单点性质改成pair性质就行，区间变一变。
n, r, d := 0, 0, 0
;do n ≠ N-1 →
if PP.(f.(n-1)).(f.n) → n, r, d := n+1, r ↑ (1+d) ↑ 0, (1+d) ↑ 0
[] ¬PP.(f.(n-1)).(f.n) → n, r, d := n+1, r ↑ 0, 0
fi
od
r = r+1most property (One exception)
找一个区间大部分都是某个性质，最多只有一个点不满足。 比如找最多有一个零的，最长的区间。 那么这时候我们就需要引入新方程来解决这个问题了 找最长区间almost满足性质P
Pre f[0..N)
Post r = 〈↑ i, j : 0 <= i <= j <= N ∧ OP.i.j : j-i 〉 0 <= i <= j < N //OP = one property
Domain model:
(0) g.x = 1 <== P.x
(1) g.x = 0 <== ¬P.x
(2) OP.i.j = 〈+k : i<= k <j : g.(f.k)〉 <= 1 //计数，区间内不满足条件的点最多为1
(3) OP.i.i
(4) OP.i.(j+1) = OP.i.j <== ¬P.(f.j) 0 <= i <= j < N
(5) OP.i.(j+1) = NP.i.j <== P.(f.j) 0 <= i <= j < N // NP = no property
(6) NP.i.j = 〈+k : i<= k <j : g.(f.k)〉 <= 0
(7) NP.i.i
(8) NP.i.(j+1) = NP.i.j <== ¬P.(f.j) 0 <= i <= j < N
(9) NP.i.(j+1) = false <== P.(f.j) 0 <= i <= j < N
(10) C.n = 〈↑ i, j : 0 <= i <= j <= N ∧ OP.i.j : j-i 〉 0 <= n <= N
(11) C.0 = 0
(12) C.(n+1) = C.n ↑ 〈↑ i : 0 ≤ i ≤ n+1 ∧ OP.i.(n+1) : (n+1)-i = C.n ↑ D.(n+1)
(13) D.n = 〈↑ i : 0 ≤ i ≤ n ∧ OP.i.n : n-i 〉 0 ≤ n ≤ N
(14) D.0 = 0
(15) D.(n+1) = (1+D.n)↑0 ⇐ ¬P.(f.n) ,0 ≤ n < N
(16) D.(n+1) = (1 + 〈↑ i : 0 ≤ i ≤ n ∧ NP.i.n : n-i 〉) ↑ 0 = (1+E.n)↑0 ⇐ P.(f.n) ,0 ≤ n < N
(17) E.n = 〈↑ i : 0 ≤ i ≤ n ∧ NP.i.n : n-i 〉 ,0 ≤ n ≤ N
(18) E.0 = 0
(19) E.(n+1) = (1+E.n)↑0 ⇐ ¬P.(f.n) ,0 ≤ n < N
(20) E.(n+1) = 0 ⇐ P.(f.n) ,0 ≤ n < N
现在我们终于列完了domin model
Post: r = C.n ∧ n = N
Invar:
P0: r = C.n and d = D.n and e = E.n
P1: 0<= n <= N
Guard n != N
vf N-n
Loop body:
n,r,d,e -> n+1, R,D,E
C.n+1, D.n+1, E.n+1
Case ¬P.(f.n)
C.n ↑ D.(n+1), (1+D.n)↑0,(1+E.n)↑0
C.n ↑ (1+D.n)↑0, (1+D.n)↑0,(1+E.n)↑0
Case P.(f.n)
C.n ↑ (1+E.n)↑0, (1+E.n)↑0, 0
n, r, d, e := 0, 0, 0, 0
;do n≠N →
if ¬P.(f.n) → n. r. d, e := n+1, r ↑ (1+d)↑0, (1+d)↑0, (1+e)↑0
[] P.(f.n) → n. r. d, e := n+1, r↑(1+e) ↑0, (1+e) ↑0, 0
fi
odRecursion
这一周的主题是recursion， 也就是如何将递归转化为循环。 首先老师用fibonacci数列引入线性组合(Linear combination)作为一个常见的invariant。
选取invariant的原则
它在一开始很好保持true 在最终能达成postcondition 在 vf 变化的过程中也很好保持true
P0 : α * fib.n + β * fib.(n+1) = fib.N 这个式子看起来很怪：为什么fib.N能用这个式子表述？作为不变量这个式子是怎么在程序中保持关系的？ 这个式子的核心思想是：通过展开fib.N来获取最终的式子,展开的同时保持等式成立，这样右边的就是原式，等号左边的就是我们展开出来的式子。 根据 fibonacci 数列的性质我们可以得到fib.N 和它自己展开的两个子式的关系，也就是 fib(N-1) + fib(N-2),那么当我们继续一层一层的向下展开(n -> n - 1)的时候，我们就需要变量来记录子问题怎么组合回原问题.因为 fibonacci 数列的形式，当前值完全依赖于前两个数值，因此我们可以简单的用 α 和 β 记录关系。
实际上线性组合的几个新加的参数都是累加器，记录不同变量的变化。如果递归式会展开出常数就加一个γ作为常数的累加器。我们后面也会遇到。
接下来我们观察当n降到0之后会发生什么？ n := 0 -> α * 0 + β*1 得出当循环过完之后 beta 是最终的解。 观察循环体，发现可以用 n!=0 作为guard, n自身就是变量，也就是vf，我们要通过一个下降的循环来最终计算出fib(N) Guard： n != 0 vf: n 接下来计算loop body 将n设为n-1时，可以简单的利用fibonacci数列的性质来转化α和β
还有一种例子就是fusc function(这个方程由Dijkstra命名)
(0) fusc.0 = 0
(1) fusc.1 = 1
(2) fusc.(2*n) = fusc.n , 0 < n
(3) fusc.(2*n+1) = fusc.n + fusc.(n+1) , 0 < n
有点像是fibonacci数列的推广。
我们首先也还是将它设为α * f.n + β * f.(n+1) = f.N
P0 = α * f.n + β * f.(n+1) = f.N
首先我们可以开始分类讨论了，也就是当n为偶数时，那么此时可以将n表示为2p
此时α * f.n + β * f.(n+1) = f.N -> α * f.p + β * f.(2p+1) = f.N
-> α * f.p + β \*( f.p+f.(p+1)) = f.N
简单合并可得
if even.n → n, α, β := n div 2(p), α + β, β
分析odd case，
α * f.n + β * f.(n+1) = f.N -> α\*(fusc.p + fusc.(p+1)) + β\*fusc.(p+1)
简单合并可得
if odd.n → n, α, β := (n-1) div 2, α , α + β
这样我们就能用一个简单的程序算出值，且复杂度为logn
if N = 0 → r := 0
[] N = 1 → r := 1
[] N > 1 → n, α, β := N, 1, 0 {P0 ∧ P1} ;
do n ≠ 1 →
if even.n → n, α, β := n div 2, α + β, β
[] odd.n → n, α, β := (n-1) div 2, α , α + β
fi
od ;
r := α + β
fi最后是一个简单的递归程序转循环的general case： (0) f.n = c.n <= ¬b.n (1) f.n = h.n ⊕ f.(g.n) <= b.n
对于所有在满足条件b下进行一些操作(结束)，不满足b的情况下进行另一种操作的递归式 （比如 n !=0 ->
h.n代表是递归式对每一个需要计算的节点进行的操作。 f.(g.n)代表下一个递归出的子问题，其中g.n一般是下降式的,比如-，/，%等等, 我们将下一个需要计算的值传入给f，进行下一步计算。而所有最终所有计算出的结果会用连接符⊕ 连接，得出最终结果。
在将这种递归程序转换为循环的时候，我们可以简单的引入一个变量 r 来提前累加(可以不是加，任意binary combinator⊕都行)所有的h.n，这样我们就能消除递归深度，优化为循环。 因此简单的设立invariant为 P0: r⊕f.n = f.N Guard 需要通过P0 and
这样最终程序就是 do b.n -> n,r := g.n, r⊕h.n od r ⊕ c.n
记住最后要加上最终符合条件b.n的那c.n
那么按照老师的说法，本学期的内容就这样完结了，可喜可贺。
[!重要内容] Post condition 需要是一个boolean expression, 因此如果最后计算得出一个int, 那就需要一个赋值的过程.
EX1: Binary Chop revisit
对于之前的BC来说，我们缺乏一个捕获缺失的工具，也就是说只有当找到那个i之后确定它不存在，之后才能确定整体不存在这个解。 足够使用但是不够优雅。
因此我们可以拓展数组来将“不存在解”囊括到我们的解集中。通过在原数组中添加-1 和 N 位置。如果最后找到的解落在了这两个位置上代表数组中没有。这给我们一个很简单的，在程序范围内判断有无解的方法。