Proof: While Test True Store Example

Let's prove the following theorem:

if the following are true:

the line at time 11 = 2
the tab at time 11 = 0
statement at line 2, tab 0 = while __lt__(a, 2):
expression state at time 11 = "end_expr"
Return Value at time 11 = True
Control Map at time 11 = [ ]

then Control Map at time 12 = [ entry 0: (pair ("while", 2)), [ ] ]

This example shows that if there is a "while" statement at the current line number 2 and current tab number 0, and test is True, then a new entry 0:pair("while":2) is stored in the "Control" map

Code Editor

LW Python State

Current Line

Current Tab

Time

LW Python Simulator

The proof uses the While Test True Store Property to show that a new pair is added to the "Control" map, then some algebra to simplify the time to 12.

Proof:

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

Given

1	the line at time 11 = 2
2	the tab at time 11 = 0
3	statement at line 2, tab 0 = `while __lt__(a, 2):`
4	expression state at time 11 = "end_expr"
5	Return Value at time 11 = True
6	Control Map at time 11 = [ ]

Proof Table

#	Claim	Reason
1	Control Map at time (11 + 1) = result of storing (pair ("while", 2)) at key: 0 in map: (Control Map at time 11)	if the line at time 11 = 2 and the tab at time 11 = 0 and statement at line 2, tab 0 = `while __lt__(a, 2):` and expression state at time 11 = "end_expr" and Return Value at time 11 = True, then Control Map at time (11 + 1) = result of storing (pair ("while", 2)) at key: 0 in map: (Control Map at time 11) (While Go (3))
2	result of storing (pair ("while", 2)) at key: 0 in map: (Control Map at time 11) = result of storing (pair ("while", 2)) at key: 0 in map: [ ]	if Control Map at time 11 = [ ], then result of storing (pair ("while", 2)) at key: 0 in map: (Control Map at time 11) = result of storing (pair ("while", 2)) at key: 0 in map: [ ] (Substitution)
3	result of storing (pair ("while", 2)) at key: 0 in map: [ ] = [ entry 0: (pair ("while", 2)), [ ] ]	result of storing (pair ("while", 2)) at key: 0 in map: [ ] = [ entry 0: (pair ("while", 2)), [ ] ] (do_set_key_value_11_0)
4	result of storing (pair ("while", 2)) at key: 0 in map: (Control Map at time 11) = [ entry 0: (pair ("while", 2)), [ ] ]	if result of storing (pair ("while", 2)) at key: 0 in map: (Control Map at time 11) = result of storing (pair ("while", 2)) at key: 0 in map: [ ] and result of storing (pair ("while", 2)) at key: 0 in map: [ ] = [ entry 0: (pair ("while", 2)), [ ] ], then result of storing (pair ("while", 2)) at key: 0 in map: (Control Map at time 11) = [ entry 0: (pair ("while", 2)), [ ] ] (Transitive Property of Equality)
5	Control Map at time (11 + 1) = [ entry 0: (pair ("while", 2)), [ ] ]	if Control Map at time (11 + 1) = result of storing (pair ("while", 2)) at key: 0 in map: (Control Map at time 11) and result of storing (pair ("while", 2)) at key: 0 in map: (Control Map at time 11) = [ entry 0: (pair ("while", 2)), [ ] ], then Control Map at time (11 + 1) = [ entry 0: (pair ("while", 2)), [ ] ] (Transitive Property of Equality)
6	11 + 1 = 12	11 + 1 = 12 (Fixed Value Statement)
7	Control Map at time (11 + 1) = Control Map at time 12	if 11 + 1 = 12, then Control Map at time (11 + 1) = Control Map at time 12 (Substitution)
8	Control Map at time 12 = [ entry 0: (pair ("while", 2)), [ ] ]	if Control Map at time (11 + 1) = Control Map at time 12 and Control Map at time (11 + 1) = [ entry 0: (pair ("while", 2)), [ ] ], then Control Map at time 12 = [ entry 0: (pair ("while", 2)), [ ] ] (Transitive Property of Equality Variation 2)

Comments

Please log in to add comments