|
State Index |
Path Conditions |
Facts | Obligations |
|---|---|---|---|
procedure Multiply (updates n: Natural, |
|||
| 0 |
n₀ ≥ 0 m₀ ≥ 0 |
m₀ ≥ 0 | |
variable zero: Natural |
|||
| 1 |
n₁ ≥ 0 m₁ ≥ 0 zero₁ ≥ 0 n₁ = n₀ m₁ = m₀ zero₁ = 0 |
||
if AreEqual (m, zero) then |
|||
| 2 | m₁ = zero₁ |
n₂ ≥ 0 m₂ ≥ 0 zero₂ ≥ 0 n₂ = n₁ m₂ = m₁ zero₂ = zero₁ |
|
Clear (n) |
|||
| 3 | m₁ = zero₁ |
n₃ ≥ 0 m₃ ≥ 0 zero₃ ≥ 0 n₃ = 0 m₃ = m₂ zero₃ = zero₂ |
|
else |
|||
| 4 | m₁ ≠ zero₁ |
n₄ ≥ 0 m₄ ≥ 0 zero₄ ≥ 0 n₄ = n₁ m₄ = m₁ zero₄ = zero₁ |
|
variable one: Natural |
|||
| 5 | m₁ ≠ zero₁ |
one₅ ≥ 0 n₅ ≥ 0 m₅ ≥ 0 zero₅ ≥ 0 n₅ = n₄ m₅ = m₄ zero₅ = zero₄ one₅ = 0 |
|
Increment (one) |
|||
| 6 | m₁ ≠ zero₁ |
one₆ ≥ 0 n₆ ≥ 0 m₆ ≥ 0 zero₆ ≥ 0 one₆ = one₅ + 1 n₆ = n₅ m₆ = m₅ zero₆ = zero₅ |
|
if IsGreater (m, one) then |
|||
| 7 |
m₁ ≠ zero₁ m₆ > one₆ |
one₇ ≥ 0 n₇ ≥ 0 m₇ ≥ 0 zero₇ ≥ 0 one₇ = one₆ n₇ = n₆ m₇ = m₆ zero₇ = zero₆ |
|
variable nCopy: Natural |
|||
| 8 |
m₁ ≠ zero₁ m₆ > one₆ |
nCopy₈ ≥ 0 one₈ ≥ 0 n₈ ≥ 0 m₈ ≥ 0 zero₈ ≥ 0 one₈ = one₇ n₈ = n₇ m₈ = m₇ zero₈ = zero₇ nCopy₈ = 0 |
|
nCopy := Replica (n) |
|||
| 9 |
m₁ ≠ zero₁ m₆ > one₆ |
nCopy₉ ≥ 0 one₉ ≥ 0 n₉ ≥ 0 m₉ ≥ 0 zero₉ ≥ 0 nCopy₉ = n₈ one₉ = one₈ n₉ = n₈ m₉ = m₈ zero₉ = zero₈ |
m₉ > 0 |
Decrement (m) |
|||
| 10 |
m₁ ≠ zero₁ m₆ > one₆ |
nCopy₁₀ ≥ 0 one₁₀ ≥ 0 n₁₀ ≥ 0 m₁₀ ≥ 0 zero₁₀ ≥ 0 m₁₀ = m₉ – 1 nCopy₁₀ = nCopy₉ one₁₀ = one₉ n₁₀ = n₉ zero₁₀ = zero₉ |
m₁₀ < m₀ |
Multiply (n, m) |
|||
| 11 |
m₁ ≠ zero₁ m₆ > one₆ |
nCopy₁₁ ≥ 0 one₁₁ ≥ 0 n₁₁ ≥ 0 m₁₁ ≥ 0 zero₁₁ ≥ 0 n₁₁ = n₁₀ × m₁₁ m₁₁ = m₁₀ nCopy₁₁ = nCopy₁₀ one₁₁ = one₁₀ zero₁₁ = zero₁₀ |
|
Increment (m) |
|||
| 12 |
m₁ ≠ zero₁ m₆ > one₆ |
nCopy₁₂ ≥ 0 one₁₂ ≥ 0 n₁₂ ≥ 0 m₁₂ ≥ 0 zero₁₂ ≥ 0 m₁₂ = m₁₁ + 1 nCopy₁₂ = nCopy₁₁ one₁₂ = one₁₁ n₁₂ = n₁₁ zero₁₂ = zero₁₁ |
|
Add (n, nCopy) |
|||
| 13 |
m₁ ≠ zero₁ m₆ > one₆ |
nCopy₁₃ ≥ 0 one₁₃ ≥ 0 n₁₃ ≥ 0 m₁₃ ≥ 0 zero₁₃ ≥ 0 n₁₃ = n₁₂ + nCopy₁₃ nCopy₁₃ = nCopy₁₂ one₁₃ = one₁₂ m₁₃ = m₁₂ zero₁₃ = zero₁₂ |
|
end if |
|||
| 14 | m₁ ≠ zero₁ |
one₁₄ ≥ 0 n₁₄ ≥ 0 m₁₄ ≥ 0 zero₁₄ ≥ 0 m₆ > one₆ ⇒ one₁₄ = one₁₃ m₆ > one₆ ⇒ n₁₄ = n₁₃ m₆ > one₆ ⇒ m₁₄ = m₁₃ m₆ > one₆ ⇒ zero₁₄ = zero₁₃ m₆ ≤ one₆ ⇒ one₁₄ = one₆ m₆ ≤ one₆ ⇒ n₁₄ = n₆ m₆ ≤ one₆ ⇒ m₁₄ = m₆ m₆ ≤ one₆ ⇒ zero₁₄ = zero₆ |
|
end if |
|||
| 15 |
n₁₅ ≥ 0 m₁₅ ≥ 0 zero₁₅ ≥ 0 m₁ = zero₁ ⇒ n₁₅ = n₃ m₁ = zero₁ ⇒ m₁₅ = m₃ m₁ = zero₁ ⇒ zero₁₅ = zero₃ m₁ ≠ zero₁ ⇒ n₁₅ = n₁₄ m₁ ≠ zero₁ ⇒ m₁₅ = m₁₄ m₁ ≠ zero₁ ⇒ zero₁₅ = zero₁₄ |
m₁₅ = m₀ n₁₅ = n₀ × m₁₅ |
|
end Multiply |
|||