Proof: ADDI Instruction Example

Let's prove the following theorem:

if the following are true:
  • instruction #0 is addi dst=2 src=1 imm=5
  • the PC at time 0 = 0
  • value of cell 1 at time 0 = 4

then value of cell 2 at time 1 = 9

This proof shows an ADDI instruction that adds the value in memory cell #1 and 5 and stores the result in memory cell #2. It starts with the ADDI Instruction Property and performs some basic algebra to compute the value of memory cell #2. 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 addi dst=2 src=1 imm=5
2 the PC at time 0 = 0
3 value of cell 1 at time 0 = 4
Proof Table
# Claim Reason
1 value of cell 2 at time (0 + 1) = (value of cell 1 at time 0) + 5 if instruction #0 is addi dst=2 src=1 imm=5 and the PC at time 0 = 0, then value of cell 2 at time (0 + 1) = (value of cell 1 at time 0) + 5
2 0 + 1 = 1 0 + 1 = 1
3 value of cell 2 at time (0 + 1) = value of cell 2 at time 1 if 0 + 1 = 1, then value of cell 2 at time (0 + 1) = value of cell 2 at time 1
4 value of cell 2 at time 1 = (value of cell 1 at time 0) + 5 if value of cell 2 at time (0 + 1) = value of cell 2 at time 1 and value of cell 2 at time (0 + 1) = (value of cell 1 at time 0) + 5, then value of cell 2 at time 1 = (value of cell 1 at time 0) + 5
5 value of cell 2 at time 1 = 4 + 5 if value of cell 2 at time 1 = (value of cell 1 at time 0) + 5 and value of cell 1 at time 0 = 4, then value of cell 2 at time 1 = 4 + 5
6 4 + 5 = 9 4 + 5 = 9
7 value of cell 2 at time 1 = 9 if value of cell 2 at time 1 = 4 + 5 and 4 + 5 = 9, then value of cell 2 at time 1 = 9

Comments

Please log in to add comments