Legnagyobb közös osztó meghatározása

A feladat specifikációja:

A =ℕ a×ℕ b×ℕ d

B ={ℕ \atop a′}×{ℕ \atop b′}

Q : (a = a′ ∧ b = b′)

R : (d = lnko(a′, b′))

Keressük a megoldást adó programot ciklus formában, ahol

P : (lnko(a′, b′) = lnko(a, d))

1. Q ⇏ P, de Q ⇒ P^{d←b}.

Innen adódik, hogy Q ⇒ lf(d := b, P)

2. A ciklus levezetési szabálya második feltétele: P ∧ ¬π ⇒ R teljesül, ha ¬π : (a = d), mivel lnko(a′, b′) = lnko(a, d) ∧ a = d ⇒ d = lnko(a′, b′). Ezért π : (a ≠ d) alkalmas választás.

3. A ciklus levezetési szabálya harmadik feltétele: P ∧ π ⇒ t > 0 teljesül, ha t : a + d a π választása miatt.

5. A ciklus levezetési szabálya ötödik feltétele: P ∧ π ∧ t ≤ t_{0} + 1 ⇒ lf(S_{0}, t ≤ t_{0}) minden t_{0} ∈ ℤ-re. Könnyen látható, hogy P ∧ π ∧ a > d ∧ a + d ≤ t_{0} + 1 ⇒ (a − d) + d ≤ t_{0} ⇔ (t ≤ t_{0})^{a←a−d} ⇔ ⇔ lf(a := a − d, t ≤ t_{0}), valamint P ∧ π ∧ a < d ∧ a + d ≤ t_{0} + 1 ⇒ a + (d − a) ≤ t_{0} ⇔ (t ≤ t_{0})^{d←d−a} ⇔ ⇔ lf(d := d − a, t ≤ t_{0}). Alkalmazva az elágazás levezetési szabályát, kapjuk P ∧ π ∧ (a < d ∨ a > d) ∧ t ≤ t_{0} + 1 ⇒ ⇒ lf(IF (a > d : a := a − d, a < d : d := d − a), t ≤ t_{0}). Vegyük észre, hogy π ∧ (a < d ∨ a > d) ⇔ π, ezért P ∧ π ∧ t ≤ t_{0} + 1 ⇒ lf(IF (a > d : a := a − d, a < d : d := d − a), t ≤ t_{0}).

4. Belátható, hogy a ciklus levezetési szabályának negyedik feltétele is teljesül, ha S_{0} : IF (a > d : a := a − d, a < d : d := d − a). Vegyük észre, hogy P ∧ π ∧ a > d ⇒ (lnko(a′, b′) = lnko(a, d) = lnko(a − d, d)) ⇒ ⇒ (lnko(a′, b′) = lnko(a − d, d)) ⇔ P^{a←a−d} ⇔ lf(a := a − d, P). Tehát P ∧ π ∧ a > d ⇒ lf(a := a − d, P). Ugyanígy belátható, hogy P ∧ π ∧ a < d ⇒ lf(d := d − a, P). Alkalmazva az elágazás levezetési szabályát, kapjuk, hogy P ∧ π ⇒ lf(IF (a > d : a := a − d, a < d : d := d − a), P), tehát a ciklus levezetési szabályának negyedik feltétele is teljesül az S_{0} fenti választása esetén. Mivel P ⇒ P nyilván teljesül, ezért P ⇒ lf(DO(a ≠ d, IF (a > d : a := a − d, a < d : d := d − a)), R).

Alkalmazva a szekvencia levezetési szabályat, kapjuk, hogy Q ⇒ lf((d := b, DO(a ≠ d, IF (a > d : a := a − d, a < d : d := d − a))), R). A specifikáció tételének alkalmazásával adódik, hogy egy lehetséges megoldás a

(d := b, DO(a ≠ d, IF (a > d : a := a − d, a < d : d := d − a)))

program, amely struktogrammja:

d := b ; a ≠ d ; \overline{\frac{\begin{aligned}\  a > d \\ & \  a < d \end{aligned}}{\begin{aligned}a := a − d \\ & d := d − a \end{aligned}}}