Proof: Program Counter Example

Let's prove the following theorem:

if the following are true:

instruction #1 is add dst=dst src1=src1 src2=src2
the PC at time 1 = 1

then the PC at time 2 = 2

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

Note that src1 src2, 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 src1, src2, and dst.

For reference, here is the simulator. We cannot use variable values in the simulator so src1, src2, and dst are given numerical values.

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 `add dst=dst src1=src1 src2=src2`
2	the PC at time 1 = 1

Proof Table

#	Claim	Reason
1	the PC at time (1 + 1) = 1 + 1	if instruction #1 is `add dst=dst src1=src1 src2=src2` and the PC at time 1 = 1, then the PC at time (1 + 1) = 1 + 1 (Program Counter on ADD)
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