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 Object Store At Unchanged 29
if the following are true:
  • expression state at time 29 = "iterate_args"
  • Python Object Store at time 29 = [ {"ES": "Spain", "MX": "Mexico"}, [ ] ]

then Python Object Store at time 30 = [ {"ES": "Spain", "MX": "Mexico"}, [ ] ]


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

then Control Map at time 30 = [ ]


Do Variables At Unchanged 29
if the following are true:
  • expression state at time 29 = "iterate_args"
  • Variables Map at time 29 = [ entry locations: (Python reference 0), [ ] ]

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


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

then Class Map at time 30 = [ ]


Do Get Key Value 30 0
value at locations in map [ entry locations: (Python reference 0), [ ] ] = Python reference 0

Do Variables At Unchanged 30
if the following are true:
  • expression state at time 30 = "begin_expr"
  • Variables Map at time 30 = [ entry locations: (Python reference 0), [ ] ]

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


Get Begin Expr State Name 30
if the following are true:
  • the expression at time 30 = locations
  • expression state at time 30 = "begin_expr"
  • locations is a variable
  • parent stack at time 30 = [ __getitem__(locations, "ES"), [ ] ]

then expression state at time 31 = "return"


Get Begin Expr Value Unchaged Name 30
if the following are true:
  • the expression at time 30 = locations
  • expression state at time 30 = "begin_expr"
  • locations is a variable
  • Value Stack at time 30 = [ [ ], [ ] ]

then Value Stack at time 31 = [ [ ], [ ] ]


Get Begin Expr Params Unchanged Name30
if the following are true:
  • the expression at time 30 = locations
  • expression state at time 30 = "begin_expr"
  • locations is a variable
  • arguments stack at time 30 = [ [ "ES", [ ] ], [ ] ]

then arguments stack at time 31 = [ [ "ES", [ ] ], [ ] ]


Get Begin Expr Return Name 30
if the following are true:
  • expression state at time 30 = "begin_expr"
  • the expression at time 30 = locations
  • locations is a variable
  • Variables Map at time 30 = [ entry locations: (Python reference 0), [ ] ]

then Return Value at time 31 = Python reference 0


Get Begin Expr Parent Name 30
if the following are true:
  • expression state at time 30 = "begin_expr"
  • the expression at time 30 = locations
  • locations is a variable
  • parent stack at time 30 = [ __getitem__(locations, "ES"), [ ] ]

then parent stack at time 31 = [ __getitem__(locations, "ES"), [ ] ]


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

then the line at time 31 = 2


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

then the tab at time 31 = 0


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

then stack at time 31 = [ ]


Do Object Store At Unchanged 30
if the following are true:
  • expression state at time 30 = "begin_expr"
  • Python Object Store at time 30 = [ {"ES": "Spain", "MX": "Mexico"}, [ ] ]

then Python Object Store at time 31 = [ {"ES": "Spain", "MX": "Mexico"}, [ ] ]


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

then Control Map at time 31 = [ ]


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

then Class Map at time 31 = [ ]


Get New State 31
if expression state at time 31 = "return", then expression state at time 32 = "iterate_args"

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

then Value Stack at time 32 = [ [ Python reference 0, [ ] ], [ ] ]


Do Variables At Unchanged 31
if the following are true:
  • expression state at time 31 = "return"
  • Variables Map at time 31 = [ entry locations: (Python reference 0), [ ] ]

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


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

then the line at time 32 = 2


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

then the tab at time 32 = 0


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

then arguments stack at time 32 = [ [ "ES", [ ] ], [ ] ]


Do Parent Stack At Unchanged 31
if the following are true:
  • expression state at time 31 = "return"
  • parent stack at time 31 = [ __getitem__(locations, "ES"), [ ] ]

then parent stack at time 32 = [ __getitem__(locations, "ES"), [ ] ]


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

then stack at time 32 = [ ]


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

then Class Map at time 32 = [ ]


Do Object Store At Unchanged 31
if the following are true:
  • expression state at time 31 = "return"
  • Python Object Store at time 31 = [ {"ES": "Spain", "MX": "Mexico"}, [ ] ]

then Python Object Store at time 32 = [ {"ES": "Spain", "MX": "Mexico"}, [ ] ]


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

then Control Map at time 32 = [ ]


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

then the expression at time 33 = "ES"


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

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


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

then expression state at time 33 = "begin_expr"


Get Iterate Parent 32
if the following are true:
  • expression state at time 32 = "iterate_args"
  • arguments stack at time 32 = [ [ "ES", [ ] ], [ ] ]
  • parent stack at time 32 = [ __getitem__(locations, "ES"), [ ] ]

then parent stack at time 33 = [ __getitem__(locations, "ES"), [ ] ]


Do Value Stack At Unchanged 32
if the following are true:
  • expression state at time 32 = "iterate_args"
  • Value Stack at time 32 = [ [ Python reference 0, [ ] ], [ ] ]

then Value Stack at time 33 = [ [ Python reference 0, [ ] ], [ ] ]


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

then the line at time 33 = 2


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

then the tab at time 33 = 0


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

then stack at time 33 = [ ]


Do Object Store At Unchanged 32
if the following are true:
  • expression state at time 32 = "iterate_args"
  • Python Object Store at time 32 = [ {"ES": "Spain", "MX": "Mexico"}, [ ] ]

then Python Object Store at time 33 = [ {"ES": "Spain", "MX": "Mexico"}, [ ] ]


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

then Control Map at time 33 = [ ]


Do Variables At Unchanged 32
if the following are true:
  • expression state at time 32 = "iterate_args"
  • Variables Map at time 32 = [ entry locations: (Python reference 0), [ ] ]

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


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

then Class Map at time 33 = [ ]


Get Begin Expr State 33
if the following are true:
  • the expression at time 33 = "ES"
  • expression state at time 33 = "begin_expr"
  • "ES" is constant
  • parent stack at time 33 = [ __getitem__(locations, "ES"), [ ] ]

then expression state at time 34 = "return"


Get Begin Expr Value Unchaged 33
if the following are true:
  • the expression at time 33 = "ES"
  • expression state at time 33 = "begin_expr"
  • "ES" is constant
  • Value Stack at time 33 = [ [ Python reference 0, [ ] ], [ ] ]

then Value Stack at time 34 = [ [ Python reference 0, [ ] ], [ ] ]


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

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


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

then Return Value at time 34 = "ES"


Get Begin Expr Const Parent 33
if the following are true:
  • expression state at time 33 = "begin_expr"
  • the expression at time 33 = "ES"
  • "ES" is constant
  • parent stack at time 33 = [ __getitem__(locations, "ES"), [ ] ]

then parent stack at time 34 = [ __getitem__(locations, "ES"), [ ] ]


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

then the line at time 34 = 2


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

then the tab at time 34 = 0


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

then stack at time 34 = [ ]


Do Object Store At Unchanged 33
if the following are true:
  • expression state at time 33 = "begin_expr"
  • Python Object Store at time 33 = [ {"ES": "Spain", "MX": "Mexico"}, [ ] ]

then Python Object Store at time 34 = [ {"ES": "Spain", "MX": "Mexico"}, [ ] ]


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

then Control Map at time 34 = [ ]


Do Variables At Unchanged 33
if the following are true:
  • expression state at time 33 = "begin_expr"
  • Variables Map at time 33 = [ entry locations: (Python reference 0), [ ] ]

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


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

then Class Map at time 34 = [ ]


Get New State 34
if expression state at time 34 = "return", then expression state at time 35 = "iterate_args"

Get Return Value 34
if the following are true:
  • expression state at time 34 = "return"
  • Value Stack at time 34 = [ [ Python reference 0, [ ] ], [ ] ]
  • Return Value at time 34 = "ES"

then Value Stack at time 35 = [ [ "ES", [ Python reference 0, [ ] ] ], [ ] ]


Do Variables At Unchanged 34
if the following are true:
  • expression state at time 34 = "return"
  • Variables Map at time 34 = [ entry locations: (Python reference 0), [ ] ]

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


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

then the line at time 35 = 2


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

then the tab at time 35 = 0


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

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


Do Parent Stack At Unchanged 34
if the following are true:
  • expression state at time 34 = "return"
  • parent stack at time 34 = [ __getitem__(locations, "ES"), [ ] ]

then parent stack at time 35 = [ __getitem__(locations, "ES"), [ ] ]


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

then stack at time 35 = [ ]


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

then Class Map at time 35 = [ ]


Do Object Store At Unchanged 34
if the following are true:
  • expression state at time 34 = "return"
  • Python Object Store at time 34 = [ {"ES": "Spain", "MX": "Mexico"}, [ ] ]

then Python Object Store at time 35 = [ {"ES": "Spain", "MX": "Mexico"}, [ ] ]


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

then Control Map at time 35 = [ ]


Get Iterate End State 35
if the following are true:
  • expression state at time 35 = "iterate_args"
  • arguments stack at time 35 = [ [ ], [ ] ]
  • parent stack at time 35 = [ __getitem__(locations, "ES"), [ ] ]

then expression state at time 36 = "call_function_begin"


Get Iterate End Expr 35
if the following are true:
  • expression state at time 35 = "iterate_args"
  • arguments stack at time 35 = [ [ ], [ ] ]
  • parent stack at time 35 = [ __getitem__(locations, "ES"), [ ] ]

then the expression at time 36 = __getitem__(locations, "ES")


Get Iterate End Parent 35
if the following are true:
  • expression state at time 35 = "iterate_args"
  • arguments stack at time 35 = [ [ ], [ ] ]
  • parent stack at time 35 = [ __getitem__(locations, "ES"), [ ] ]

then parent stack at time 36 = [ ]


Get Iterate End Params 35
if the following are true:
  • expression state at time 35 = "iterate_args"
  • arguments stack at time 35 = [ [ ], [ ] ]
  • parent stack at time 35 = [ __getitem__(locations, "ES"), [ ] ]

then arguments stack at time 36 = [ ]


Do Value Stack At Unchanged 35
if the following are true:
  • expression state at time 35 = "iterate_args"
  • Value Stack at time 35 = [ [ "ES", [ Python reference 0, [ ] ] ], [ ] ]

then Value Stack at time 36 = [ [ "ES", [ Python reference 0, [ ] ] ], [ ] ]


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

then the line at time 36 = 2


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

then the tab at time 36 = 0


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

then stack at time 36 = [ ]


Do Object Store At Unchanged 35
if the following are true:
  • expression state at time 35 = "iterate_args"
  • Python Object Store at time 35 = [ {"ES": "Spain", "MX": "Mexico"}, [ ] ]

then Python Object Store at time 36 = [ {"ES": "Spain", "MX": "Mexico"}, [ ] ]


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

then Control Map at time 36 = [ ]


Do Variables At Unchanged 35
if the following are true:
  • expression state at time 35 = "iterate_args"
  • Variables Map at time 35 = [ entry locations: (Python reference 0), [ ] ]

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


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

then Class Map at time 36 = [ ]


Write Element At Object Store 36
if Python Object Store at time 36 = [ {"ES": "Spain", "MX": "Mexico"}, [ ] ], then the element at index 0 of stack (Python Object Store at time 36) = {"ES": "Spain", "MX": "Mexico"}

Do Get Key Value 36 0
value at "ES" in map [ entry "ES": "Spain", [ entry "MX": "Mexico", [ ] ] ] = "Spain"

Get Dictionary Item Property Example
if the following are true:
  • expression state at time 36 = "call_function_begin"
  • Value Stack at time 36 = [ [ "ES", [ Python reference 0, [ ] ] ], [ ] ]
  • the expression at time 36 = __getitem__(locations, "ES")
  • the element at index 0 of stack (Python Object Store at time 36) = {"ES": "Spain", "MX": "Mexico"}

then Return Value at time 37 = "Spain"


Do Object Store At Unchanged 36
if the following are true:
  • expression state at time 36 = "call_function_begin"
  • the expression at time 36 = __getitem__(locations, "ES")
  • Python Object Store at time 36 = [ {"ES": "Spain", "MX": "Mexico"}, [ ] ]

then Python Object Store at time 37 = [ {"ES": "Spain", "MX": "Mexico"}, [ ] ]


Write Call Function Begin Next State 36
if the following are true:
  • expression state at time 36 = "call_function_begin"
  • parent stack at time 36 = [ ]
  • the expression at time 36 = __getitem__(locations, "ES")

then expression state at time 37 = "end_expr"


Write Call Function Begin Value Stack 36
if the following are true:
  • expression state at time 36 = "call_function_begin"
  • Value Stack at time 36 = [ [ "ES", [ Python reference 0, [ ] ] ], [ ] ]
  • the expression at time 36 = __getitem__(locations, "ES")

then Value Stack at time 37 = [ ]


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

then arguments stack at time 37 = [ ]


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

then parent stack at time 37 = [ ]


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

then Control Map at time 37 = [ ]


Do Variables At Unchanged 36
if the following are true:
  • expression state at time 36 = "call_function_begin"
  • Variables Map at time 36 = [ entry locations: (Python reference 0), [ ] ]

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


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

then the line at time 37 = 2


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

then the tab at time 37 = 0


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

then stack at time 37 = [ ]


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

then Class Map at time 37 = [ ]


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

Write Increment T And Val Line At 37
if the following are true:
  • the line at time 37 = 2
  • the tab at time 37 = 0
  • statement at line 2, tab 0 = __getitem__(locations, "ES")
  • expression state at time 37 = "end_expr"

then the line at time 38 = 3


Write Stmt Tab At Unchanged Expr37
if the following are true:
  • the line at time 37 = 2
  • the tab at time 37 = 0
  • statement at line 2, tab 0 = __getitem__(locations, "ES")
  • expression state at time 37 = "end_expr"

then the tab at time 38 = 0


Write Stmt Object Store At Unchanged Expr37
if the following are true:
  • the line at time 37 = 2
  • the tab at time 37 = 0
  • statement at line 2, tab 0 = __getitem__(locations, "ES")
  • expression state at time 37 = "end_expr"
  • Python Object Store at time 37 = [ {"ES": "Spain", "MX": "Mexico"}, [ ] ]

then Python Object Store at time 38 = [ {"ES": "Spain", "MX": "Mexico"}, [ ] ]


Write Stmt Stack At Unchanged Expr37
if the following are true:
  • the line at time 37 = 2
  • the tab at time 37 = 0
  • statement at line 2, tab 0 = __getitem__(locations, "ES")
  • expression state at time 37 = "end_expr"
  • stack at time 37 = [ ]

then stack at time 38 = [ ]


Write Stmt Variables At Unchanged Expr37
if the following are true:
  • the line at time 37 = 2
  • the tab at time 37 = 0
  • statement at line 2, tab 0 = __getitem__(locations, "ES")
  • expression state at time 37 = "end_expr"
  • Variables Map at time 37 = [ entry locations: (Python reference 0), [ ] ]

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


Write Stmt Control Map At Unchanged 37
if the following are true:
  • the line at time 37 = 2
  • the tab at time 37 = 0
  • statement at line 2, tab 0 = __getitem__(locations, "ES")
  • Control Map at time 37 = [ ]

then Control Map at time 38 = [ ]


Write Stmt Class Defs At Unchanged 37
if the following are true:
  • the line at time 37 = 2
  • the tab at time 37 = 0
  • statement at line 2, tab 0 = __getitem__(locations, "ES")
  • Class Map at time 37 = [ ]

then Class Map at time 38 = [ ]


Write Set Name Expr At on State 0
if the following are true:
  • the line at time 0 = 1
  • the tab at time 0 = 0
  • statement at line 1, tab 0 = locations = {"ES": "Estonia", "MX": "Mexico"}
  • expression state at time 0 = "not_expr"

then the expression at time 1 = {"ES": "Estonia", "MX": "Mexico"}


Write Set Name Expr State At on State 0
if the following are true:
  • the line at time 0 = 1
  • the tab at time 0 = 0
  • statement at line 1, tab 0 = locations = {"ES": "Estonia", "MX": "Mexico"}
  • expression state at time 0 = "not_expr"

then expression state at time 1 = "begin_expr"


Write Set Name Line At on State 0
if the following are true:
  • the line at time 0 = 1
  • the tab at time 0 = 0
  • statement at line 1, tab 0 = locations = {"ES": "Estonia", "MX": "Mexico"}
  • expression state at time 0 = "not_expr"

then the line at time 1 = 1



Pages: 147 148 149 ... 193