Fibonacci-like 6步走

$(0) f.0 = e_0$

$(1) f.1 = e_1$

$(2) f.(n+2) = x*f.n + y*f.(n+1) + z, 0 ≤ n$

1. Choose invariants

P0: $𝛼*f.n + 𝛽*f.(n+1) +𝛾 = f.N$

P1: $0 ≤ n ≤ N$

2. Establish

3. Guard

we observe

	α*f.n + 𝛽*f.(n+1) + 𝛾 = f.N ∧ n = 0 
⇒		{ Leibniz } 
	α*f.0 + 𝛽*f.1 +𝛾 = f.N 
=		{(0)(1)} 
	α*e0 + 𝛽*e1 +𝛾 = f.N 

4. vf.

5. Loop body

​ $P0$

=

​ $\alpha* f(n) + \beta* f(n+1) + \gamma = f(N)$

= $\{\text{From } P1 \text{ and guard} \Rightarrow 1 \leq n, \text{ so } 2 \leq n+1\}$

​ $\alpha* f(n) + \beta*(x* f(n-1) + y* f(n) + z) + \gamma = f(N)$

= ${ \{*/+ \} }$

​ $\alpha* f(n) + \beta x* f(n-1) + \beta y* f(n) + \beta z + \gamma = f(N)$

= $\{\text{+ symmetric, */+}\}$

​ $\beta* x*f(n-1) + (\alpha + \beta y)* f(n) + \beta z + \gamma = f(N)$

= $\{\text{WP}\}$

​ $(n, \alpha, \beta, \gamma := n-1, \beta* x, \alpha + \beta *y, \beta *z + \gamma).P0$

6. Finished Algorithm.

n,𝛼,𝛽,𝛾 := N, 1, 0, 0
;do n ≠ 0 →
        n, 𝛼, 𝛽,𝛾 := n-1, 𝛽*x, 𝛼+𝛽*y, 𝛽*z  + 𝛾
od
;r:=𝛼*e0+𝛽*e1+𝛾 
{r=f.N}