|
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 not AreEqual (m, zero) then |
|||
| 2 | m₁ ≠ zero₁ |
n₂ ≥ 0 m₂ ≥ 0 zero₂ ≥ 0 n₂ = n₁ m₂ = m₁ zero₂ = zero₁ |
|
variable one: Natural |
|||
| 3 | m₁ ≠ zero₁ |
one₃ ≥ 0 n₃ ≥ 0 m₃ ≥ 0 zero₃ ≥ 0 n₃ = n₂ m₃ = m₂ zero₃ = zero₂ one₃ = 0 |
|
Increment (one) |
|||
| 4 | m₁ ≠ zero₁ |
one₄ ≥ 0 n₄ ≥ 0 m₄ ≥ 0 zero₄ ≥ 0 one₄ = one₃ + 1 n₄ = n₃ m₄ = m₃ zero₄ = zero₃ |
|
if IsGreater (m, one) then |
|||
| 5 |
m₁ ≠ zero₁ m₄ > one₄ |
one₅ ≥ 0 n₅ ≥ 0 m₅ ≥ 0 zero₅ ≥ 0 one₅ = one₄ n₅ = n₄ m₅ = m₄ zero₅ = zero₄ |
|
variable nCopy: Natural |
|||
| 6 |
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) |
|||
| 7 |
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) |
|||
| 8 |
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) |
|||
| 9 |
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) |
|||
| 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₉ |
|
Add (n, nCopy) |
|||
| 11 |
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 |
|||
| 12 | 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 |
|||
| 13 |
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 |
|||