Proof: ADD Instruction Example

Let's prove the following theorem:

if the following are true:
  • instruction #0 is add dst=3 src1=1 src2=2
  • the PC at time 0 = 0
  • value of cell 1 at time 0 = 2
  • value of cell 2 at time 0 = 6

then value of cell 3 at time 1 = 8

This proof shows an ADD instruction that adds the values in memory cell numbers 1 and 2 and stores the result in memory cell #3. It uses the ADD Instruction Property and performs some basic algebra to compute the value of memory cell #3. For reference, here is the simulator:

Instructions
Memory Cells
Program Counter Time
0 0
LW Computer Simulator

Proof:

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

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

Comments

Please log in to add comments