Proof: Proof: Multiplication Example

This proof shows that the following program multiplies 7 by 3. More precisely, we prove that

Let's prove the following theorem:

if the following are true:

the PC at time 0 = 0
instruction #0 is addi dst=3 src=0 imm=3
instruction #1 is addi dst=4 src=0 imm=0
instruction #2 is addi dst=5 src=0 imm=0
instruction #3 is addi dst=5 src=5 imm=7
instruction #4 is addi dst=4 src=4 imm=1
instruction #5 is beq left=3 right=4 imm=1
instruction #6 is jump imm=3

then value of cell 5 at time 14 = 21

The program is shown on the simulator below:

Instructions

Memory Cells

Program Counter	Time
0	0

LW Computer Simulator

We are given the program instructions and the PC at time 0. We use this information to make claims about the program's state at time 1. For example:

Since the PC is 0 at time 0 and instruction #0 is an ADDI instruction, at time 1, PC is 1.
Since the PC is 0 at time 0 and instruction #0 is addi dst=3 src=0 imm=3, at time 1, memory cell #3 becomes 3.

Then we use the claims about time 1 to prove claims about time 2, and so on. Eventually, at time 14, we prove that memory cell #5 stores 21 and the program terminates.

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=3 src=0 imm=3`
3	instruction #1 is `addi dst=4 src=0 imm=0`
4	instruction #2 is `addi dst=5 src=0 imm=0`
5	instruction #3 is `addi dst=5 src=5 imm=7`
6	instruction #4 is `addi dst=4 src=4 imm=1`
7	instruction #5 is `beq left=3 right=4 imm=1`
8	instruction #6 is `jump imm=3`

Proof Table

#	Claim	Reason
1	value of cell 3 at time 1 = 3	if instruction #0 is `addi dst=3 src=0 imm=3` and the PC at time 0 = 0, then value of cell 3 at time 1 = 3 (Addi Zero Insn 0)
2	the PC at time 1 = 1	if instruction #0 is `addi dst=3 src=0 imm=3` and the PC at time 0 = 0, then the PC at time 1 = 1 (Pc 0)
3	value of cell 4 at time 2 = 0	if instruction #1 is `addi dst=4 src=0 imm=0` and the PC at time 1 = 1, then value of cell 4 at time 2 = 0 (Addi Zero Insn 1)
4	the PC at time 2 = 2	if instruction #1 is `addi dst=4 src=0 imm=0` and the PC at time 1 = 1, then the PC at time 2 = 2 (Pc 1)
5	value of cell 3 at time 2 = 3	if instruction #1 is `addi dst=4 src=0 imm=0` and the PC at time 1 = 1 and value of cell 3 at time 1 = 3, then value of cell 3 at time 2 = 3 (Byte 3 Stays the Same 1)
6	value of cell 5 at time 3 = 0	if instruction #2 is `addi dst=5 src=0 imm=0` and the PC at time 2 = 2, then value of cell 5 at time 3 = 0 (Addi Zero Insn 2)
7	the PC at time 3 = 3	if instruction #2 is `addi dst=5 src=0 imm=0` and the PC at time 2 = 2, then the PC at time 3 = 3 (Pc 2)
8	value of cell 3 at time 3 = 3	if instruction #2 is `addi dst=5 src=0 imm=0` and the PC at time 2 = 2 and value of cell 3 at time 2 = 3, then value of cell 3 at time 3 = 3 (Byte 3 Stays the Same 2)
9	value of cell 4 at time 3 = 0	if instruction #2 is `addi dst=5 src=0 imm=0` and the PC at time 2 = 2 and value of cell 4 at time 2 = 0, then value of cell 4 at time 3 = 0 (Byte 4 Stays the Same 2)
10	value of cell 5 at time 4 = 7	if instruction #3 is `addi dst=5 src=5 imm=7` and the PC at time 3 = 3 and value of cell 5 at time 3 = 0, then value of cell 5 at time 4 = 7 (Addi Insn 3)
11	the PC at time 4 = 4	if instruction #3 is `addi dst=5 src=5 imm=7` and the PC at time 3 = 3, then the PC at time 4 = 4 (Pc 3)
12	value of cell 3 at time 4 = 3	if instruction #3 is `addi dst=5 src=5 imm=7` and the PC at time 3 = 3 and value of cell 3 at time 3 = 3, then value of cell 3 at time 4 = 3 (Byte 3 Stays the Same 3)
13	value of cell 4 at time 4 = 0	if instruction #3 is `addi dst=5 src=5 imm=7` and the PC at time 3 = 3 and value of cell 4 at time 3 = 0, then value of cell 4 at time 4 = 0 (Byte 4 Stays the Same 3)
14	value of cell 4 at time 5 = 1	if instruction #4 is `addi dst=4 src=4 imm=1` and the PC at time 4 = 4 and value of cell 4 at time 4 = 0, then value of cell 4 at time 5 = 1 (Addi Insn 4)
15	the PC at time 5 = 5	if instruction #4 is `addi dst=4 src=4 imm=1` and the PC at time 4 = 4, then the PC at time 5 = 5 (Pc 4)
16	value of cell 3 at time 5 = 3	if instruction #4 is `addi dst=4 src=4 imm=1` and the PC at time 4 = 4 and value of cell 3 at time 4 = 3, then value of cell 3 at time 5 = 3 (Byte 3 Stays the Same 4)
17	value of cell 5 at time 5 = 7	if instruction #4 is `addi dst=4 src=4 imm=1` and the PC at time 4 = 4 and value of cell 5 at time 4 = 7, then value of cell 5 at time 5 = 7 (Byte 5 Stays the Same 4)
18	the PC at time 6 = 6	if instruction #5 is `beq left=3 right=4 imm=1` and the PC at time 5 = 5 and value of cell 3 at time 5 = 3 and value of cell 4 at time 5 = 1, then the PC at time 6 = 6 (Beq No Branch 5)
19	value of cell 3 at time 6 = 3	if instruction #5 is `beq left=3 right=4 imm=1` and the PC at time 5 = 5 and value of cell 3 at time 5 = 3, then value of cell 3 at time 6 = 3 (Byte 3 Stays the Same 5)
20	value of cell 4 at time 6 = 1	if instruction #5 is `beq left=3 right=4 imm=1` and the PC at time 5 = 5 and value of cell 4 at time 5 = 1, then value of cell 4 at time 6 = 1 (Byte 4 Stays the Same 5)
21	value of cell 5 at time 6 = 7	if instruction #5 is `beq left=3 right=4 imm=1` and the PC at time 5 = 5 and value of cell 5 at time 5 = 7, then value of cell 5 at time 6 = 7 (Byte 5 Stays the Same 5)
22	the PC at time 7 = 3	if instruction #6 is `jump imm=3` and the PC at time 6 = 6, then the PC at time 7 = 3 (Jump Help 6)
23	value of cell 3 at time 7 = 3	if instruction #6 is `jump imm=3` and the PC at time 6 = 6 and value of cell 3 at time 6 = 3, then value of cell 3 at time 7 = 3 (Byte 3 Stays the Same 6)
24	value of cell 4 at time 7 = 1	if instruction #6 is `jump imm=3` and the PC at time 6 = 6 and value of cell 4 at time 6 = 1, then value of cell 4 at time 7 = 1 (Byte 4 Stays the Same 6)
25	value of cell 5 at time 7 = 7	if instruction #6 is `jump imm=3` and the PC at time 6 = 6 and value of cell 5 at time 6 = 7, then value of cell 5 at time 7 = 7 (Byte 5 Stays the Same 6)
26	value of cell 5 at time 8 = 14	if instruction #3 is `addi dst=5 src=5 imm=7` and the PC at time 7 = 3 and value of cell 5 at time 7 = 7, then value of cell 5 at time 8 = 14 (Addi Insn 7)
27	the PC at time 8 = 4	if instruction #3 is `addi dst=5 src=5 imm=7` and the PC at time 7 = 3, then the PC at time 8 = 4 (Pc 7)
28	value of cell 3 at time 8 = 3	if instruction #3 is `addi dst=5 src=5 imm=7` and the PC at time 7 = 3 and value of cell 3 at time 7 = 3, then value of cell 3 at time 8 = 3 (Byte 3 Stays the Same 7)
29	value of cell 4 at time 8 = 1	if instruction #3 is `addi dst=5 src=5 imm=7` and the PC at time 7 = 3 and value of cell 4 at time 7 = 1, then value of cell 4 at time 8 = 1 (Byte 4 Stays the Same 7)
30	value of cell 4 at time 9 = 2	if instruction #4 is `addi dst=4 src=4 imm=1` and the PC at time 8 = 4 and value of cell 4 at time 8 = 1, then value of cell 4 at time 9 = 2 (Addi Insn 8)
31	the PC at time 9 = 5	if instruction #4 is `addi dst=4 src=4 imm=1` and the PC at time 8 = 4, then the PC at time 9 = 5 (Pc 8)
32	value of cell 3 at time 9 = 3	if instruction #4 is `addi dst=4 src=4 imm=1` and the PC at time 8 = 4 and value of cell 3 at time 8 = 3, then value of cell 3 at time 9 = 3 (Byte 3 Stays the Same 8)
33	value of cell 5 at time 9 = 14	if instruction #4 is `addi dst=4 src=4 imm=1` and the PC at time 8 = 4 and value of cell 5 at time 8 = 14, then value of cell 5 at time 9 = 14 (Byte 5 Stays the Same 8)
34	the PC at time 10 = 6	if instruction #5 is `beq left=3 right=4 imm=1` and the PC at time 9 = 5 and value of cell 3 at time 9 = 3 and value of cell 4 at time 9 = 2, then the PC at time 10 = 6 (Beq No Branch 9)
35	value of cell 3 at time 10 = 3	if instruction #5 is `beq left=3 right=4 imm=1` and the PC at time 9 = 5 and value of cell 3 at time 9 = 3, then value of cell 3 at time 10 = 3 (Byte 3 Stays the Same 9)
36	value of cell 4 at time 10 = 2	if instruction #5 is `beq left=3 right=4 imm=1` and the PC at time 9 = 5 and value of cell 4 at time 9 = 2, then value of cell 4 at time 10 = 2 (Byte 4 Stays the Same 9)
37	value of cell 5 at time 10 = 14	if instruction #5 is `beq left=3 right=4 imm=1` and the PC at time 9 = 5 and value of cell 5 at time 9 = 14, then value of cell 5 at time 10 = 14 (Byte 5 Stays the Same 9)
38	the PC at time 11 = 3	if instruction #6 is `jump imm=3` and the PC at time 10 = 6, then the PC at time 11 = 3 (Jump Help 10)
39	value of cell 3 at time 11 = 3	if instruction #6 is `jump imm=3` and the PC at time 10 = 6 and value of cell 3 at time 10 = 3, then value of cell 3 at time 11 = 3 (Byte 3 Stays the Same 10)
40	value of cell 4 at time 11 = 2	if instruction #6 is `jump imm=3` and the PC at time 10 = 6 and value of cell 4 at time 10 = 2, then value of cell 4 at time 11 = 2 (Byte 4 Stays the Same 10)
41	value of cell 5 at time 11 = 14	if instruction #6 is `jump imm=3` and the PC at time 10 = 6 and value of cell 5 at time 10 = 14, then value of cell 5 at time 11 = 14 (Byte 5 Stays the Same 10)
42	value of cell 5 at time 12 = 21	if instruction #3 is `addi dst=5 src=5 imm=7` and the PC at time 11 = 3 and value of cell 5 at time 11 = 14, then value of cell 5 at time 12 = 21 (Addi Insn 11)
43	the PC at time 12 = 4	if instruction #3 is `addi dst=5 src=5 imm=7` and the PC at time 11 = 3, then the PC at time 12 = 4 (Pc 11)
44	value of cell 3 at time 12 = 3	if instruction #3 is `addi dst=5 src=5 imm=7` and the PC at time 11 = 3 and value of cell 3 at time 11 = 3, then value of cell 3 at time 12 = 3 (Byte 3 Stays the Same 11)
45	value of cell 4 at time 12 = 2	if instruction #3 is `addi dst=5 src=5 imm=7` and the PC at time 11 = 3 and value of cell 4 at time 11 = 2, then value of cell 4 at time 12 = 2 (Byte 4 Stays the Same 11)
46	value of cell 4 at time 13 = 3	if instruction #4 is `addi dst=4 src=4 imm=1` and the PC at time 12 = 4 and value of cell 4 at time 12 = 2, then value of cell 4 at time 13 = 3 (Addi Insn 12)
47	the PC at time 13 = 5	if instruction #4 is `addi dst=4 src=4 imm=1` and the PC at time 12 = 4, then the PC at time 13 = 5 (Pc 12)
48	value of cell 3 at time 13 = 3	if instruction #4 is `addi dst=4 src=4 imm=1` and the PC at time 12 = 4 and value of cell 3 at time 12 = 3, then value of cell 3 at time 13 = 3 (Byte 3 Stays the Same 12)
49	value of cell 5 at time 13 = 21	if instruction #4 is `addi dst=4 src=4 imm=1` and the PC at time 12 = 4 and value of cell 5 at time 12 = 21, then value of cell 5 at time 13 = 21 (Byte 5 Stays the Same 12)
50	the PC at time 14 = 7	if instruction #5 is `beq left=3 right=4 imm=1` and the PC at time 13 = 5 and value of cell 3 at time 13 = 3 and value of cell 4 at time 13 = 3, then the PC at time 14 = 7 (Beq Branch)
51	value of cell 3 at time 14 = 3	if instruction #5 is `beq left=3 right=4 imm=1` and the PC at time 13 = 5 and value of cell 3 at time 13 = 3, then value of cell 3 at time 14 = 3 (Byte 3 Stays the Same 13)
52	value of cell 4 at time 14 = 3	if instruction #5 is `beq left=3 right=4 imm=1` and the PC at time 13 = 5 and value of cell 4 at time 13 = 3, then value of cell 4 at time 14 = 3 (Byte 4 Stays the Same 13)
53	value of cell 5 at time 14 = 21	if instruction #5 is `beq left=3 right=4 imm=1` and the PC at time 13 = 5 and value of cell 5 at time 13 = 21, then value of cell 5 at time 14 = 21 (Byte 5 Stays the Same 13)

Previous Lesson

Comments

Please log in to add comments