Proof: Copy Example

In this example, we present a program that copies 3 numbers to other memory locations. Then we show that:

Let's prove the following theorem:

if the following are true:

the PC at time 0 = 0
instruction #0 is addi dst=7 src=3 imm=0
instruction #1 is addi dst=8 src=4 imm=0
instruction #2 is addi dst=9 src=5 imm=0
value of cell 3 at time 0 = 13
value of cell 4 at time 0 = 11
value of cell 5 at time 0 = 20

then value of cell 8 at time 3 = 11

Instructions

Memory Cells

Program Counter	Time
0	0

LW Computer Simulator

The ADDI instructions adds two numbers, but by setting the imm to 0, we can use them to copy numbers from one location to another.

Instruction #0 copies cell #3 to cell #7 by adding 0 to cell #3 and storing the result in cell #7.

Similarly, instruction #1 stores cell #4 to cell #8, and instruction #2 copies cell #5 to cell #9.

Proof:

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

Given

1	the PC at time 0 = 0
2	instruction #0 is `addi dst=7 src=3 imm=0`
3	instruction #1 is `addi dst=8 src=4 imm=0`
4	instruction #2 is `addi dst=9 src=5 imm=0`
5	value of cell 3 at time 0 = 13
6	value of cell 4 at time 0 = 11
7	value of cell 5 at time 0 = 20

Proof Table

Comments

Please log in to add comments

#	Claim	Reason
1	value of cell 7 at time 1 = 13	if instruction #0 is `addi dst=7 src=3 imm=0` and the PC at time 0 = 0 and value of cell 3 at time 0 = 13, then value of cell 7 at time 1 = 13 (Addi Insn 0)
2	the PC at time 1 = 1	if instruction #0 is `addi dst=7 src=3 imm=0` and the PC at time 0 = 0, then the PC at time 1 = 1 (Pc 0)
3	value of cell 3 at time 1 = 13	if instruction #0 is `addi dst=7 src=3 imm=0` and the PC at time 0 = 0 and value of cell 3 at time 0 = 13, then value of cell 3 at time 1 = 13 (Byte 3 Stays the Same 0)
4	value of cell 4 at time 1 = 11	if instruction #0 is `addi dst=7 src=3 imm=0` and the PC at time 0 = 0 and value of cell 4 at time 0 = 11, then value of cell 4 at time 1 = 11 (Byte 4 Stays the Same 0)
5	value of cell 5 at time 1 = 20	if instruction #0 is `addi dst=7 src=3 imm=0` and the PC at time 0 = 0 and value of cell 5 at time 0 = 20, then value of cell 5 at time 1 = 20 (Byte 5 Stays the Same 0)
6	value of cell 8 at time 2 = 11	if instruction #1 is `addi dst=8 src=4 imm=0` and the PC at time 1 = 1 and value of cell 4 at time 1 = 11, then value of cell 8 at time 2 = 11 (Addi Insn 1)
7	the PC at time 2 = 2	if instruction #1 is `addi dst=8 src=4 imm=0` and the PC at time 1 = 1, then the PC at time 2 = 2 (Pc 1)
8	value of cell 3 at time 2 = 13	if instruction #1 is `addi dst=8 src=4 imm=0` and the PC at time 1 = 1 and value of cell 3 at time 1 = 13, then value of cell 3 at time 2 = 13 (Byte 3 Stays the Same 1)
9	value of cell 4 at time 2 = 11	if instruction #1 is `addi dst=8 src=4 imm=0` and the PC at time 1 = 1 and value of cell 4 at time 1 = 11, then value of cell 4 at time 2 = 11 (Byte 4 Stays the Same 1)
10	value of cell 5 at time 2 = 20	if instruction #1 is `addi dst=8 src=4 imm=0` and the PC at time 1 = 1 and value of cell 5 at time 1 = 20, then value of cell 5 at time 2 = 20 (Byte 5 Stays the Same 1)
11	value of cell 7 at time 2 = 13	if instruction #1 is `addi dst=8 src=4 imm=0` and the PC at time 1 = 1 and value of cell 7 at time 1 = 13, then value of cell 7 at time 2 = 13 (Byte 7 Stays the Same 1)
12	value of cell 9 at time 3 = 20	if instruction #2 is `addi dst=9 src=5 imm=0` and the PC at time 2 = 2 and value of cell 5 at time 2 = 20, then value of cell 9 at time 3 = 20 (Addi Insn 2)
13	the PC at time 3 = 3	if instruction #2 is `addi dst=9 src=5 imm=0` and the PC at time 2 = 2, then the PC at time 3 = 3 (Pc 2)
14	value of cell 3 at time 3 = 13	if instruction #2 is `addi dst=9 src=5 imm=0` and the PC at time 2 = 2 and value of cell 3 at time 2 = 13, then value of cell 3 at time 3 = 13 (Byte 3 Stays the Same 2)
15	value of cell 4 at time 3 = 11	if instruction #2 is `addi dst=9 src=5 imm=0` and the PC at time 2 = 2 and value of cell 4 at time 2 = 11, then value of cell 4 at time 3 = 11 (Byte 4 Stays the Same 2)
16	value of cell 5 at time 3 = 20	if instruction #2 is `addi dst=9 src=5 imm=0` and the PC at time 2 = 2 and value of cell 5 at time 2 = 20, then value of cell 5 at time 3 = 20 (Byte 5 Stays the Same 2)
17	value of cell 7 at time 3 = 13	if instruction #2 is `addi dst=9 src=5 imm=0` and the PC at time 2 = 2 and value of cell 7 at time 2 = 13, then value of cell 7 at time 3 = 13 (Byte 7 Stays the Same 2)
18	value of cell 8 at time 3 = 11	if instruction #2 is `addi dst=9 src=5 imm=0` and the PC at time 2 = 2 and value of cell 8 at time 2 = 11, then value of cell 8 at time 3 = 11 (Byte 8 Stays the Same 2)