Let's see this example in the simulator:
Memory Cells |
---|
Program Counter | Time |
---|---|
0 | 0 |
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.
Quiz (1 point)
store src=3 addr=6 imm=0
store src=4 addr=6 imm=1
store src=5 addr=6 imm=2
if the following are true:
- instruction #0 is
store src=3 addr=6 imm=0
- the PC at time 0 = 0
- value of cell 6 at time 0 = 7
- value of cell 3 at time 0 = 13
then value of cell 7 at time 1 = 13
- instruction #0 is
if the following are true:
- instruction #0 is
store src=3 addr=6 imm=0
- the PC at time 0 = 0
then the PC at time 1 = 1
- instruction #0 is
if the following are true:
- instruction #0 is
store src=3 addr=6 imm=0
- the PC at time 0 = 0
- value of cell 3 at time 0 = 13
- value of cell 6 at time 0 = 7
then value of cell 3 at time 1 = 13
- instruction #0 is
if the following are true:
- instruction #0 is
store src=3 addr=6 imm=0
- the PC at time 0 = 0
- value of cell 4 at time 0 = 11
- value of cell 6 at time 0 = 7
then value of cell 4 at time 1 = 11
- instruction #0 is
if the following are true:
- instruction #0 is
store src=3 addr=6 imm=0
- the PC at time 0 = 0
- value of cell 5 at time 0 = 20
- value of cell 6 at time 0 = 7
then value of cell 5 at time 1 = 20
- instruction #0 is
if the following are true:
- instruction #0 is
store src=3 addr=6 imm=0
- the PC at time 0 = 0
- value of cell 6 at time 0 = 7
- value of cell 6 at time 0 = 7
then value of cell 6 at time 1 = 7
- instruction #0 is
if the following are true:
- instruction #1 is
store src=4 addr=6 imm=1
- the PC at time 1 = 1
- value of cell 6 at time 1 = 7
- value of cell 4 at time 1 = 11
then value of cell 8 at time 2 = 11
- instruction #1 is
if the following are true:
- instruction #1 is
store src=4 addr=6 imm=1
- the PC at time 1 = 1
then the PC at time 2 = 2
- instruction #1 is
if the following are true:
- instruction #1 is
store src=4 addr=6 imm=1
- the PC at time 1 = 1
- value of cell 3 at time 1 = 13
- value of cell 6 at time 1 = 7
then value of cell 3 at time 2 = 13
- instruction #1 is
if the following are true:
- instruction #1 is
store src=4 addr=6 imm=1
- the PC at time 1 = 1
- value of cell 4 at time 1 = 11
- value of cell 6 at time 1 = 7
then value of cell 4 at time 2 = 11
- instruction #1 is
if the following are true:
- instruction #1 is
store src=4 addr=6 imm=1
- the PC at time 1 = 1
- value of cell 5 at time 1 = 20
- value of cell 6 at time 1 = 7
then value of cell 5 at time 2 = 20
- instruction #1 is
if the following are true:
- instruction #1 is
store src=4 addr=6 imm=1
- the PC at time 1 = 1
- value of cell 6 at time 1 = 7
- value of cell 6 at time 1 = 7
then value of cell 6 at time 2 = 7
- instruction #1 is
if the following are true:
- instruction #1 is
store src=4 addr=6 imm=1
- the PC at time 1 = 1
- value of cell 7 at time 1 = 13
- value of cell 6 at time 1 = 7
then value of cell 7 at time 2 = 13
- instruction #1 is
if the following are true:
- instruction #2 is
store src=5 addr=6 imm=2
- the PC at time 2 = 2
- value of cell 6 at time 2 = 7
- value of cell 5 at time 2 = 20
then value of cell 9 at time 3 = 20
- instruction #2 is
if the following are true:
- instruction #2 is
store src=5 addr=6 imm=2
- the PC at time 2 = 2
then the PC at time 3 = 3
- instruction #2 is
if the following are true:
- instruction #2 is
store src=5 addr=6 imm=2
- the PC at time 2 = 2
- value of cell 3 at time 2 = 13
- value of cell 6 at time 2 = 7
then value of cell 3 at time 3 = 13
- instruction #2 is
if the following are true:
- instruction #2 is
store src=5 addr=6 imm=2
- the PC at time 2 = 2
- value of cell 4 at time 2 = 11
- value of cell 6 at time 2 = 7
then value of cell 4 at time 3 = 11
- instruction #2 is
if the following are true:
- instruction #2 is
store src=5 addr=6 imm=2
- the PC at time 2 = 2
- value of cell 5 at time 2 = 20
- value of cell 6 at time 2 = 7
then value of cell 5 at time 3 = 20
- instruction #2 is
if the following are true:
- instruction #2 is
store src=5 addr=6 imm=2
- the PC at time 2 = 2
- value of cell 6 at time 2 = 7
- value of cell 6 at time 2 = 7
then value of cell 6 at time 3 = 7
- instruction #2 is
if the following are true:
- instruction #2 is
store src=5 addr=6 imm=2
- the PC at time 2 = 2
- value of cell 7 at time 2 = 13
- value of cell 6 at time 2 = 7
then value of cell 7 at time 3 = 13
- instruction #2 is
if the following are true:
- instruction #2 is
store src=5 addr=6 imm=2
- the PC at time 2 = 2
- value of cell 8 at time 2 = 11
- value of cell 6 at time 2 = 7
then value of cell 8 at time 3 = 11
- instruction #2 is
Please write your proof in the table below. Each row should contain one claim. The last claim is the statement that you are trying to prove.