Proof: Assign Constant Example

Let's prove the following theorem:

if the following are true:

the line at time 0 = 1
the tab at time 0 = 0
statement at line 1, tab 0 = c = 16
16 is constant
Variables Map at time 0 = [ ]

then Variables Map at time 1 = [ entry c: 16, [ ] ]

Code Editor

LW Python State

Current Line

Current Tab

Time

LW Python Simulator

The variables map is initially empty. In steps 6 to 10, we prove that after we set key c to value 16 in the variables map, the variables map contains 1 entry:

c: 16

Then we prove that the variables map at time 0 + 1 is equal to variables map at time 1.

Proof:

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

Given

1	the line at time 0 = 1
2	the tab at time 0 = 0
3	statement at line 1, tab 0 = `c = 16`
4	16 is constant
5	Variables Map at time 0 = [ ]

Proof Table

#	Claim	Reason
1	Variables Map at time (0 + 1) = result of storing 16 at key: c in map: (Variables Map at time 0)	if the line at time 0 = 1 and the tab at time 0 = 0 and statement at line 1, tab 0 = `c = 16` and 16 is constant, then Variables Map at time (0 + 1) = result of storing 16 at key: c in map: (Variables Map at time 0) (Constant Assignment Property)
2	result of storing 16 at key: c in map: (Variables Map at time 0) = result of storing 16 at key: c in map: [ ]	if Variables Map at time 0 = [ ], then result of storing 16 at key: c in map: (Variables Map at time 0) = result of storing 16 at key: c in map: [ ] (Substitution)
3	result of storing 16 at key: c in map: [ ] = [ entry c: 16, [ ] ]	result of storing 16 at key: c in map: [ ] = [ entry c: 16, [ ] ] (do_set_key_value_0_0)
4	result of storing 16 at key: c in map: (Variables Map at time 0) = [ entry c: 16, [ ] ]	if result of storing 16 at key: c in map: (Variables Map at time 0) = result of storing 16 at key: c in map: [ ] and result of storing 16 at key: c in map: [ ] = [ entry c: 16, [ ] ], then result of storing 16 at key: c in map: (Variables Map at time 0) = [ entry c: 16, [ ] ] (Transitive Property of Equality)
5	Variables Map at time (0 + 1) = [ entry c: 16, [ ] ]	if Variables Map at time (0 + 1) = result of storing 16 at key: c in map: (Variables Map at time 0) and result of storing 16 at key: c in map: (Variables Map at time 0) = [ entry c: 16, [ ] ], then Variables Map at time (0 + 1) = [ entry c: 16, [ ] ] (Transitive Property of Equality)
6	0 + 1 = 1	0 + 1 = 1 (Fixed Value Statement)
7	Variables Map at time (0 + 1) = Variables Map at time 1	if 0 + 1 = 1, then Variables Map at time (0 + 1) = Variables Map at time 1 (Substitution)
8	Variables Map at time 1 = [ entry c: 16, [ ] ]	if Variables Map at time (0 + 1) = Variables Map at time 1 and Variables Map at time (0 + 1) = [ entry c: 16, [ ] ], then Variables Map at time 1 = [ entry c: 16, [ ] ] (Transitive Property of Equality Variation 2)

Comments

Please log in to add comments