Proof: Program Counter Example

Let's prove the following theorem:

if the following are true:

instruction #1 is addi dst=dst src=src imm=imm
the PC at time 1 = 1

then the PC at time 2 = 2

This proof shows that when an ADDI instruction is executed, the Program Counter (PC) increments by 1. Specifically, when the PC is 1, it is incremented to 2.

Note that src imm, and dst are left as variables because these values do not affect the PC. In other words, this property is true regardless of the values of src, imm, and dst.

For reference, here is the simulator. We cannot use variable values in the simulator so src, imm, and dst are given numerical values. Initially, the PC is 0, then 1, and finally 2.

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 #1 is `addi dst=dst src=src imm=imm`
2	the PC at time 1 = 1

Proof Table

#	Claim	Reason
1	the PC at time (1 + 1) = 1 + 1	if instruction #1 is `addi dst=dst src=src imm=imm` and the PC at time 1 = 1, then the PC at time (1 + 1) = 1 + 1 (Program Counter on ADDI)
2	1 + 1 = 2	1 + 1 = 2 (Fixed Value Statement)
3	the PC at time (1 + 1) = the PC at time 2	if 1 + 1 = 2, then the PC at time (1 + 1) = the PC at time 2 (Substitution)
4	the PC at time 2 = 2	if the PC at time (1 + 1) = 1 + 1 and the PC at time (1 + 1) = the PC at time 2 and 1 + 1 = 2, then the PC at time 2 = 2 (Transitive Property Application 2)

Comments

Please log in to add comments