Proofs

A proof is a series of claims that lead to a conclusion. Some proofs are conditional, which means that the claims can only be made under certain conditions. Click on a statement to see the proof

Do Line At Unchanged 3
if the following are true:
  • expression state at time 3 = "begin_expr"
  • the line at time 3 = 1

then the line at time 4 = 1


Do Tab At Unchanged 3
if the following are true:
  • expression state at time 3 = "begin_expr"
  • the tab at time 3 = 0

then the tab at time 4 = 0


Do Stack At Unchanged 3
if the following are true:
  • expression state at time 3 = "begin_expr"
  • stack at time 3 = [ ]

then stack at time 4 = [ ]


Do Object Store At Unchanged 3
if the following are true:
  • expression state at time 3 = "begin_expr"
  • Python Object Store at time 3 = [ ]

then Python Object Store at time 4 = [ ]


Do Control Map At Unchanged 3
if the following are true:
  • expression state at time 3 = "begin_expr"
  • Control Map at time 3 = [ ]

then Control Map at time 4 = [ ]


Do Variables At Unchanged 3
if the following are true:
  • expression state at time 3 = "begin_expr"
  • Variables Map at time 3 = [ ]

then Variables Map at time 4 = [ ]


Do Class Defs At Unchanged 3
if the following are true:
  • expression state at time 3 = "begin_expr"
  • Class Map at time 3 = [ ]

then Class Map at time 4 = [ ]


Get New State 4
if expression state at time 4 = "return", then expression state at time 5 = "iterate_args"

Get Return Value 4
if the following are true:
  • expression state at time 4 = "return"
  • Value Stack at time 4 = [ [ ], [ ] ]
  • Return Value at time 4 = 4

then Value Stack at time 5 = [ [ 4, [ ] ], [ ] ]


Do Variables At Unchanged 4
if the following are true:
  • expression state at time 4 = "return"
  • Variables Map at time 4 = [ ]

then Variables Map at time 5 = [ ]


Do Line At Unchanged 4
if the following are true:
  • expression state at time 4 = "return"
  • the line at time 4 = 1

then the line at time 5 = 1


Do Tab At Unchanged 4
if the following are true:
  • expression state at time 4 = "return"
  • the tab at time 4 = 0

then the tab at time 5 = 0


Do Arg Stack At Unchanged 4
if the following are true:
  • expression state at time 4 = "return"
  • arguments stack at time 4 = [ [ 7, [ ] ], [ ] ]

then arguments stack at time 5 = [ [ 7, [ ] ], [ ] ]


Do Parent Stack At Unchanged 4
if the following are true:
  • expression state at time 4 = "return"
  • parent stack at time 4 = [ [4, 7], [ ] ]

then parent stack at time 5 = [ [4, 7], [ ] ]


Do Stack At Unchanged 4
if the following are true:
  • expression state at time 4 = "return"
  • stack at time 4 = [ ]

then stack at time 5 = [ ]


Do Class Defs At Unchanged 4
if the following are true:
  • expression state at time 4 = "return"
  • Class Map at time 4 = [ ]

then Class Map at time 5 = [ ]


Do Object Store At Unchanged 4
if the following are true:
  • expression state at time 4 = "return"
  • Python Object Store at time 4 = [ ]

then Python Object Store at time 5 = [ ]


Do Control Map At Unchanged 4
if the following are true:
  • expression state at time 4 = "return"
  • Control Map at time 4 = [ ]

then Control Map at time 5 = [ ]


Get Iterate Expr 5
if the following are true:
  • expression state at time 5 = "iterate_args"
  • arguments stack at time 5 = [ [ 7, [ ] ], [ ] ]

then the expression at time 6 = 7


Get Iterate Params 5
if the following are true:
  • expression state at time 5 = "iterate_args"
  • arguments stack at time 5 = [ [ 7, [ ] ], [ ] ]

then arguments stack at time 6 = [ [ ], [ ] ]


Get Iterate State 5
if the following are true:
  • expression state at time 5 = "iterate_args"
  • arguments stack at time 5 = [ [ 7, [ ] ], [ ] ]

then expression state at time 6 = "begin_expr"


Get Iterate Parent 5
if the following are true:
  • expression state at time 5 = "iterate_args"
  • arguments stack at time 5 = [ [ 7, [ ] ], [ ] ]
  • parent stack at time 5 = [ [4, 7], [ ] ]

then parent stack at time 6 = [ [4, 7], [ ] ]


Do Value Stack At Unchanged 5
if the following are true:
  • expression state at time 5 = "iterate_args"
  • Value Stack at time 5 = [ [ 4, [ ] ], [ ] ]

then Value Stack at time 6 = [ [ 4, [ ] ], [ ] ]


Do Line At Unchanged 5
if the following are true:
  • expression state at time 5 = "iterate_args"
  • the line at time 5 = 1

then the line at time 6 = 1


Do Tab At Unchanged 5
if the following are true:
  • expression state at time 5 = "iterate_args"
  • the tab at time 5 = 0

then the tab at time 6 = 0


Do Stack At Unchanged 5
if the following are true:
  • expression state at time 5 = "iterate_args"
  • stack at time 5 = [ ]

then stack at time 6 = [ ]


Do Object Store At Unchanged 5
if the following are true:
  • expression state at time 5 = "iterate_args"
  • Python Object Store at time 5 = [ ]

then Python Object Store at time 6 = [ ]


Do Control Map At Unchanged 5
if the following are true:
  • expression state at time 5 = "iterate_args"
  • Control Map at time 5 = [ ]

then Control Map at time 6 = [ ]


Do Variables At Unchanged 5
if the following are true:
  • expression state at time 5 = "iterate_args"
  • Variables Map at time 5 = [ ]

then Variables Map at time 6 = [ ]


Do Class Defs At Unchanged 5
if the following are true:
  • expression state at time 5 = "iterate_args"
  • Class Map at time 5 = [ ]

then Class Map at time 6 = [ ]


Get Begin Expr State 6
if the following are true:
  • the expression at time 6 = 7
  • expression state at time 6 = "begin_expr"
  • 7 is constant
  • parent stack at time 6 = [ [4, 7], [ ] ]

then expression state at time 7 = "return"


Get Begin Expr Value Unchaged 6
if the following are true:
  • the expression at time 6 = 7
  • expression state at time 6 = "begin_expr"
  • 7 is constant
  • Value Stack at time 6 = [ [ 4, [ ] ], [ ] ]

then Value Stack at time 7 = [ [ 4, [ ] ], [ ] ]


Get Begin Expr Params Unchanged6
if the following are true:
  • the expression at time 6 = 7
  • expression state at time 6 = "begin_expr"
  • 7 is constant
  • arguments stack at time 6 = [ [ ], [ ] ]

then arguments stack at time 7 = [ [ ], [ ] ]


Get Begin Expr Return 6
if the following are true:
  • expression state at time 6 = "begin_expr"
  • the expression at time 6 = 7
  • 7 is constant

then Return Value at time 7 = 7


Get Begin Expr Const Parent 6
if the following are true:
  • expression state at time 6 = "begin_expr"
  • the expression at time 6 = 7
  • 7 is constant
  • parent stack at time 6 = [ [4, 7], [ ] ]

then parent stack at time 7 = [ [4, 7], [ ] ]


Do Line At Unchanged 6
if the following are true:
  • expression state at time 6 = "begin_expr"
  • the line at time 6 = 1

then the line at time 7 = 1


Do Tab At Unchanged 6
if the following are true:
  • expression state at time 6 = "begin_expr"
  • the tab at time 6 = 0

then the tab at time 7 = 0


Do Stack At Unchanged 6
if the following are true:
  • expression state at time 6 = "begin_expr"
  • stack at time 6 = [ ]

then stack at time 7 = [ ]


Do Object Store At Unchanged 6
if the following are true:
  • expression state at time 6 = "begin_expr"
  • Python Object Store at time 6 = [ ]

then Python Object Store at time 7 = [ ]


Do Control Map At Unchanged 6
if the following are true:
  • expression state at time 6 = "begin_expr"
  • Control Map at time 6 = [ ]

then Control Map at time 7 = [ ]


Do Variables At Unchanged 6
if the following are true:
  • expression state at time 6 = "begin_expr"
  • Variables Map at time 6 = [ ]

then Variables Map at time 7 = [ ]


Do Class Defs At Unchanged 6
if the following are true:
  • expression state at time 6 = "begin_expr"
  • Class Map at time 6 = [ ]

then Class Map at time 7 = [ ]


Get New State 7
if expression state at time 7 = "return", then expression state at time 8 = "iterate_args"

Get Return Value 7
if the following are true:
  • expression state at time 7 = "return"
  • Value Stack at time 7 = [ [ 4, [ ] ], [ ] ]
  • Return Value at time 7 = 7

then Value Stack at time 8 = [ [ 7, [ 4, [ ] ] ], [ ] ]


Do Variables At Unchanged 7
if the following are true:
  • expression state at time 7 = "return"
  • Variables Map at time 7 = [ ]

then Variables Map at time 8 = [ ]


Do Line At Unchanged 7
if the following are true:
  • expression state at time 7 = "return"
  • the line at time 7 = 1

then the line at time 8 = 1


Do Tab At Unchanged 7
if the following are true:
  • expression state at time 7 = "return"
  • the tab at time 7 = 0

then the tab at time 8 = 0


Do Arg Stack At Unchanged 7
if the following are true:
  • expression state at time 7 = "return"
  • arguments stack at time 7 = [ [ ], [ ] ]

then arguments stack at time 8 = [ [ ], [ ] ]


Do Parent Stack At Unchanged 7
if the following are true:
  • expression state at time 7 = "return"
  • parent stack at time 7 = [ [4, 7], [ ] ]

then parent stack at time 8 = [ [4, 7], [ ] ]


Do Stack At Unchanged 7
if the following are true:
  • expression state at time 7 = "return"
  • stack at time 7 = [ ]

then stack at time 8 = [ ]


Do Class Defs At Unchanged 7
if the following are true:
  • expression state at time 7 = "return"
  • Class Map at time 7 = [ ]

then Class Map at time 8 = [ ]


Do Object Store At Unchanged 7
if the following are true:
  • expression state at time 7 = "return"
  • Python Object Store at time 7 = [ ]

then Python Object Store at time 8 = [ ]


Do Control Map At Unchanged 7
if the following are true:
  • expression state at time 7 = "return"
  • Control Map at time 7 = [ ]

then Control Map at time 8 = [ ]


Get Iterate End State 8
if the following are true:
  • expression state at time 8 = "iterate_args"
  • arguments stack at time 8 = [ [ ], [ ] ]
  • parent stack at time 8 = [ [4, 7], [ ] ]

then expression state at time 9 = "call_function_begin"


Get Iterate End Expr 8
if the following are true:
  • expression state at time 8 = "iterate_args"
  • arguments stack at time 8 = [ [ ], [ ] ]
  • parent stack at time 8 = [ [4, 7], [ ] ]

then the expression at time 9 = [4, 7]


Get Iterate End Parent 8
if the following are true:
  • expression state at time 8 = "iterate_args"
  • arguments stack at time 8 = [ [ ], [ ] ]
  • parent stack at time 8 = [ [4, 7], [ ] ]

then parent stack at time 9 = [ ]


Get Iterate End Params 8
if the following are true:
  • expression state at time 8 = "iterate_args"
  • arguments stack at time 8 = [ [ ], [ ] ]
  • parent stack at time 8 = [ [4, 7], [ ] ]

then arguments stack at time 9 = [ ]


Do Value Stack At Unchanged 8
if the following are true:
  • expression state at time 8 = "iterate_args"
  • Value Stack at time 8 = [ [ 7, [ 4, [ ] ] ], [ ] ]

then Value Stack at time 9 = [ [ 7, [ 4, [ ] ] ], [ ] ]


Do Line At Unchanged 8
if the following are true:
  • expression state at time 8 = "iterate_args"
  • the line at time 8 = 1

then the line at time 9 = 1


Do Tab At Unchanged 8
if the following are true:
  • expression state at time 8 = "iterate_args"
  • the tab at time 8 = 0

then the tab at time 9 = 0


Do Stack At Unchanged 8
if the following are true:
  • expression state at time 8 = "iterate_args"
  • stack at time 8 = [ ]

then stack at time 9 = [ ]


Do Object Store At Unchanged 8
if the following are true:
  • expression state at time 8 = "iterate_args"
  • Python Object Store at time 8 = [ ]

then Python Object Store at time 9 = [ ]


Do Control Map At Unchanged 8
if the following are true:
  • expression state at time 8 = "iterate_args"
  • Control Map at time 8 = [ ]

then Control Map at time 9 = [ ]


Do Variables At Unchanged 8
if the following are true:
  • expression state at time 8 = "iterate_args"
  • Variables Map at time 8 = [ ]

then Variables Map at time 9 = [ ]


Do Class Defs At Unchanged 8
if the following are true:
  • expression state at time 8 = "iterate_args"
  • Class Map at time 8 = [ ]

then Class Map at time 9 = [ ]


Do Len At 9
length of stack [ ] = 0

Do Reverse 9 0
reverse of [ ] = [ ]

Do Reverse 9 1
reverse of [ [4, 7], [ ] ] = [ [4, 7], [ ] ]

Do Reverse 9 2
reverse of [ 7, [ 4, [ ] ] ] = [ 4, [ 7, [ ] ] ]

Do Append 9
result of appending [4, 7] to [ ] = [ [4, 7], [ ] ]

Write Call Function Begin Py List Append 9
if the following are true:
  • expression state at time 9 = "call_function_begin"
  • Value Stack at time 9 = [ [ 7, [ 4, [ ] ] ], [ ] ]
  • the expression at time 9 = [4, 7]
  • Python Object Store at time 9 = [ ]

then Python Object Store at time 10 = [ [4, 7], [ ] ]


Write Call Function Begin Py List Return Val 9
if the following are true:
  • expression state at time 9 = "call_function_begin"
  • Value Stack at time 9 = [ [ 7, [ 4, [ ] ] ], [ ] ]
  • the expression at time 9 = [4, 7]
  • Python Object Store at time 9 = [ ]

then Return Value at time 10 = Python reference 0


Write Call Function Begin Next State 9
if the following are true:
  • expression state at time 9 = "call_function_begin"
  • parent stack at time 9 = [ ]
  • the expression at time 9 = [4, 7]

then expression state at time 10 = "end_expr"


Write Call Function Begin Value Stack 9
if the following are true:
  • expression state at time 9 = "call_function_begin"
  • Value Stack at time 9 = [ [ 7, [ 4, [ ] ] ], [ ] ]
  • the expression at time 9 = [4, 7]

then Value Stack at time 10 = [ ]


Do Arg Stack At Unchanged 9
if the following are true:
  • expression state at time 9 = "call_function_begin"
  • arguments stack at time 9 = [ ]

then arguments stack at time 10 = [ ]


Do Parent Stack At Unchanged 9
if the following are true:
  • expression state at time 9 = "call_function_begin"
  • parent stack at time 9 = [ ]

then parent stack at time 10 = [ ]


Do Control Map At Unchanged 9
if the following are true:
  • expression state at time 9 = "call_function_begin"
  • Control Map at time 9 = [ ]

then Control Map at time 10 = [ ]


Do Variables At Unchanged 9
if the following are true:
  • expression state at time 9 = "call_function_begin"
  • Variables Map at time 9 = [ ]

then Variables Map at time 10 = [ ]


Do Line At Unchanged 9
if the following are true:
  • expression state at time 9 = "call_function_begin"
  • the line at time 9 = 1

then the line at time 10 = 1


Do Tab At Unchanged 9
if the following are true:
  • expression state at time 9 = "call_function_begin"
  • the tab at time 9 = 0

then the tab at time 10 = 0


Do Stack At Unchanged 9
if the following are true:
  • expression state at time 9 = "call_function_begin"
  • stack at time 9 = [ ]

then stack at time 10 = [ ]


Do Class Defs At Unchanged 9
if the following are true:
  • expression state at time 9 = "call_function_begin"
  • Class Map at time 9 = [ ]

then Class Map at time 10 = [ ]


Do Set Key Value 10 0
result of storing (Python reference 0) at key: numbers in map: [ ] = [ entry numbers: (Python reference 0), [ ] ]

Write Assign End Vars 10
if the following are true:
  • the line at time 10 = 1
  • the tab at time 10 = 0
  • statement at line 1, tab 0 = numbers = [4, 7]
  • expression state at time 10 = "end_expr"
  • Variables Map at time 10 = [ ]
  • Return Value at time 10 = Python reference 0

then Variables Map at time 11 = [ entry numbers: (Python reference 0), [ ] ]


Write Increment T And Val Line At 10
if the following are true:
  • the line at time 10 = 1
  • the tab at time 10 = 0
  • statement at line 1, tab 0 = numbers = [4, 7]
  • expression state at time 10 = "end_expr"

then the line at time 11 = 2


Write Stmt Tab At Unchanged Expr10
if the following are true:
  • the line at time 10 = 1
  • the tab at time 10 = 0
  • statement at line 1, tab 0 = numbers = [4, 7]
  • expression state at time 10 = "end_expr"

then the tab at time 11 = 0


Write Stmt Object Store At Unchanged Expr10
if the following are true:
  • the line at time 10 = 1
  • the tab at time 10 = 0
  • statement at line 1, tab 0 = numbers = [4, 7]
  • expression state at time 10 = "end_expr"
  • Python Object Store at time 10 = [ [4, 7], [ ] ]

then Python Object Store at time 11 = [ [4, 7], [ ] ]


Write Assign End Stack 10
if the following are true:
  • the line at time 10 = 1
  • the tab at time 10 = 0
  • statement at line 1, tab 0 = numbers = [4, 7]
  • stack at time 10 = [ ]
  • expression state at time 10 = "end_expr"

then stack at time 11 = [ ]


Write End to Not Expr 10
if expression state at time 10 = "end_expr", then expression state at time 11 = "not_expr"

Write Stmt Control Map At Unchanged 10
if the following are true:
  • the line at time 10 = 1
  • the tab at time 10 = 0
  • statement at line 1, tab 0 = numbers = [4, 7]
  • Control Map at time 10 = [ ]

then Control Map at time 11 = [ ]


Write Stmt Class Defs At Unchanged 10
if the following are true:
  • the line at time 10 = 1
  • the tab at time 10 = 0
  • statement at line 1, tab 0 = numbers = [4, 7]
  • Class Map at time 10 = [ ]

then Class Map at time 11 = [ ]


Do Has Key 11 0
map [ ] contains key 0 = False

Get Substitute Map 11
if Control Map at time 11 = [ ], then map (Control Map at time 11) contains key 0 = False

Get Not Has For At 11
if map (Control Map at time 11) contains key 0 = False, then map (Control Map at time 11) does not contain a for loop entry at line: 2 and tab: 0

Write Set Name Expr At on State 11
if the following are true:
  • the line at time 11 = 2
  • the tab at time 11 = 0
  • statement at line 2, tab 0 = for value in numbers:
  • expression state at time 11 = "not_expr"
  • map (Control Map at time 11) does not contain a for loop entry at line: 2 and tab: 0

then the expression at time 12 = numbers


Write Set Name Expr State At on State 11
if the following are true:
  • the line at time 11 = 2
  • the tab at time 11 = 0
  • statement at line 2, tab 0 = for value in numbers:
  • expression state at time 11 = "not_expr"
  • map (Control Map at time 11) does not contain a for loop entry at line: 2 and tab: 0

then expression state at time 12 = "begin_expr"


Write Set Name Line At on State 11
if the following are true:
  • the line at time 11 = 2
  • the tab at time 11 = 0
  • statement at line 2, tab 0 = for value in numbers:
  • expression state at time 11 = "not_expr"
  • map (Control Map at time 11) does not contain a for loop entry at line: 2 and tab: 0

then the line at time 12 = 2


Write Set Name Tab At on State 11
if the following are true:
  • the line at time 11 = 2
  • the tab at time 11 = 0
  • statement at line 2, tab 0 = for value in numbers:
  • expression state at time 11 = "not_expr"
  • map (Control Map at time 11) does not contain a for loop entry at line: 2 and tab: 0

then the tab at time 12 = 0


Write Set Name Value Stack At on State 11
if the following are true:
  • the line at time 11 = 2
  • the tab at time 11 = 0
  • statement at line 2, tab 0 = for value in numbers:
  • expression state at time 11 = "not_expr"
  • map (Control Map at time 11) does not contain a for loop entry at line: 2 and tab: 0

then Value Stack at time 12 = [ ]


Write Set Name Parent Stack At on State 11
if the following are true:
  • the line at time 11 = 2
  • the tab at time 11 = 0
  • statement at line 2, tab 0 = for value in numbers:
  • expression state at time 11 = "not_expr"
  • map (Control Map at time 11) does not contain a for loop entry at line: 2 and tab: 0

then parent stack at time 12 = [ ]



Pages: 160 161 162 ... 193