Proof: LOAD Instruction Example

The following example shows what happens when a LOAD instruction is executed.

More precisely, we prove that

Let's prove the following theorem:

if the following are true:
  • instruction #0 is load dst=5 addr=1 imm=1
  • the PC at time 0 = 0
  • value of cell 1 at time 0 = 3
  • value of cell 4 at time 0 = 7

then value of cell 5 at time 1 = 7

Try out the example in the simulator:

Instructions
Memory Cells
Program Counter Time
0 0
LW Computer Simulator

The following example shows that when a LOAD instruction with dst = 5, addr = 1, and imm = 1 is executed, the computer performs the following actions:

  1. Looks up memory cell #1 and finds 3
  2. Adds 1 to 3, which is 4.
  3. Copies the value in memory cell #4 (9) to memory cell #5.

Proof:

View as a tree | View dependent proofs | Try proving it

Given
1 instruction #0 is load dst=5 addr=1 imm=1
2 the PC at time 0 = 0
3 value of cell 1 at time 0 = 3
4 value of cell 4 at time 0 = 7
Proof Table
# Claim Reason
1 value of cell 5 at time (0 + 1) = value of cell ((value of cell 1 at time 0) + 1) at time 0 if instruction #0 is load dst=5 addr=1 imm=1 and the PC at time 0 = 0, then value of cell 5 at time (0 + 1) = value of cell ((value of cell 1 at time 0) + 1) at time 0
2 (value of cell 1 at time 0) + 1 = 3 + 1 if value of cell 1 at time 0 = 3, then (value of cell 1 at time 0) + 1 = 3 + 1
3 3 + 1 = 4 3 + 1 = 4
4 (value of cell 1 at time 0) + 1 = 4 if (value of cell 1 at time 0) + 1 = 3 + 1 and 3 + 1 = 4, then (value of cell 1 at time 0) + 1 = 4
5 value of cell ((value of cell 1 at time 0) + 1) at time 0 = value of cell 4 at time 0 if (value of cell 1 at time 0) + 1 = 4, then value of cell ((value of cell 1 at time 0) + 1) at time 0 = value of cell 4 at time 0
6 value of cell ((value of cell 1 at time 0) + 1) at time 0 = 7 if value of cell ((value of cell 1 at time 0) + 1) at time 0 = value of cell 4 at time 0 and value of cell 4 at time 0 = 7, then value of cell ((value of cell 1 at time 0) + 1) at time 0 = 7
7 value of cell 5 at time (0 + 1) = 7 if value of cell 5 at time (0 + 1) = value of cell ((value of cell 1 at time 0) + 1) at time 0 and value of cell ((value of cell 1 at time 0) + 1) at time 0 = 7, then value of cell 5 at time (0 + 1) = 7
8 0 + 1 = 1 0 + 1 = 1
9 value of cell 5 at time (0 + 1) = value of cell 5 at time 1 if 0 + 1 = 1, then value of cell 5 at time (0 + 1) = value of cell 5 at time 1
10 value of cell 5 at time 1 = 7 if value of cell 5 at time (0 + 1) = value of cell 5 at time 1 and value of cell 5 at time (0 + 1) = 7, then value of cell 5 at time 1 = 7

Comments

Please log in to add comments