Prím tulajdonság meghatározása

A =ℕ n×𝕃 l

B ={ℕ \atop n′}

Q : (n = n′)

R : (Q ∧ (¬l ↔ (n = 1 ∨ ∃k ∈ [2..n − 1] : n mod k = 0)))

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

P : (Q ∧ i ∈ [1..n] ∧ (¬l ↔ (n = 1 ∨ ∃k ∈ [2..i] : n mod k = 0)))

1. A ciklus levezetési szabálya második feltétele: P ∧ ¬π ⇒ R teljesül, ha ¬π : ¬l ∨ i ≥ n − 1. Tehát π : l ∧ i < n − 1 alkalmas választás.

2. A ciklus levezetési szabálya harmadik feltétele: P ∧ π ⇒ t > 0 teljesül, ha t : n − 1 − i a π választása miatt.

3. Célszerű a ciklusmagot S_{0} : (S_{1}; S_{2}) szekvencia fomában keresni, ahol S_{2} = (i := i + 1) abból a meggondolásból, hogy a ciklus levezetési szabályának 5. feltétele is teljesüljön. Alkalmazva a szekvencia leggyengébb előfeltételére ismert tételt, P ∧ π ⇒ lf(S_{0}, P) ⇔ lf(S_{1}, lf(S_{2}, P)) teljesül, ha P ∧ π ⇒ lf(S_{1}, P^{i←i+1}), mivel lf(i := i + 1, P) ⇔ P^{i←i+1}. P^{i←i+1} : (Q ∧ i + 1 ∈ [1..n] ∧ (¬l ↔ (n = 1 ∨ ∃k ∈ [2..i + 1] : n mod k = 0))), ugyanakkor P ∧ π ⇒ Q ∧ i + 1 ∈ [1..n] ∧ (¬n mod i + 1 ≠ 0 ↔ (n = 1 ∨ ∃k ∈ [2..i + 1] : n mod k = 0)), ahonnan P ∧ π ⇒ P^{i←i+1}^{l←nmodi+1≠0}. Ezért Tehát S_{0} = (l := n mod i + 1 ≠ 0; i := i + 1) alkalmas választás a ciklus levezetési szabálya negyedik feltétele teljesüléséhez.

4. 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.

Mivel lf(S_{0}, t ≤ t_{0}) ⇔ (t ≤ t_{0})^{i←i+1}^{l←nmodi+1≠0} ⇔ n − 1 − i ≤ t_{0} + 1 ⇔ t ≤ t_{0} + 1 tetszőleges t_{0} ∈ ℤ-re, ezért a ciklus levezetési szabályának ötödik feltétele is teljesül.

5. Könnyen ellenőrizhető, hogy Q ⇒ P nem teljesül. Ugyanakkor látható, hogy Q ⇒ P^{i,l←1,n≠1} fennáll, mivel P^{i,l←1,n≠1} : (Q ∧ 1 ∈ [1..n] ∧ (¬n ≠ 1 ↔ (n = 1 ∨ ∃k ∈ [2..1] : n mod k = 0))) és (1 ∈ [1..n] ∧ (¬n ≠ 1 ↔ (n = 1 ∨ ∃k ∈ [2..1] : n mod k = 0))) ⇔ true. Tehát Q ⇒ lf(i, l := 1, n ≠ 1, P). Ugyanakkor a ciklus levezetési szabálya első feltétele: P ⇒ P nyilván teljesül, ezért P ⇒ lf(DO, R) is igaz, ahol DO = (l ∧ i < n − 1, S_{0}). Alkalmazva a szekvenciával kapcsolatos levezetési szabályt, kapjuk: Q ⇒ lf((i, l := 1, n ≠ 1; DO), R)

Tehát a keresett program:

i, l := 1, n ≠ 1 ; l ∧ i < n − 1 ; \overline{\frac{l := n mod i + 1 ≠ 0}{i := i + 1}}