\binom{n}{k} kiszámítása

Legyen X : vekt(N, N).

\begin{aligned}A : & N_{0} & × & N_{0} & × & X \\ & n & k & x \end{aligned}

\begin{aligned}B : & N_{0} & × & N_{0} \\ & n′ & k′ \end{aligned}

Q : (n = n′ ∧ k = k′ ∧ k ≤ n)
R : (Q ∧ x.hiv = \binom{n′}{k′})

A feladat megoldásához ciklust használunk a következő invariánssal:

P : (Q ∧ x.dom = n − k + 1 ∧ i ∈ [0..k] ∧ ∀j ∈ [x.lob..x.hib] : x[j] = \binom{j − x.lob + i}{i})

Könnyen látható, hogy

Q ⇒ P^{i,x←0,(1,<1_{1},1_{2},...,1_{n−k+1}>)} ⇔ lf(i, x := 0, (1, < 1_{1}, 1_{2}, ..., 1_{n−k+1} >); P ) Emiatt a keresett program a következő szekvencia lesz:

(i, x := 0, (1, < 1_{1}, 1_{2}, ..., 1_{n−k+1} >); DO)

ahol a DO ciklust kell alkalmasan megválasztani. 1. P ⇒ P nyilván teljesül.

2. P ∧ ¬π ⇒ R feltétel teljesíthető, ha ¬π : i ≥ k, hiszen x.hiv = \binom{x.hib−x.lob+k}{k} = \binom{n}{k}. Ennek megfelően

π : i < k

3. P ∧ π ⇒ t > 0 feltétel kielégíthető, ha

t : k − i Typeset by A_{M}S-TEX A t termináló függvény választása miatt keressük a ciklusmagot

S : (S_{1}; i := i + 1)

alakban.

5. ∀t_{0} ∈ Z : P ∧ π ∧ t ≤ t_{0} + 1 ⇒ lf(S; t ≤ t_{0}) feltétel teljesül, ha az i projekció az S_{1} programra nézve konstans függvény.

4. P ∧ π ⇒ lf(S; P ) feltétel kielégítéséhez elegendő, ha olyan S_{1} programot keresünk, amelyre

P ∧ π ⇒ lf(S_{1}; P^{i←i+1})

Keressük az S_{1} programot ciklus formában, amely invariánsa:

\overline{P} : (Q ∧ x.dom = n − k + 1 ∧ i + 1 ∈ [0..k] ∧ l ∈ [x.lob..x.hib]∧

∧ ∀j ∈ [x.lob..l] : x[j] = \binom{j − x.lob + (i + 1)}{i + 1}∧

∧ ∀j ∈ [l + 1..x.hib] : x[j] = \binom{j − x.lob + i}{i})

Könnyen látható, hogy

P ∧ π ⇒ \overline{P}^{l←1} ⇔ lf(l := 1; \overline{P} )

teljesül. Ezért S_{1}-et

S_{1} : (l := 1; \overline{DO})

alakban kell keresnünk.

1.a \overline{P} ⇒ \overline{P} nyilván teljesül. 2.a \overline{P} ∧ ¬\overline{π} ⇒ P^{i←i+1} feltétel teljesül, ahol P^{i←i+1} \overline{R}-nek felel meg, ha ¬\overline{π} : l ≥ x.hib

tehát, ha

\overline{π} : l < x.hib

3.a \overline{P} ∧ \overline{π} → \overline{t} > 0 teljesül,ha

\overline{t} : x.hib − l

A \overline{t} termináló függvény választása miatt keressük a ciklusmagot

\overline{S} : (\overline{S}_{1}; l := l + 1)

alakban.

5.a ∀\overline{t}_{0} ∈ Z : \overline{P} ∧ \overline{π} ∧ \overline{t} ≤ \overline{t}_{0} + 1 ⇒ lf(\overline{S}; \overline{t} ≤ \overline{t}_{0}) feltétel teljesül, ha az l projekció az \overline{S}_{1} programra nézve konstans függvény.

4.a \overline{P} ∧ \overline{π} ⇒ lf(\overline{S}; \overline{P} ) feltétel kielégítéséhez elegendő, ha olyan \overline{S}_{1} programot keresünk, amelyre

\overline{P} ∧ \overline{π} ⇒ lf(\overline{S}_{1}; \overline{P}^{l←l+1})

\overline{P} ∧ \overline{π} : (Q ∧ x.dom = n − k + 1 ∧ i + 1 ∈ [0..k] ∧ l ∈ [x.lob..x.hib] ∧ l < x.hib∧

∧ ∀j ∈ [x.lob..l] : x[j] = \binom{j − x.lob + (i + 1)}{i + 1}∧

∧ ∀j ∈ [l + 1..x.hib] : x[j] = \binom{j − x.lob + i}{i})

alapján könnyen látható:

\overline{P} ∧ \overline{π} ⇒ (Q ∧ x.dom = n − k + 1 ∧ i + 1 ∈ [0..k] ∧ l + 1 ∈ [x.lob..x.hib]∧

∧ ∀j ∈ [x.lob..l] : x[j] = \binom{j − x.lob + (i + 1)}{i + 1}∧

∧ \binom{(l + 1) − x.lob + (i + 1)}{i + 1} = x[l] + x[l + 1]∧

∧ ∀j ∈ [l + 2..x.hib] : x[j] = \binom{j − x.hib + i}{i})

Ebből következik, hogy

\overline{P} ∧ \overline{π} = (\overline{P}^{l←l+1})^{x[l+1]←x[l+1]+x[l]} = lf(x[l + 1] := x[l + 1] + x[l]; \overline{P}^{l←l+1})

Könnyen belátható, hogy az l projekció az \overline{S}_{1} programra nézve konstans függvény, ugyanúgy az i projekció az S_{1} programra nézve konstans függvény.

Összegezve a kapott eredményeket, a következő program megoldja a feladatot:

i, x := 0, (1, < 1_{1}, 1_{2}, ..., 1_{n−k+1} >) ; i < k ; \overline{l := 1 ; l < x.hib ; \overline{\frac{x[l + 1] := x[l + 1] + x[l]}{l := l + 1}} ; i := i + 1}