CS计算机代考程序代写 state space state prestate poststate

state space state prestate poststate
addresses state variables
memory int; (0,..20); char; rat memory contents –2; 15; “A”; 3.14
initialstate finalstate
low level
high level initialvalues
finalvalues
σ = σ0;σ1;σ2;σ3 = i; n; c; x
σʹ = σʹ0;σʹ1;σʹ2;σʹ3 = iʹ; nʹ; cʹ; xʹ
0 , 1 , 2 , 3 i , n , c , x
i, n, c, x iʹ, nʹ, cʹ, xʹ
Specification
For now: prestate, poststate
Later: time (termination = finite time), space, interaction, communication, …
1/64

Specification
specification of computer behavior: a boolean expression in variables σ and σʹ
We provide a prestate as input.
A computation satisfies a specification by computing a satisfactory poststate as output. The given prestate and computed poststate must make the specification true.
2/64

Specification
specification of computer behavior: a boolean expression
in the initial values x , y , … and final values xʹ , yʹ , … of some state variables
We provide initial values as input.
A computation satisfies a specification by computing satisfactory final values as output. The given initial values and computed final values must make the specification true.
3/64

Specification Specification S is unsatisfiable for prestate σ :
Specification S is satisfiable for prestate σ : Specification S is deterministic for prestate σ : Specification S is nondeterministic for prestate σ :
Specification S is satisfiable for prestate σ : Specification S is implementable:
¢(§σʹ· S) < 1 ¢(§σʹ· S) ≥ 1 ¢(§σʹ· S) ≤ 1 ¢(§σʹ· S) > 1
∃σʹ· S
∀σ· ∃σʹ· S
4/64

examples
xʹ = x+1 ∧ yʹ = y xʹ > x
⊤
⊥
implementable, deterministic implementable, nondeterministic implementable, extremely nondeterministic unimplementable, overly deterministic unimplementable, overly deterministic implementable, nondeterministic
x≥0 ∧ yʹ=0 x≥0 ⇒ yʹ=0
ok x:= e
= =
σʹ=σ
σʹ = σ⊲address “x”⊳e
= xʹ=x ∧ yʹ=y ∧ …
= xʹ=e ∧ yʹ=y ∧ …
= xʹ=x+1 ∧ yʹ=y
x:= x+y
if x=y then x:= x+1 else xʹ+yʹ = 3 fi
Specification
5/64

dependent composition
S. R = ∃xʹʹ, yʹʹ, …· (substitute xʹʹ, yʹʹ, … for xʹ, yʹ, … in S ) ∧ (substitute xʹʹ, yʹʹ, … for x, y, … in R )
In integer variable x
xʹ=x ∨ xʹ=x+1 . xʹ=x ∨ xʹ=x+1
= ∃xʹʹ· (xʹʹ=x ∨ xʹʹ=x+1) ∧ (xʹ=xʹʹ ∨ xʹ=xʹʹ+1)
= ∃xʹʹ· xʹʹ=x ∧ xʹ=xʹʹ ∨ xʹʹ=x+1 ∧ xʹ=xʹʹ
∨ xʹʹ=x ∧ xʹ=xʹʹ+1 ∨ xʹʹ=x+1 ∧ xʹ=xʹʹ+1
= (∃xʹʹ· xʹʹ=x ∧ xʹ=xʹʹ) ∨ (∃xʹʹ· xʹʹ=x+1 ∧ xʹ=xʹʹ)
∨ (∃xʹʹ· xʹʹ=x ∧ xʹ=xʹʹ+1) ∨ (∃xʹʹ· xʹʹ=x+1 ∧ xʹ=xʹʹ+1)
= xʹ=x ∨ xʹ=x+1 ∨ xʹ=x+2
distribute ∧ over ∨ distribute ∃ over ∨
One-Point Law 4 times
6/64

dependent composition
S. R = ∃xʹʹ, yʹʹ, …· (substitute xʹʹ, yʹʹ, … for xʹ, yʹ, … in S ) ∧ (substitute xʹʹ, yʹʹ, … for x, y, … in R )
In integer variable x
xʹ=x ∨ xʹ=x+1 . xʹ=x ∨ xʹ=x+1
x x􏱆 x x􏱆 x x􏱆􏱆 x􏱆 x x􏱆
0000 00000
1111 11111
2 2 . 2 2 = 􏲔x􏱆􏱆· 2 2 2 = 2 2
3333 33333
::: :444 :44:4
::: ::5:55
::: :::
7/64

dependent composition
S. R = ∃xʹʹ, yʹʹ, …·
∧
In integer variables x and y x:= 3. y:= x+y
(substitute xʹʹ, yʹʹ, … for xʹ, yʹ, … in S ) (substitute xʹʹ, yʹʹ, … for x, y, … in R )
= xʹ=3 ∧ yʹ=y. xʹ=x ∧ yʹ=x+y then eliminate dependent composition
= ∃xʹʹ, yʹʹ: int· xʹʹ=3 ∧ yʹʹ=y ∧ xʹ=xʹʹ ∧ yʹ=xʹʹ+yʹʹ use One-Point Law twice
= xʹ=3 ∧ yʹ = 3+y
eliminate assignments first
8/64

specification laws
ok. P = P. ok = P
P. (Q. R) = (P. Q). R
ifbthenPelsePfi = P
ifbthenPelseQfi = if¬bthenQelsePfi
P = if b then b ⇒ P else ¬b ⇒ P fi ifbthenSelseRfi = b∧S∨¬b∧Rfi
if b then S else R fi = (b⇒S) ∧ (¬b⇒R)
P∨Q. R∨S = (P. R) ∨ (P. S) ∨ (Q. R) ∨ (Q. S) ifbthenPelseQfi∧R = ifbthenP∧RelseQ∧Rfi ifbthenPelseQfi.R = ifbthenP.RelseQ.Rfi x:= if b then e else f fi = if b then x:= e else x:= f fi x:= e. P = (for x substitute e in P )
Identity Law
Associative Law IdempotentLaw CaseReversalLaw
Case Creation Law CaseAnalysisLaw
Case Analysis Law Distributive Law DistributiveLaw DistributiveLaw Functional-Imperative Law Substitution Law
9/64

substitution law
x:=e.P = (for x substitute e in P)
x:=y+1. yʹ>xʹ = yʹ>xʹ
x:=x+1. yʹ>x∧xʹ>x = yʹ>x+1 ∧ xʹ>x+1
x:= y+1. yʹ = 2×x = yʹ = 2×(y+1)
x:= 1. x≥1 ⇒ ∃x· yʹ = 2×x = 1≥1 ⇒ ∃x· yʹ = 2×x = even yʹ x:=y. x≥1⇒∃y· yʹ=x×y = x:=y. x≥1⇒∃k· yʹ=x×k
= y≥1⇒∃k· yʹ=y×k x:= 1. ok = x:= 1. xʹ=x ∧ yʹ=y = xʹ=1 ∧ yʹ=y
x:= 1. y:= 2 = x:= 1. xʹ=x ∧ yʹ=2 = xʹ=1 ∧ yʹ=2
10/64

substitution law
x:=e.P = (for x substitute e in P) x:= 1. y:= 2. x:= x+y
= x:= 1. y:= 2. xʹ = x+y ∧ yʹ=y
= x:= 1. xʹ = x+2 ∧ yʹ=2
= xʹ=3 ∧ yʹ=2
x:= 1. xʹ > x. xʹ = x+1
= xʹ > 1. xʹ = x+1
= ∃xʹʹ, yʹʹ· xʹʹ>1 ∧ xʹ = xʹʹ+1
= ∃xʹʹ· xʹʹ>1 ∧ xʹ = xʹʹ+1
= ∃xʹʹ· xʹʹ>1 ∧ xʹʹ = xʹ–1
= xʹ–1 >1
= xʹ>2
11/64

Refinement
Specification P (the problem) is refined by specification S (the solution)
if and only if P is satisfied whenever S is satisfied. ∀σ, σʹ· P⇐S
xʹ>x ⇐ xʹ=x+1 ∧ yʹ=y = x:= x+1
xʹ≤x ⇐ ifx=0thenxʹ=xelsexʹyʹ>x ⇐ y:= x+1. x:= y+1
= y:= x+1. xʹ=y+1 ∧ yʹ=y
= xʹ=x+2 ∧ yʹ=x+1
12/64

condition: specification that refers to (at most) one state
initial condition, precondition: refers to (at most) the initial state (prestate)
final condition, postcondition: refers to (at most) the final state (poststate)
exact precondition for P to be refined by S : ∀σʹ· P⇐S
exact postcondition for P to be refined by S : ∀σ· P⇐S sufficient ⇒ exact ⇒ necessary
13/64

(the exact precondition for xʹ>5 to be refined by x:= x+1 )
= ∀xʹ· xʹ>5 ⇐ (x:= x+1)
= ∀xʹ· xʹ>5 ⇐ xʹ=x+1
= x+1 > 5
= x> 4
x>4 ⇒ xʹ>5 ⇐ x:= x+1
one-point laws
∃v·v=e∧P = (replace v with e in P) ∀v·v=e⇒P = (replace v with e in P)
One-Point Law
14/64

(the exact postcondition for x>4 to be refined by x:= x+1 )
= ∀x· x>4 ⇐ (x:= x+1)
= ∀x· x>4 ⇐ xʹ=x+1
= ∀x· x>4 ⇐ x=xʹ–1
= xʹ–1 > 4
= xʹ > 5
xʹ>5 ⇒ x>4 ⇐ x:= x+1
x≤4 ⇒ xʹ≤5 ⇐ x:= x+1
contrapositive law
a⇒b = ¬b⇒¬a
One-Point Law
15/64

condition laws
C∧(P.Q) ⇐ C∧P.Q C⇒(P.Q) ⇐ C⇒P.Q (P.Q) ∧ Cʹ ⇐ P. Q∧Cʹ (P.Q) ⇐ Cʹ ⇐ P. Q⇐Cʹ P. C∧Q ⇐ P∧Cʹ. Q
P. Q ⇐ P∧Cʹ. C⇒Q precondition law
C is a sufficient precondition for P to be refined by S if and only if C⇒P is refined by S .
postcondition law
Cʹ is a sufficient postcondition for P to be refined by S if and only if Cʹ⇒P is refined by S .
16/64

A program is an implemented specification.
ok
x:= e
if b then P else Q fi P.Q
binaries, numbers, characters bunches, sets, strings, lists NOT functions, quantifiers
An implementable specification that is refined by a program is a program.
Recursion is allowed.
x≥0⇒xʹ=0 ⇐ ifx=0thenokelsex:=x–1. x≥0⇒xʹ=0fi
17/64

refinement by steps
If A ⇐ ifbthenCelseDfi and C⇐E and D⇐F, then A ⇐ ifbthenEelseFfi.
If A ⇐ B.C and B ⇐ D and C ⇐ E , then A ⇐ D.E . If A ⇐ B and B ⇐ C , then A ⇐ C .
refinement by parts
If A ⇐ ifbthenCelseDfi and E ⇐ ifbthenFelseGfi, then A∧E ⇐ ifbthenC∧FelseD∧Gfi .
If A ⇐ B.C and D ⇐ E.F , then A∧D ⇐ B∧E. C∧F . If A ⇐ B and C ⇐ D , then A∧C ⇐ B∧D .
refinement by cases
P ⇐ ifbthenQelseRfi
if and only if P ⇐ b ∧ Q and P ⇐ ¬b ∧ R
18/64

List Summation
List of numbers L ; number variable s .
sʹ = ΣL ⇐ s:= 0. n:= 0. sʹ = s + Σ L [n;..#L]
sʹ=s+ΣL[n;..#L] ⇐
ifn=#Lthenn=#L ⇒ sʹ=s+ΣL[n;..#L] elsen #L ⇒ sʹ=s+ΣL[n;..#L]fi
n=#L ⇒ sʹ=s+ΣL[n;..#L] ⇐ ok
n⧧#L ⇒ sʹ=s+ΣL[n;..#L] ⇐ s:=s+Ln. n:=n+1. sʹ=s+ΣL[n;..#L]
19/64

A⇐ B ⇐ C ⇐ D ⇐
s:= 0. n:= 0. B ifn=#LthenCelseDfi
ok
s:=s+Ln. n:=n+1. B
Refinement by Steps = in-line macro-expansion
B ⇐ ifn=#Lthenokelses:=s+Ln. n:=n+1. Bfi
translation
void A(void) {s = 0; n = 0; B( );}
void B(void) {if (n==sizeof(L)/sizeof(L[0])); else {s+=L[n]; n++; B( );}}
s = 0; n = 0;
B: if (n==sizeof(L)/sizeof(L[0])); else {s+=L[n]; n++; goto B;}
compilation
20/64

Binary Exponentiation
Given natural variables x and y , write a program for yʹ = 2x . yʹ=2x ⇐ if x=0 then x=0 ⇒ yʹ=2x else x>0 ⇒ yʹ=2x fi
x=0 ⇒ yʹ=2x ⇐ y:= 1. x:= 3
x>0 ⇒ yʹ=2x ⇐ x>0 ⇒ yʹ=2x–1. yʹ=2×y x>0 ⇒ yʹ=2x–1 ⇐ xʹ=x–1. yʹ=2x
yʹ=2×y ⇐ y:= 2×y. x:= 5
xʹ=x–1 ⇐ x:= x–1. y:= 7
21/64

A ⇐
B ⇐
C ⇐
D ⇐
E ⇐
F ⇐
A ⇐
ifx=0thenBelseCfi y:= 1. x:= 3
D. E F. A
y:= 2×y. x:= 5 x:= x–1. y:= 7
if x=0 then y:= 1. x:= 3 else x:= x–1.
y:= 7.
A. y:= 2×y.
x:= 5 fi
Binary Exponentiation
Given natural variables x and y , write a program for yʹ = 2x .
int x, y;
void A (void) {if (x==0) {y = 1; x = 3;} else {x = x–1; y = 7; A( ); y = 2*y; x = 5;}} x = 5; A( ); printf (“%i”, y);
22/64

σ = t;x;y;…
state = time variable; memory variables
t is the time at which execution starts
tʹ is the time at which execution ends
extended natural or extended nonnegative real
Specification S is implementable if and only if ∀σ· ∃σʹ· S ∧ tʹ≥t
Time
23/64

t:= t+(the time to evaluate and store e ). t:= t+(the time to evaluate b and branch). t:= t+(the time for the call and return).
tʹ = t + f σ tʹ ≤ t + f σ tʹ ≥ t + f σ
x:= e
if b then P else Q fi P
real time
24/64

P
⇐ t:=t+1. ifx=0thenokelse t:=t+1. x:=x–1.t:=t+1. Pfi is a theorem when
= xʹ=0
= ifx≥0thentʹ=t+3×x+1elsetʹ=∞fi
= ifx≥0thenxʹ=0∧tʹ=t+3×x+1elsetʹ=∞fi = xʹ=0 ∧ if x≥0 then tʹ=t+3×x+1 else tʹ=∞ fi
P P P P
real time
25/64

• •
P
P P P P
Each recursive call costs time 1. All else is free.
⇐ ifx=0thenokelsex:=x–1. t:=t+1. Pfi is a theorem when
= xʹ=0
= if x≥0 then tʹ=t+x else tʹ=∞ fi
= if x≥0 then xʹ=0 ∧ tʹ=t+x else tʹ=∞ fi = xʹ=0 ∧ if x≥0 then tʹ=t+x else tʹ=∞ fi
recursive time
Recursion can be direct or indirect.
In every loop of calls, there must be a time increment of at least one time unit.
26/64

Prove R ⇐ ifx=1thenokelsex:=divx2. t:=t+1. Rfi where R= xʹ=1 ∧ if x≥1 then tʹ ≤ t + log x else tʹ=∞ fi
= xʹ=1 ∧ (x≥1 ⇒ tʹ ≤ t + log x) ∧ (x<1 ⇒ tʹ=∞) use Refinement by Parts; prove: xʹ=1 ⇐ ifx=1thenokelsex:=divx2. t:=t+1. xʹ=1fi x≥1 ⇒ tʹ ≤ t + log x ⇐ if x=1 then ok else x:= div x 2. t:= t+1. x≥1 ⇒ tʹ ≤ t + log x fi x<1 ⇒ tʹ=∞ ⇐ ifx=1thenokelsex:=divx2. t:=t+1. x<1⇒tʹ=∞fi 27/64 Prove R ⇐ ifx=1thenokelsex:=divx2. t:=t+1. Rfi where R= xʹ=1 ∧ if x≥1 then tʹ ≤ t + log x else tʹ=∞ fi = xʹ=1 ∧ (x≥1 ⇒ tʹ ≤ t + log x) ∧ (x<1 ⇒ tʹ=∞) use Refinement by Parts and Cases; prove: xʹ=1 ⇐ x=1 ∧ ok xʹ=1 ⇐ x⧧1 ∧ (x:= div x 2. t:= t+1. xʹ=1) x≥1 ⇒ tʹ ≤ t + log x ⇐ x=1 ∧ ok x≥1 ⇒ tʹ ≤ t + log x ⇐ x⧧1 ∧ (x:= div x 2. t:= t+1. x≥1 ⇒ tʹ ≤ t + log x) x<1 ⇒ tʹ=∞ ⇐ x=1∧ok x<1 ⇒ tʹ=∞ ⇐ x⧧1∧(x:=divx2. t:=t+1. x<1⇒tʹ=∞) 28/64 (x≥1 ⇒ tʹ ≤ t + log x ⇐ x=1 ∧ xʹ=x ∧ tʹ=t) = (1≥1 ⇒ t ≤t+log1 ⇐ x=1∧xʹ=x∧tʹ=t) = ( ⊤ ⇐ x=1 ∧ xʹ=x ∧ tʹ=t) =⊤ context x=1 and tʹ=t simplify base law 29/64 = x⧧1 = x>1
= x>1
= x>1
⇐ x>1 = x>1
∧ (div x 2 ≥ 1 ⇒ tʹ ≤ t + 1 + log (div x 2)) ∧ x≥1 ⇒ ∧ (x>1 ⇒ tʹ ≤ t + 1 + log (div x 2)) ⇒ tʹ ≤ t + log x
∧ tʹ ≤ t + 1 + log (div x 2) ⇒ tʹ ≤ t + log x ⇒ (tʹ ≤ t + 1 + log (div x 2) ⇒ tʹ ≤ t + log x)
⇒ t + 1 + log (div x 2) ≤ t + log x ⇒ log (div x 2) ≤ log x – 1
tʹ ≤ t + log x
discharge
(x≥1 ⇒ tʹ ≤ t + log x ⇐ x⧧1 ∧ (div x 2 ≥ 1 ⇒ tʹ ≤ t + 1 + log (div x 2))) portation
= x>1
⇐ div x 2 ≤ x/2
subtract t+1 from each side property of log
log is monotonic for x>0
=⊤
⇒ log (div x 2) ≤ log (x/2)
portation Connection Law tʹ≤a ⇒ tʹ≤b ⇐ a≤b
simplify
30/64

(x<1 ⇒ tʹ=∞ ⇐ x=1 ∧ xʹ=x ∧ tʹ=t) = x<1 ∧ x=1 ∧ xʹ=x ∧ tʹ=t ⇒ tʹ=∞ = ⊥ ⇒ tʹ=∞ =⊤ portation generic, base base 31/64 (x<1 ⇒ tʹ=∞ ⇐ x⧧1 ∧ (div x 2 < 1 ⇒ tʹ=∞)) portation = x<1 ∧ x⧧1 ∧ (div x 2 < 1 ⇒ tʹ=∞) = x<1 ∧ tʹ=∞ ⇒ tʹ=∞ =⊤ ⇒ tʹ=∞ discharge specialization 32/64 xʹ=2 ⇐ t:= t+1. xʹ=2 complain only if xʹ⧧2 xʹ=2 ∧ tʹ<∞ unimplementable xʹ=2 ∧ (t<∞ ⇒ tʹ<∞) ⇐ t:= t+1. xʹ=2 ∧ (t<∞ ⇒ tʹ<∞) complain only if xʹ⧧2 ∨ t<∞ ∧ tʹ=∞ xʹ=2 ∧ tʹ≤t+1 ⇐ t:= t+1. xʹ=2 ∧ tʹ≤t+1 ✗ xʹ=2 ∧ tʹ≤t+1 ⇐ x:= 2 Termination 33/64 Linear Search Find the first occurrence of item x in list L . The execution time must be linear in #L . ¬ x: L (0,..hʹ) ∧ (Lhʹ=x ∨ hʹ=#L) [ ? ; ? ; ? ; ? ; x ; ? ; ? ; ? ; ?] ↑↑↑ 0← x is not in this part→hʹ #L 34/64 Linear Search Find the first occurrence of item x in list L . The execution time must be linear in #L . ¬ x: L (0,..hʹ) ∧ (Lhʹ=x ∨ hʹ=#L) ⇐ h:= 0. h≤#L ⇒ ¬ x: L (h,..hʹ) ∧ (Lhʹ=x ∨ hʹ=#L) h≤#L ⇒ ¬ x: L (h,..hʹ) ∧ (Lhʹ=x ∨ hʹ=#L) ⇐ if h=#L then ok else h<#L ⇒ ¬ x: L (h,..hʹ) ∧ (Lhʹ=x ∨ hʹ=#L) fi h<#L ⇒ ¬ x: L (h,..hʹ) ∧ (Lhʹ=x ∨ hʹ=#L) ⇐ if Lh=x then ok else h:= h+1. h≤#L ⇒ ¬ x: L (h,..hʹ) ∧ (Lhʹ=x ∨ hʹ=#L) fi 35/64 Linear Search timing tʹ ≤ t+#L ⇐ h:= 0. h≤#L ⇒ tʹ ≤ t+#L–h h≤#L ⇒ tʹ≤t+#L–h ⇐ ifh=#Lthenokelseh<#L ⇒ tʹ≤t+#L–hfi h<#L ⇒ tʹ≤t+#L–h ⇐ ifLh=xthenokelseh:=h+1. t:=t+1. h≤#L ⇒ tʹ≤t+#L–hfi h:= h+1. t:= t+1. h≤#L ⇒ tʹ ≤ t+#L–h = h:= h+1. h≤#L ⇒ tʹ ≤ t+1+#L–h = h+1≤#L ⇒ tʹ ≤ t+1+#L–h–1 = h<#L ⇒ tʹ ≤ t+#L–h substitution law substitution law simplify 36/64 Linear Search Find the first occurrence of item x in list L . The execution time must be linear in #L . nonempty ¬ x: L (0,..hʹ) ∧ (Lhʹ=x ∨ hʹ=#L) ⇐ h:= 0. h≤#L ⇒ ¬ x: L (h,..hʹ) ∧ (Lhʹ=x ∨ hʹ=#L) < h≤#L ⇒ ¬ x: L (h,..hʹ) ∧ (Lhʹ=x ∨ hʹ=#L) ⇐ if h=#L then ok else h<#L ⇒ ¬ x: L (h,..hʹ) ∧ (Lhʹ=x ∨ hʹ=#L) fi h<#L ⇒ ¬ x: L (h,..hʹ) ∧ (Lhʹ=x ∨ hʹ=#L) ⇐ if Lh=x then ok else h:= h+1. h≤#L ⇒ ¬ x: L (h,..hʹ) ∧ (Lhʹ=x ∨ hʹ=#L) fi 37/64 Find an occurrence of item x in nonempty sorted list L . The execution time must be logarithmic in #L . (x: L (0,..#L) = h0⇒zʹ=z×xy fi
Proof:
=
⇒
=
⇒
y=0 ∧ok
y=0 ∧ xʹ=x ∧ yʹ=y ∧ zʹ=z
y=0 ∧ zʹ = z×1 y=0 ∧ zʹ = z×x0
zʹ= z×xy
expand ok specialize, 1 is identity for ×
x0=1 context y=0 and specialize
Fast Exponentiation
Given rational variables x and z and natural variable y , write a program for zʹ = xy that runs fast without using exponentiation.
zʹ=xy ⇐ z:= 1. zʹ = z×xy
42/64

Fast Exponentiation
Given rational variables x and z and natural variable y , write a program for zʹ = xy that runs fast without using exponentiation.
zʹ=xy ⇐ z:= 1. zʹ = z×xy
zʹ=z×xy ⇐ ify=0thenokelsey>0⇒zʹ=z×xy fi
y>0⇒zʹ=z×xy ⇐ z:=z×x. y:=y–1. zʹ=z×xy
Proof: (y>0 ⇒ zʹ = z×xy ⇐ z:= z×x. y:= y–1. zʹ = z×xy)
= zʹ = z×xy ⇐ y>0 ∧ (z:= z×x. y:= y–1. zʹ = z×xy)
= zʹ = z×xy ⇐ y>0 ∧ zʹ = z×x×xy–1
= zʹ = z×xy ⇐ y>0 ∧ zʹ = z×xy
=⊤
portation Substitution Law twice Law of Exponents specialize
43/64

Fast Exponentiation
Given rational variables x and z and natural variable y , write a program for zʹ = xy that runs fast without using exponentiation.
zʹ=xy ⇐ z:= 1. zʹ = z×xy
zʹ=z×xy ⇐ ify=0thenokelsey>0⇒zʹ=z×xy fi
y>0⇒zʹ=z×xy ⇐ z:=z×x. y:=y–1. zʹ=z×xy
if even y then even y ∧ y>0 ⇒ zʹ = z×xy else odd y ⇒ zʹ = z×xy fi
even y ∧ y>0 ⇒ zʹ = z×xy ⇐ x:= x×x. y:= y/2. zʹ = z×xy
Proof: (even y ∧ y>0 ⇒ zʹ = z×xy ⇐ x:= x×x. y:= y/2. zʹ = z×xy)
= zʹ = z×xy ⇐ even y ∧ y>0 ∧ (x:= x×x. y:= y/2. zʹ = z×xy)
= zʹ = z×xy ⇐ even y ∧ y>0 ∧ zʹ = z×(x×x)y/2
= zʹ = z×xy ⇐ even y ∧ y>0 ∧ zʹ = z×xy =⊤
portation
Substitution Law twice Law of Exponents specialize
44/64

Fast Exponentiation
Given rational variables x and z and natural variable y , write a program for zʹ = xy that runs fast without using exponentiation.
zʹ=xy ⇐ z:= 1. zʹ = z×xy
zʹ=z×xy ⇐ ify=0thenokelsey>0⇒zʹ=z×xy fi
y>0⇒zʹ=z×xy ⇐ z:=z×x. y:=y–1. zʹ=z×xy
if even y then even y ∧ y>0 ⇒ zʹ = z×xy else odd y ⇒ zʹ = z×xy fi
even y ∧ y>0 ⇒ zʹ = z×xy ⇐ x:= x×x. y:= y/2. zʹ = z×xy odd y ⇒ zʹ = z×xy ⇐ z:= z×x. y:= y–1. zʹ = z×xy
45/64

Fast Exponentiation
Given rational variables x and z and natural variable y , write a program for zʹ = xy that runs fast without using exponentiation.
zʹ=xy ⇐ z:= 1. zʹ = z×xy
zʹ=z×xy ⇐ ify=0thenokelsey>0⇒zʹ=z×xy fi
y>0⇒zʹ=z×xy ⇐ z:=z×x. y:=y–1. zʹ=z×xy
if even y then even y ∧ y>0 ⇒ zʹ = z×xy else odd y ⇒ zʹ = z×xy fi
even y ∧ y>0 ⇒ zʹ = z×xy ⇐ x:= x×x. y:= y/2. zʹ = z×xy y>0 ⇒ zʹ = z×xy odd y ⇒ zʹ = z×xy ⇐ z:= z×x. y:= y–1. zʹ = z×xy
46/64

Fast Exponentiation
Given rational variables x and z and natural variable y , write a program for zʹ = xy that runs fast without using exponentiation.
zʹ=xy ⇐ z:= 1. zʹ = z×xy
zʹ=z×xy ⇐ ify=0thenokelsey>0⇒zʹ=z×xy fi
y>0⇒zʹ=z×xy ⇐ z:=z×x. y:=y–1. zʹ=z×xy
if even y then even y ∧ y>0 ⇒ zʹ = z×xy else odd y ⇒ zʹ = z×xy fi
even y ∧ y>0 ⇒ zʹ = z×xy ⇐ x:= x×x. y:= y/2. zʹ = z×xy y>0 ⇒ zʹ = z×xy
odd y ⇒ zʹ = z×xy ⇐ even y ⇒ zʹ = z×xy ⇐
z:= z×x. y:= y–1. zʹ = z×xy even y ⇒ zʹ = z×xy if y = 0 then ok else even y ∧ y>0 ⇒ zʹ = z×xy fi
47/64

Fast Exponentiation
Given rational variables x and z and natural variable y , write a program for zʹ = xy that runs fast without using exponentiation.
zʹ=xy ⇐ z:= 1. zʹ = z×xy
zʹ=z×xy ⇐ ify=0thenokelsey>0⇒zʹ=z×xy fi
if even y then even y ⇒ zʹ = z×xy else odd y ⇒ zʹ = z×xy fi y>0⇒zʹ=z×xy ⇐ z:=z×x. y:=y–1. zʹ=z×xy
if even y then even y ∧ y>0 ⇒ zʹ = z×xy else odd y ⇒ zʹ = z×xy fi even y ∧ y>0 ⇒ zʹ = z×xy ⇐ x:= x×x. y:= y/2. zʹ = z×xy y>0 ⇒ zʹ = z×xy
odd y ⇒ zʹ = z×xy ⇐ even y ⇒ zʹ = z×xy ⇐
z:= z×x. y:= y–1. zʹ = z×xy even y ⇒ zʹ = z×xy if y = 0 then ok else even y ∧ y>0 ⇒ zʹ = z×xy fi
48/64

even y ∧ y>0 ⇒ zʹ = z×xy ⇐ x:= x×x. y:= y/2. t:= t+1. y>0 ⇒ zʹ = z×xy
y =0123456789101112131415161718 tʹ–t = 0 0 1 1 2 2 2 2 3 3 3 3 3 3 3 3 4 4 4
49/64

even y ∧ y>0 ⇒ zʹ = z×xy ⇐ x:= x×x. y:= y/2. t:= t+1. y>0 ⇒ zʹ = z×xy
if y=0 then tʹ=t else tʹ = t + floor (log y) fi if y=0 then tʹ=t else tʹ ≤ t + log y fi
50/64

Fibonacci Numbers
fib0 = 0
fib1 = 1
fib (n+2) = fib n + fib (n+1)
fib = 0→0 | 1→1 | 〈n: nat+2 → fib(n–2) + fib(n–1)〉 fib = 〈n: nat → if n<2 then n else fib(n–2) + fib(n–1) fi〉 51/64 Fibonacci Numbers xʹ = fib n ⇐ xʹ = fib n ∧ yʹ = fib (n+1) = P P ⇐ if n=0 then x:= 0. y:= 1 else n:= n–1. P. we have these x y ↓↓ ... f f f f f f f f f f f f f f f f ... ↑↑ we want these xʹ yʹ xʹ=y ∧ yʹ=x+y fi 52/64 Fibonacci Numbers xʹ = fib n ⇐ xʹ = fib n ∧ yʹ = fib (n+1) = P P ⇐ if n=0 then x:= 0. y:= 1 else n:= n–1. P. xʹ=y ∧ yʹ=x+y fi xʹ=y ∧ yʹ=x+y ⇐ n:= x. x:= y. y:= n+y tʹ=t+n ⇐ if n=0 then x:= 0. y:= 1 else n:= n–1. t:= t+1. tʹ=t+n. tʹ=t fi tʹ=t ⇐ n:=x. x:=y. y:=n+y 53/64 Fibonacci Numbers fib(2×k+1) = (fib k)2 + (fib(k+1))2 fib(2×k+2) = 2 × fib k × fib(k+1) + (fib(k+1))2 P ⇐ if n=0 then x:= 0. y:= 1 else if even n then even n ∧ n>0 ⇒ P fi
else odd n ⇒ P fi
odd n ⇒ P ⇐ n:= (n–1)/2. P. xʹ = x2 + y2 ∧ yʹ = 2×x×y + y2
even n ∧ n>0 ⇒ P ⇐ n:= n/2 – 1. P. xʹ = 2×x×y + y2 ∧ yʹ = x2 + y2 + xʹ
xʹ = x2 + y2 ∧ yʹ = 2×x×y + y2 ⇐ n:= x. x:= x2 + y2. y:= 2×n×y + y2
xʹ = 2×x×y + y2 ∧ yʹ = x2 + y2 + xʹ ⇐ n:= x. x:= 2×x×y + y2. y:= n2 + y2 + x
54/64

Fibonacci Numbers
T = tʹ≤t+log(n+1)
T ⇐ if n=0 then x:= 0. y:= 1
else if even n then even n ∧ n>0 ⇒ T fi
else odd n ⇒ T fi
odd n ⇒ T ⇐ n:= (n–1)/2. t:= t+1. T. tʹ=t
even n ∧ n>0 ⇒ T ⇐ n:= n/2 – 1. t:= t+1. T. tʹ=t tʹ=t ⇐ n:= x. x:= x2 + y2. y:= 2×n×y + y2
tʹ=t ⇐ n:= x. x:= 2×x×y + y2. y:= n2 + y2 + x
55/64

Fibonacci Numbers
void P (void)
{ if (n==0) {x = 0; y = 1;}
else if (n%2==0) {n = n / 2 – 1; P(); n = x; x = 2*x*y + y*y; y = n*n + y*y + x;}
else {n = (n–1) / 2; P(); n = x; x = x*x + y*y; y = 2*n*y + y*y;} }
56/64

Towers of Hanoi
post A
post B
post C
disk disk
disk
57/64

Towers of Hanoi
MovePile from to using ⇐ if n=0 then ok
else n:= n–1.
MovePile from using to.
MoveDisk from to. MovePile using to from. n:= n+1 fi
58/64

Towers of Hanoi — time
t:= t + 2n – 1 ⇐ if n=0 then ok
else n:= n–1.
t:= t + 2n – 1.
t:= t+1.
t:= t + 2n – 1. n:= n+1 fi
59/64

Towers of Hanoi — space
sʹ=s ⇐
if n=0 then ok
else n:= n–1.
s:= s+1. sʹ=s. s:= s–1.
ok.
s:= s+1. sʹ=s. s:= s–1. n:= n+1 fi
60/64

Towers of Hanoi — maximum space
m≥s ⇒ (m:= max m (s+n)) ⇐ if n=0 then ok
else n:= n–1.
s:= s+1. m:= max m s. m≥s ⇒ (m:= max m (s+n)). s:= s–1. ok.
s:= s+1. m:= max m s. m≥s ⇒ (m:= max m (s+n)). s:= s–1. n:= n+1 fi
61/64

Towers of Hanoi — average space
p:= p + s×(2n – 1) + (n–2)×2n + 2 ⇐ if n=0 then ok
else n:= n–1.
s:= s+1. p:= p + s×(2n – 1) + (n–2)×2n + 2. s:= s–1. p:= p+s.
s:= s+1. p:= p + s×(2n – 1) + (n–2)×2n + 2. s:= s–1. n:= n+1 fi
space
s, sʹ
(n–2)×2n + 2
t tʹ
p
s×(2n – 1)
time
62/64

Towers of Hanoi — average space
p:= p + s×(2n – 1) + (n–2)×2n +2 ⇐ if n=0 then ok
else n:= n–1.
s:= s+1. p:= p + s×(2n – 1) + (n–2)×2n + 2. s:= s–1. p:= p+s.
s:= s+1. p:= p + s×(2n – 1) + (n–2)×2n + 2. s:= s–1. n:= n+1 fi
average space = ((n–2)×2n + 2) / (2n – 1) = n + n/(2n – 1) – 2
Easier: pʹ ≤ p + (s+n)×(2n–1) average space ≤ n
63/64

Towers of Hanoi
MovePile ⇐
if n=0 then ok
MovePile =
else
n:= n–1.
s:= s+1. m:= max m s. MovePile. s:= s–1. t:= t+1. p:= p+s. ok.
s:= s+1. m:= max m s. MovePile. s:= s–1. n:= n+1 fi
nʹ=n
∧ tʹ= t + 2n – 1
∧ sʹ=s
∧ (m≥s⇒mʹ=maxm(s+n))
∧ pʹ = p + s×(2n – 1) + (n–2)×2n + 2
64/64