Proof: Store 7
Let's prove the following theorem:
if the following are true:
- instruction #13 is
store src=3 addr=1 imm=0 - the PC at time 7 = 13
- value of cell 1 at time 7 = 126
- value of cell 3 at time 7 = 3
then value of cell 126 at time 8 = 3
Proof:
Given
| 1 | instruction #13 is store src=3 addr=1 imm=0 |
|---|---|
| 2 | the PC at time 7 = 13 |
| 3 | value of cell 1 at time 7 = 126 |
| 4 | value of cell 3 at time 7 = 3 |
| # | Claim | Reason |
|---|---|---|
| 1 | value of cell ((value of cell 1 at time 7) + 0) at time (7 + 1) = value of cell 3 at time 7 | if instruction #13 is store src=3 addr=1 imm=0 and the PC at time 7 = 13, then value of cell ((value of cell 1 at time 7) + 0) at time (7 + 1) = value of cell 3 at time 7 |
| 2 | (value of cell 1 at time 7) + 0 = 126 + 0 | if value of cell 1 at time 7 = 126, then (value of cell 1 at time 7) + 0 = 126 + 0 |
| 3 | 126 + 0 = 126 | 126 + 0 = 126 |
| 4 | (value of cell 1 at time 7) + 0 = 126 | if (value of cell 1 at time 7) + 0 = 126 + 0 and 126 + 0 = 126, then (value of cell 1 at time 7) + 0 = 126 |
| 5 | value of cell ((value of cell 1 at time 7) + 0) at time (7 + 1) = value of cell 126 at time (7 + 1) | if (value of cell 1 at time 7) + 0 = 126, then value of cell ((value of cell 1 at time 7) + 0) at time (7 + 1) = value of cell 126 at time (7 + 1) |
| 6 | 7 + 1 = 8 | 7 + 1 = 8 |
| 7 | value of cell 126 at time (7 + 1) = value of cell 126 at time 8 | if 7 + 1 = 8, then value of cell 126 at time (7 + 1) = value of cell 126 at time 8 |
| 8 | value of cell 126 at time 8 = value of cell 3 at time 7 | if value of cell ((value of cell 1 at time 7) + 0) at time (7 + 1) = value of cell 126 at time (7 + 1) and value of cell 126 at time (7 + 1) = value of cell 126 at time 8 and value of cell ((value of cell 1 at time 7) + 0) at time (7 + 1) = value of cell 3 at time 7, then value of cell 126 at time 8 = value of cell 3 at time 7 |
| 9 | value of cell 126 at time 8 = 3 | if value of cell 126 at time 8 = value of cell 3 at time 7 and value of cell 3 at time 7 = 3, then value of cell 126 at time 8 = 3 |
Comments
Please log in to add comments