Proof: Copy By Store Example
In this example, we present a program that copies 3 values using STORE instructions.
More precisely, we show that
Let's prove the following theorem:
if the following are true:
- the PC at time 0 = 0
- instruction #0 is
store src=3 addr=6 imm=0 - instruction #1 is
store src=4 addr=6 imm=1 - instruction #2 is
store src=5 addr=6 imm=2 - value of cell 3 at time 0 = 13
- value of cell 4 at time 0 = 11
- value of cell 5 at time 0 = 20
- value of cell 6 at time 0 = 7
then value of cell 8 at time 3 = 11
Let's see this example in the simulator:
Instructions
| Memory Cells |
|---|
| Program Counter | Time |
|---|---|
| 0 | 0 |
LW Computer Simulator
Notice how addr remains the same, and the imm is increased. In this pattern, the addr indicates the beginning of an array of values, and the imm is the index, or location, within the array.
Instruction #0 copies cell #3 to cell #7. The destination is the value stored in cell #6 (7) plus the imm (0).
Instruction #1 copies cell #4 to cell #8. The destination is the value stored in cell #6 (7) plus the imm (1).
Finally, instruction #2 copies cell #5 to cell #9. The destination is the value stored in cell #6 (7) plus the imm (2).
To make claims about value of the cell #8 at time 3, we start at time 0, then make claims about the state at time 1, and use them to make claims about time 2, and so on.
Proof:
Given
| 1 | the PC at time 0 = 0 |
|---|---|
| 2 | instruction #0 is store src=3 addr=6 imm=0 |
| 3 | instruction #1 is store src=4 addr=6 imm=1 |
| 4 | instruction #2 is store src=5 addr=6 imm=2 |
| 5 | value of cell 3 at time 0 = 13 |
| 6 | value of cell 4 at time 0 = 11 |
| 7 | value of cell 5 at time 0 = 20 |
| 8 | value of cell 6 at time 0 = 7 |
| # | Claim | Reason |
|---|---|---|
| 1 | value of cell 7 at time 1 = 13 | if instruction #0 is store src=3 addr=6 imm=0 and the PC at time 0 = 0 and value of cell 6 at time 0 = 7 and value of cell 3 at time 0 = 13, then value of cell 7 at time 1 = 13 |
| 2 | the PC at time 1 = 1 | if instruction #0 is store src=3 addr=6 imm=0 and the PC at time 0 = 0, then the PC at time 1 = 1 |
| 3 | value of cell 3 at time 1 = 13 | if instruction #0 is store src=3 addr=6 imm=0 and the PC at time 0 = 0 and value of cell 3 at time 0 = 13 and value of cell 6 at time 0 = 7, then value of cell 3 at time 1 = 13 |
| 4 | value of cell 4 at time 1 = 11 | if instruction #0 is store src=3 addr=6 imm=0 and the PC at time 0 = 0 and value of cell 4 at time 0 = 11 and value of cell 6 at time 0 = 7, then value of cell 4 at time 1 = 11 |
| 5 | value of cell 5 at time 1 = 20 | if instruction #0 is store src=3 addr=6 imm=0 and the PC at time 0 = 0 and value of cell 5 at time 0 = 20 and value of cell 6 at time 0 = 7, then value of cell 5 at time 1 = 20 |
| 6 | value of cell 6 at time 1 = 7 | if instruction #0 is store src=3 addr=6 imm=0 and the PC at time 0 = 0 and value of cell 6 at time 0 = 7 and value of cell 6 at time 0 = 7, then value of cell 6 at time 1 = 7 |
| 7 | value of cell 8 at time 2 = 11 | if instruction #1 is store src=4 addr=6 imm=1 and the PC at time 1 = 1 and value of cell 6 at time 1 = 7 and value of cell 4 at time 1 = 11, then value of cell 8 at time 2 = 11 |
| 8 | the PC at time 2 = 2 | if instruction #1 is store src=4 addr=6 imm=1 and the PC at time 1 = 1, then the PC at time 2 = 2 |
| 9 | value of cell 3 at time 2 = 13 | if instruction #1 is store src=4 addr=6 imm=1 and the PC at time 1 = 1 and value of cell 3 at time 1 = 13 and value of cell 6 at time 1 = 7, then value of cell 3 at time 2 = 13 |
| 10 | value of cell 4 at time 2 = 11 | if instruction #1 is store src=4 addr=6 imm=1 and the PC at time 1 = 1 and value of cell 4 at time 1 = 11 and value of cell 6 at time 1 = 7, then value of cell 4 at time 2 = 11 |
| 11 | value of cell 5 at time 2 = 20 | if instruction #1 is store src=4 addr=6 imm=1 and the PC at time 1 = 1 and value of cell 5 at time 1 = 20 and value of cell 6 at time 1 = 7, then value of cell 5 at time 2 = 20 |
| 12 | value of cell 6 at time 2 = 7 | if instruction #1 is store src=4 addr=6 imm=1 and the PC at time 1 = 1 and value of cell 6 at time 1 = 7 and value of cell 6 at time 1 = 7, then value of cell 6 at time 2 = 7 |
| 13 | value of cell 7 at time 2 = 13 | if instruction #1 is store src=4 addr=6 imm=1 and the PC at time 1 = 1 and value of cell 7 at time 1 = 13 and value of cell 6 at time 1 = 7, then value of cell 7 at time 2 = 13 |
| 14 | value of cell 9 at time 3 = 20 | if instruction #2 is store src=5 addr=6 imm=2 and the PC at time 2 = 2 and value of cell 6 at time 2 = 7 and value of cell 5 at time 2 = 20, then value of cell 9 at time 3 = 20 |
| 15 | the PC at time 3 = 3 | if instruction #2 is store src=5 addr=6 imm=2 and the PC at time 2 = 2, then the PC at time 3 = 3 |
| 16 | value of cell 3 at time 3 = 13 | if instruction #2 is store src=5 addr=6 imm=2 and the PC at time 2 = 2 and value of cell 3 at time 2 = 13 and value of cell 6 at time 2 = 7, then value of cell 3 at time 3 = 13 |
| 17 | value of cell 4 at time 3 = 11 | if instruction #2 is store src=5 addr=6 imm=2 and the PC at time 2 = 2 and value of cell 4 at time 2 = 11 and value of cell 6 at time 2 = 7, then value of cell 4 at time 3 = 11 |
| 18 | value of cell 5 at time 3 = 20 | if instruction #2 is store src=5 addr=6 imm=2 and the PC at time 2 = 2 and value of cell 5 at time 2 = 20 and value of cell 6 at time 2 = 7, then value of cell 5 at time 3 = 20 |
| 19 | value of cell 6 at time 3 = 7 | if instruction #2 is store src=5 addr=6 imm=2 and the PC at time 2 = 2 and value of cell 6 at time 2 = 7 and value of cell 6 at time 2 = 7, then value of cell 6 at time 3 = 7 |
| 20 | value of cell 7 at time 3 = 13 | if instruction #2 is store src=5 addr=6 imm=2 and the PC at time 2 = 2 and value of cell 7 at time 2 = 13 and value of cell 6 at time 2 = 7, then value of cell 7 at time 3 = 13 |
| 21 | value of cell 8 at time 3 = 11 | if instruction #2 is store src=5 addr=6 imm=2 and the PC at time 2 = 2 and value of cell 8 at time 2 = 11 and value of cell 6 at time 2 = 7, then value of cell 8 at time 3 = 11 |
Comments
Please log in to add comments