Egész arithmetika

Összeadás Az x egész számokból álló vektor egy decimális szám számjegyeit tartalmazza helyi-

érték szerint csökkenő sorrendben. Állítsuk elő x-ben az eredetinél eggyel nagyobb szám ugyanilyen ábrázolását és mondjuk meg, hogy volt-e túlcsordulás.

A feladat specifikációja:

Legyen 𝕏 : vekt(ℤ, {0, 1, ..., 9}).

A =𝕏 x×𝕃 l

B ={𝕏 \atop x′}

Q : (x = x′)

R : (( ∑_{j=x′.lob}^{x′.hib} x′[j] · 10^{(x′.hib−j)}) + 1 = ( ∑_{j=x.lob}^{x.hib} x[j] · 10^{(x.hib−j)}) + χ(l) · 10^{(x.hib−x.lob+1)})

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

P : (i ∈ [x.lob..x.hib + 1] ∧

∧( ∑_{j=i}^{x′.hib} x′[j] · 10^{(x′.hib−j)}) + 1 = ( ∑_{j=i}^{x.hib} x[j] · 10^{(x.hib−j)}) + χ(l) · 10^{(x.hib−i+1)} ∧

∧∀j ∈ [x.lob..i − 1] : x′[j] = x[j])

1. Q ⇏ P, de Q ⇒ P^{l,i←↑,x.hib+1}.

Innen adódik, hogy Q ⇒ lf(l, i :=↑, x.hib + 1, P)

2. A ciklus levezetési szabálya második feltétele: P ∧ ¬π ⇒ R teljesül, ha ¬π : (i ≤ x.lob). Ezért π : (i > x.lob) alkalmas választás.

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

4. 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. Ebből adódik, hogy az S_{1} programra P ∧ π ⇒ lf(S_{1}, P^{i←i−1}) kell teljesüljön ahhoz, hogy a ciklus levezetési szabálya negyedik feltétele teljesüljön. P ∧ π ⇒ (i − 1 ∈ [x.lob..x.hib + 1] ∧

∧( ∑_{j=i−1}^{x′.hib} x′[j] · 10^{(x′.hib−j)}) + 1 = ( ∑_{j=i}^{x.hib} x[j] · 10^{(x.hib−j)}) +

+x′[i − 1] · 10^{(x′.hib−i+1)} + χ(l) · 10^{(x.hib−i+1)} ∧ ∧∀j ∈ [x.lob..i − 1] : x′[j] = x[j]). Ezért P ∧ π ∧ x[i − 1] + χ(l) ≤ 9 ⇒ (i − 1 ∈ [x.lob..x.hib + 1] ∧

∧( ∑_{j=i−1}^{x′.hib} x′[j] · 10^{(x′.hib−j)}) + 1 = ( ∑_{j=i}^{x.hib} x[j] · 10^{(x.hib−j)}) +

+(x[i − 1] + χ(l)) · 10^{(x.hib−i+1)} ∧ ∧∀j ∈ [x.lob..i − 2] : x′[j] = x[j]). Ahonnan P ∧ π ∧ x[i − 1] + χ(l) ≤ 9 ⇒ P^{i←i−1}^{x[i−1],l←x[i−1]+χ(l),↓}. Hasonlóan P ∧ π ∧ x[i − 1] + χ(l) > 9 ⇒ P^{i←i−1}^{x[i−1],l←0,↑}.

5. Könnyen ellenőrízhető, hogy a ciklus levezetési szabálya ötödik feltétele is teljesül.

Egy lehetséges megoldás tehát a következő program:

i, l := x.hib + 1, ↑ ; i > x.lob ; \overline{\  x[i − 1] + χ(l) ≤ 9  / ; \begin{aligned}x[i − 1], l := x[i − 1] + χ(l), ↓ \\ & x[i − 1], l := 0, ↑ \end{aligned} ; i := i − 1}

Kivonás Az x egész számokból álló vektor egy decimális szám számjegyeit tartalmazza helyi-

érték szerint csökkenő sorrendben. Állítsuk elő x-ben az eredetinél eggyel kisebb szám ugyanilyen ábrázolását és mondjuk meg, hogy volt-e túlcsordulás.

A feladat specifikációja: Legyen 𝕏 : vekt(ℤ, {0, 1, ..., 9}). A =𝕏 x×𝕃 l

B ={𝕏 \atop x′}

Q : (x = x′)

R : (χ(l) · 10^{(x.hib−x.lob+1)} + ( ∑_{j=x′.lob}^{x′.hib} x′[j] · 10^{(x′.hib−j)}) − 1 = ∑_{j=x.lob}^{x.hib} x[j] · 10^{(x.hib−j)})

Keressük a megoldást adó programot ciklus formában, ahol P : (i ∈ [x.lob..x.hib + 1] ∧

∧( ∑_{j=i}^{x′.hib} x′[j] · 10^{(x′.hib−j)}) − 1 = ( ∑_{j=i}^{x.hib} x[j] · 10^{(x.hib−j)}) − χ(l) · 10^{(x.hib−i+1)} ∧

∧∀j ∈ [x.lob..i − 1] : x′[j] = x[j]) A levezetés az előzőekhez hasonlóan történhet. Egy lehetséges megoldás tehát a következő program:

i, l := x.hib + 1, ↑ ; i > x.lob ; \overline{\  0 ≤ x[i − 1] − χ(l)  / ; \begin{aligned}x[i − 1], l := x[i − 1] − χ(l), ↓ \\ & x[i − 1], l := 9, ↑ \end{aligned} ; i := i − 1}