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 Control Map At Unchanged 38
if the following are true:
  • expression state at time 38 = "iterate_args"
  • Control Map at time 38 = [ entry 0: (pair ("class", "Dog")), [ ] ]

then Control Map at time 39 = [ entry 0: (pair ("class", "Dog")), [ ] ]


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

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


Do Class Defs At Unchanged 38
if the following are true:
  • expression state at time 38 = "iterate_args"
  • Class Map at time 38 = [ entry "Animal": [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ entry "move": [ entry "params": [ self, [ ] ], [ entry "line": 5, [ ] ] ], [ ] ] ], [ entry "line": 1, [ ] ] ] ], [ entry "Dog": [ entry "bases": [ "Animal", [ ] ], [ entry "methods": [ entry "jump": [ entry "params": [ self, [ ] ], [ entry "line": 8, [ ] ] ], [ ] ], [ entry "line": 7, [ ] ] ] ], [ ] ] ]

then Class Map at time 39 = [ entry "Animal": [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ entry "move": [ entry "params": [ self, [ ] ], [ entry "line": 5, [ ] ] ], [ ] ] ], [ entry "line": 1, [ ] ] ] ], [ entry "Dog": [ entry "bases": [ "Animal", [ ] ], [ entry "methods": [ entry "jump": [ entry "params": [ self, [ ] ], [ entry "line": 8, [ ] ] ], [ ] ], [ entry "line": 7, [ ] ] ] ], [ ] ] ]


Do Expr At Unchanged 39
if the following are true:
  • expression state at time 39 = "call_function_begin"
  • the expression at time 39 = joe.move()

then the expression at time 40 = joe.move()


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

Get Key Value Variables At 39
if Variables Map at time 39 = [ entry joe: (Python reference 0), [ ] ], then value at joe in map (Variables Map at time 39) = Python reference 0

Do Element At 39 0
the element at index 0 of stack [ Python object: [ entry "__class_name__": "Dog", [ entry "x": 0, [ entry "y": 0, [ ] ] ] ], [ ] ] = Python object: [ entry "__class_name__": "Dog", [ entry "x": 0, [ entry "y": 0, [ ] ] ] ]

Write Element At Object Store 39
if Python Object Store at time 39 = [ Python object: [ entry "__class_name__": "Dog", [ entry "x": 0, [ entry "y": 0, [ ] ] ] ], [ ] ], then the element at index 0 of stack (Python Object Store at time 39) = Python object: [ entry "__class_name__": "Dog", [ entry "x": 0, [ entry "y": 0, [ ] ] ] ]

Do Has Key 39 0
map [ entry "Animal": [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ entry "move": [ entry "params": [ self, [ ] ], [ entry "line": 5, [ ] ] ], [ ] ] ], [ entry "line": 1, [ ] ] ] ], [ entry "Dog": [ entry "bases": [ "Animal", [ ] ], [ entry "methods": [ entry "jump": [ entry "params": [ self, [ ] ], [ entry "line": 8, [ ] ] ], [ ] ], [ entry "line": 7, [ ] ] ] ], [ ] ] ] contains key "Dog" = True

Write Call Function Begin Method Call Has 39
if Class Map at time 39 = [ entry "Animal": [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ entry "move": [ entry "params": [ self, [ ] ], [ entry "line": 5, [ ] ] ], [ ] ] ], [ entry "line": 1, [ ] ] ] ], [ entry "Dog": [ entry "bases": [ "Animal", [ ] ], [ entry "methods": [ entry "jump": [ entry "params": [ self, [ ] ], [ entry "line": 8, [ ] ] ], [ ] ], [ entry "line": 7, [ ] ] ] ], [ ] ] ], then map (Class Map at time 39) contains key "Dog" = True

Write Call Function Begin Method Call State 39
if the following are true:
  • expression state at time 39 = "call_function_begin"
  • the expression at time 39 = joe.move()
  • value at joe in map (Variables Map at time 39) = Python reference 0
  • the element at index 0 of stack (Python Object Store at time 39) = Python object: [ entry "__class_name__": "Dog", [ entry "x": 0, [ entry "y": 0, [ ] ] ] ]
  • map (Class Map at time 39) contains key "Dog" = True

then expression state at time 40 = "call_build_args"


Write Call Function Begin Tmp Vars 39
if expression state at time 39 = "call_function_begin", then Function Variables Map at time 40 = [ ]

Do Get Key Value 39 4
value at "Animal" in map [ entry "Animal": [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ entry "move": [ entry "params": [ self, [ ] ], [ entry "line": 5, [ ] ] ], [ ] ] ], [ entry "line": 1, [ ] ] ] ], [ entry "Dog": [ entry "bases": [ "Animal", [ ] ], [ entry "methods": [ entry "jump": [ entry "params": [ self, [ ] ], [ entry "line": 8, [ ] ] ], [ ] ], [ entry "line": 7, [ ] ] ] ], [ ] ] ] = [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ entry "move": [ entry "params": [ self, [ ] ], [ entry "line": 5, [ ] ] ], [ ] ] ], [ entry "line": 1, [ ] ] ] ]

Do Get Key Value 39 1
value at "methods" in map [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ entry "move": [ entry "params": [ self, [ ] ], [ entry "line": 5, [ ] ] ], [ ] ] ], [ entry "line": 1, [ ] ] ] ] = [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ entry "move": [ entry "params": [ self, [ ] ], [ entry "line": 5, [ ] ] ], [ ] ] ]

Do Get Key Value 39 2
value at "move" in map [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ entry "move": [ entry "params": [ self, [ ] ], [ entry "line": 5, [ ] ] ], [ ] ] ] = [ entry "params": [ self, [ ] ], [ entry "line": 5, [ ] ] ]

Do Get Key Value 39 3
value at "params" in map [ entry "params": [ self, [ ] ], [ entry "line": 5, [ ] ] ] = [ self, [ ] ]

Prove Find Method Def 39
definition of method "move" of class "Animal" in [ entry "Animal": [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ entry "move": [ entry "params": [ self, [ ] ], [ entry "line": 5, [ ] ] ], [ ] ] ], [ entry "line": 1, [ ] ] ] ], [ entry "Dog": [ entry "bases": [ "Animal", [ ] ], [ entry "methods": [ entry "jump": [ entry "params": [ self, [ ] ], [ entry "line": 8, [ ] ] ], [ ] ], [ entry "line": 7, [ ] ] ] ], [ ] ] ] = [ entry "params": [ self, [ ] ], [ entry "line": 5, [ ] ] ]

Do Get Key Value 39 100
value at "Dog" in map [ entry "Animal": [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ entry "move": [ entry "params": [ self, [ ] ], [ entry "line": 5, [ ] ] ], [ ] ] ], [ entry "line": 1, [ ] ] ] ], [ entry "Dog": [ entry "bases": [ "Animal", [ ] ], [ entry "methods": [ entry "jump": [ entry "params": [ self, [ ] ], [ entry "line": 8, [ ] ] ], [ ] ], [ entry "line": 7, [ ] ] ] ], [ ] ] ] = [ entry "bases": [ "Animal", [ ] ], [ entry "methods": [ entry "jump": [ entry "params": [ self, [ ] ], [ entry "line": 8, [ ] ] ], [ ] ], [ entry "line": 7, [ ] ] ] ]

Do Get Key Value 39 101
value at "methods" in map [ entry "bases": [ "Animal", [ ] ], [ entry "methods": [ entry "jump": [ entry "params": [ self, [ ] ], [ entry "line": 8, [ ] ] ], [ ] ], [ entry "line": 7, [ ] ] ] ] = [ entry "jump": [ entry "params": [ self, [ ] ], [ entry "line": 8, [ ] ] ], [ ] ]

Do Has Key 39 100
map [ entry "jump": [ entry "params": [ self, [ ] ], [ entry "line": 8, [ ] ] ], [ ] ] contains key "move" = False

Do Get Key Value 39 102
value at "bases" in map [ entry "bases": [ "Animal", [ ] ], [ entry "methods": [ entry "jump": [ entry "params": [ self, [ ] ], [ entry "line": 8, [ ] ] ], [ ] ], [ entry "line": 7, [ ] ] ] ] = [ "Animal", [ ] ]

Prove Find Method Def Traverse 39
definition of method "move" of class "Dog" in [ entry "Animal": [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ entry "move": [ entry "params": [ self, [ ] ], [ entry "line": 5, [ ] ] ], [ ] ] ], [ entry "line": 1, [ ] ] ] ], [ entry "Dog": [ entry "bases": [ "Animal", [ ] ], [ entry "methods": [ entry "jump": [ entry "params": [ self, [ ] ], [ entry "line": 8, [ ] ] ], [ ] ], [ entry "line": 7, [ ] ] ] ], [ ] ] ] = [ entry "params": [ self, [ ] ], [ entry "line": 5, [ ] ] ]

Prove Find Method Def At 39
if Class Map at time 39 = [ entry "Animal": [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ entry "move": [ entry "params": [ self, [ ] ], [ entry "line": 5, [ ] ] ], [ ] ] ], [ entry "line": 1, [ ] ] ] ], [ entry "Dog": [ entry "bases": [ "Animal", [ ] ], [ entry "methods": [ entry "jump": [ entry "params": [ self, [ ] ], [ entry "line": 8, [ ] ] ], [ ] ], [ entry "line": 7, [ ] ] ] ], [ ] ] ], then definition of method "move" of class "Dog" in (Class Map at time 39) = [ entry "params": [ self, [ ] ], [ entry "line": 5, [ ] ] ]

Prove Find Method Params 39
if Class Map at time 39 = [ entry "Animal": [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ entry "move": [ entry "params": [ self, [ ] ], [ entry "line": 5, [ ] ] ], [ ] ] ], [ entry "line": 1, [ ] ] ] ], [ entry "Dog": [ entry "bases": [ "Animal", [ ] ], [ entry "methods": [ entry "jump": [ entry "params": [ self, [ ] ], [ entry "line": 8, [ ] ] ], [ ] ], [ entry "line": 7, [ ] ] ] ], [ ] ] ], then method parameters where the Class Map is (Class Map at time 39), class name is "Dog", and method name is "move" = [ self, [ ] ]

Write Call Function Begin Method Call Params 39
if the following are true:
  • expression state at time 39 = "call_function_begin"
  • the expression at time 39 = joe.move()
  • value at joe in map (Variables Map at time 39) = Python reference 0
  • the element at index 0 of stack (Python Object Store at time 39) = Python object: [ entry "__class_name__": "Dog", [ entry "x": 0, [ entry "y": 0, [ ] ] ] ]
  • method parameters where the Class Map is (Class Map at time 39), class name is "Dog", and method name is "move" = [ self, [ ] ]

then Parameters List at time 40 = [ self, [ ] ]


Do Reverse 39 0
reverse of "[]" = reverse of remaining stack "[]" and already reversed stack [ ]

Write Call Method Begin Values 39
if the following are true:
  • expression state at time 39 = "call_function_begin"
  • Value Stack at time 39 = [ [ ], [ ] ]
  • the expression at time 39 = joe.move()
  • value at joe in map (Variables Map at time 39) = Python reference 0
  • the element at index 0 of stack (Python Object Store at time 39) = Python object: [ entry "__class_name__": "Dog", [ entry "x": 0, [ entry "y": 0, [ ] ] ] ]
  • definition of method "move" of class "Dog" in (Class Map at time 39) = [ entry "params": [ self, [ ] ], [ entry "line": 5, [ ] ] ]

then Argument Values at time 40 = [ Python reference 0, [ ] ]


Write Call Function Begin Method Call Object Store 39
if the following are true:
  • expression state at time 39 = "call_function_begin"
  • the expression at time 39 = joe.move()
  • value at joe in map (Variables Map at time 39) = Python reference 0
  • the element at index 0 of stack (Python Object Store at time 39) = Python object: [ entry "__class_name__": "Dog", [ entry "x": 0, [ entry "y": 0, [ ] ] ] ]
  • method parameters where the Class Map is (Class Map at time 39), class name is "Dog", and method name is "move" = [ self, [ ] ]
  • Python Object Store at time 39 = [ Python object: [ entry "__class_name__": "Dog", [ entry "x": 0, [ entry "y": 0, [ ] ] ] ], [ ] ]

then Python Object Store at time 40 = [ Python object: [ entry "__class_name__": "Dog", [ entry "x": 0, [ entry "y": 0, [ ] ] ] ], [ ] ]


Write Call Function Begin Value Stack 39
if the following are true:
  • expression state at time 39 = "call_function_begin"
  • Value Stack at time 39 = [ [ ], [ ] ]
  • the expression at time 39 = joe.move()

then Value Stack at time 40 = [ ]


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

then arguments stack at time 40 = [ ]


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

then parent stack at time 40 = [ ]


Do Control Map At Unchanged 39
if the following are true:
  • expression state at time 39 = "call_function_begin"
  • Control Map at time 39 = [ entry 0: (pair ("class", "Dog")), [ ] ]

then Control Map at time 40 = [ entry 0: (pair ("class", "Dog")), [ ] ]


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

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


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

then the line at time 40 = 11


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

then the tab at time 40 = 0


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

then stack at time 40 = [ ]


Do Class Defs At Unchanged 39
if the following are true:
  • expression state at time 39 = "call_function_begin"
  • Class Map at time 39 = [ entry "Animal": [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ entry "move": [ entry "params": [ self, [ ] ], [ entry "line": 5, [ ] ] ], [ ] ] ], [ entry "line": 1, [ ] ] ] ], [ entry "Dog": [ entry "bases": [ "Animal", [ ] ], [ entry "methods": [ entry "jump": [ entry "params": [ self, [ ] ], [ entry "line": 8, [ ] ] ], [ ] ], [ entry "line": 7, [ ] ] ] ], [ ] ] ]

then Class Map at time 40 = [ entry "Animal": [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ entry "move": [ entry "params": [ self, [ ] ], [ entry "line": 5, [ ] ] ], [ ] ] ], [ entry "line": 1, [ ] ] ] ], [ entry "Dog": [ entry "bases": [ "Animal", [ ] ], [ entry "methods": [ entry "jump": [ entry "params": [ self, [ ] ], [ entry "line": 8, [ ] ] ], [ ] ], [ entry "line": 7, [ ] ] ] ], [ ] ] ]


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

Write Call Function Build Tmp 40
if the following are true:
  • expression state at time 40 = "call_build_args"
  • Function Variables Map at time 40 = [ ]
  • Parameters List at time 40 = [ self, [ ] ]
  • Argument Values at time 40 = [ Python reference 0, [ ] ]

then Function Variables Map at time 41 = [ entry self: (Python reference 0), [ ] ]


Write Call Function Build Func Args 40
if the following are true:
  • expression state at time 40 = "call_build_args"
  • Parameters List at time 40 = [ self, [ ] ]
  • Argument Values at time 40 = [ Python reference 0, [ ] ]

then Parameters List at time 41 = [ ]


Write Call Function Build Values 40
if the following are true:
  • expression state at time 40 = "call_build_args"
  • Parameters List at time 40 = [ self, [ ] ]
  • Argument Values at time 40 = [ Python reference 0, [ ] ]

then Argument Values at time 41 = [ ]


Write Call Function Build State 40
if the following are true:
  • expression state at time 40 = "call_build_args"
  • Parameters List at time 40 = [ self, [ ] ]
  • Argument Values at time 40 = [ Python reference 0, [ ] ]

then expression state at time 41 = "call_build_args"


Write Call Function Build Variables 40
if the following are true:
  • expression state at time 40 = "call_build_args"
  • Parameters List at time 40 = [ self, [ ] ]
  • Argument Values at time 40 = [ Python reference 0, [ ] ]
  • Variables Map at time 40 = [ entry joe: (Python reference 0), [ ] ]

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


Write Call Function Build Stack 40
if the following are true:
  • expression state at time 40 = "call_build_args"
  • Parameters List at time 40 = [ self, [ ] ]
  • Argument Values at time 40 = [ Python reference 0, [ ] ]
  • stack at time 40 = [ ]

then stack at time 41 = [ ]


Write Call Function Build Object Store 40
if the following are true:
  • expression state at time 40 = "call_build_args"
  • Parameters List at time 40 = [ self, [ ] ]
  • Argument Values at time 40 = [ Python reference 0, [ ] ]
  • Python Object Store at time 40 = [ Python object: [ entry "__class_name__": "Dog", [ entry "x": 0, [ entry "y": 0, [ ] ] ] ], [ ] ]

then Python Object Store at time 41 = [ Python object: [ entry "__class_name__": "Dog", [ entry "x": 0, [ entry "y": 0, [ ] ] ] ], [ ] ]


Write Call Function Build Control Map 40
if the following are true:
  • expression state at time 40 = "call_build_args"
  • Parameters List at time 40 = [ self, [ ] ]
  • Argument Values at time 40 = [ Python reference 0, [ ] ]
  • Control Map at time 40 = [ entry 0: (pair ("class", "Dog")), [ ] ]

then Control Map at time 41 = [ entry 0: (pair ("class", "Dog")), [ ] ]


Write Call Function Build Line At 40
if the following are true:
  • expression state at time 40 = "call_build_args"
  • Parameters List at time 40 = [ self, [ ] ]
  • the line at time 40 = 11

then the line at time 41 = 11


Write Call Function Build Tab At 40
if the following are true:
  • expression state at time 40 = "call_build_args"
  • Parameters List at time 40 = [ self, [ ] ]
  • the tab at time 40 = 0

then the tab at time 41 = 0


Do Value Stack At Unchanged 40
if the following are true:
  • expression state at time 40 = "call_build_args"
  • Value Stack at time 40 = [ ]

then Value Stack at time 41 = [ ]


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

then arguments stack at time 41 = [ ]


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

then parent stack at time 41 = [ ]


Do Expr At Unchanged 40
if the following are true:
  • expression state at time 40 = "call_build_args"
  • the expression at time 40 = joe.move()

then the expression at time 41 = joe.move()


Do Class Defs At Unchanged 40
if the following are true:
  • expression state at time 40 = "call_build_args"
  • Class Map at time 40 = [ entry "Animal": [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ entry "move": [ entry "params": [ self, [ ] ], [ entry "line": 5, [ ] ] ], [ ] ] ], [ entry "line": 1, [ ] ] ] ], [ entry "Dog": [ entry "bases": [ "Animal", [ ] ], [ entry "methods": [ entry "jump": [ entry "params": [ self, [ ] ], [ entry "line": 8, [ ] ] ], [ ] ], [ entry "line": 7, [ ] ] ] ], [ ] ] ]

then Class Map at time 41 = [ entry "Animal": [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ entry "move": [ entry "params": [ self, [ ] ], [ entry "line": 5, [ ] ] ], [ ] ] ], [ entry "line": 1, [ ] ] ] ], [ entry "Dog": [ entry "bases": [ "Animal", [ ] ], [ entry "methods": [ entry "jump": [ entry "params": [ self, [ ] ], [ entry "line": 8, [ ] ] ], [ ] ], [ entry "line": 7, [ ] ] ] ], [ ] ] ]


Write Call Function Build End Stack 41
if the following are true:
  • expression state at time 41 = "call_build_args"
  • Parameters List at time 41 = [ ]
  • stack at time 41 = [ ]
  • Variables Map at time 41 = [ entry joe: (Python reference 0), [ ] ]
  • parent stack at time 41 = [ ]
  • arguments stack at time 41 = [ ]
  • Value Stack at time 41 = [ ]
  • the line at time 41 = 11
  • the tab at time 41 = 0
  • Control Map at time 41 = [ entry 0: (pair ("class", "Dog")), [ ] ]

then stack at time 42 = [ program context with variables: [ entry joe: (Python reference 0), [ ] ] and expression state: (expression state with parent stack: [ ] arguments: [ ] values: [ ] line: 11 tab: 0) and control map: [ entry 0: (pair ("class", "Dog")), [ ] ], [ ] ]


Write Call Function Build End Variables 41
if the following are true:
  • expression state at time 41 = "call_build_args"
  • Parameters List at time 41 = [ ]
  • Function Variables Map at time 41 = [ entry self: (Python reference 0), [ ] ]

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


Do Get Key Value 41 0
value at "Animal" in map [ entry "Animal": [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ entry "move": [ entry "params": [ self, [ ] ], [ entry "line": 5, [ ] ] ], [ ] ] ], [ entry "line": 1, [ ] ] ] ], [ entry "Dog": [ entry "bases": [ "Animal", [ ] ], [ entry "methods": [ entry "jump": [ entry "params": [ self, [ ] ], [ entry "line": 8, [ ] ] ], [ ] ], [ entry "line": 7, [ ] ] ] ], [ ] ] ] = [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ entry "move": [ entry "params": [ self, [ ] ], [ entry "line": 5, [ ] ] ], [ ] ] ], [ entry "line": 1, [ ] ] ] ]

Do Get Key Value 41 1
value at "methods" in map [ entry "bases": [ "Animal", [ ] ], [ entry "methods": [ entry "jump": [ entry "params": [ self, [ ] ], [ entry "line": 8, [ ] ] ], [ ] ], [ entry "line": 7, [ ] ] ] ] = [ entry "jump": [ entry "params": [ self, [ ] ], [ entry "line": 8, [ ] ] ], [ ] ]

Do Get Key Value 41 2
value at "move" in map [ entry "jump": [ entry "params": [ self, [ ] ], [ entry "line": 8, [ ] ] ], [ ] ] = value at "move" in map [ ]

Do Get Key Value 41 3
value at "line" in map [ entry "params": [ self, [ ] ], [ entry "line": 5, [ ] ] ] = 5

Prove Find Method Def 41
definition of method "move" of class "Animal" in [ entry "Animal": [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ entry "move": [ entry "params": [ self, [ ] ], [ entry "line": 5, [ ] ] ], [ ] ] ], [ entry "line": 1, [ ] ] ] ], [ entry "Dog": [ entry "bases": [ "Animal", [ ] ], [ entry "methods": [ entry "jump": [ entry "params": [ self, [ ] ], [ entry "line": 8, [ ] ] ], [ ] ], [ entry "line": 7, [ ] ] ] ], [ ] ] ] = [ entry "params": [ self, [ ] ], [ entry "line": 5, [ ] ] ]

Prove Find Method Line 41
if Class Map at time 41 = [ entry "Animal": [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ entry "move": [ entry "params": [ self, [ ] ], [ entry "line": 5, [ ] ] ], [ ] ] ], [ entry "line": 1, [ ] ] ] ], [ entry "Dog": [ entry "bases": [ "Animal", [ ] ], [ entry "methods": [ entry "jump": [ entry "params": [ self, [ ] ], [ entry "line": 8, [ ] ] ], [ ] ], [ entry "line": 7, [ ] ] ] ], [ ] ] ], then line number of method "move" of class "Dog" in (Class Map at time 41) = 5

Write Call Function Build End Line Method 41
if the following are true:
  • expression state at time 41 = "call_build_args"
  • Parameters List at time 41 = [ ]
  • the expression at time 41 = joe.move()
  • line number of method "move" of class "Dog" in (Class Map at time 41) = 5

then the line at time 42 = 6


Write Call Function Build End Method Tab 41
if the following are true:
  • expression state at time 41 = "call_build_args"
  • Parameters List at time 41 = [ ]
  • the expression at time 41 = joe.move()
  • line number of method "move" of class "Dog" in (Class Map at time 41) = 5

then the tab at time 42 = 2


Write Call Function Build End State 41
if the following are true:
  • expression state at time 41 = "call_build_args"
  • Parameters List at time 41 = [ ]

then expression state at time 42 = "not_expr"


Write Call Function Build End Object Store 41
if the following are true:
  • expression state at time 41 = "call_build_args"
  • Parameters List at time 41 = [ ]
  • Python Object Store at time 41 = [ Python object: [ entry "__class_name__": "Dog", [ entry "x": 0, [ entry "y": 0, [ ] ] ] ], [ ] ]

then Python Object Store at time 42 = [ Python object: [ entry "__class_name__": "Dog", [ entry "x": 0, [ entry "y": 0, [ ] ] ] ], [ ] ]


Write Call Function Build End Control Map 41
if the following are true:
  • expression state at time 41 = "call_build_args"
  • Parameters List at time 41 = [ ]
  • the expression at time 41 = joe.move()
  • line number of method "move" of class "Dog" in (Class Map at time 41) = 5

then Control Map at time 42 = [ entry 0: (pair ("class", "Dog")), [ entry 1: (pair ("method", "move")), [ ] ] ]


Do Class Defs At Unchanged 41
if the following are true:
  • expression state at time 41 = "call_build_args"
  • Class Map at time 41 = [ entry "Animal": [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ entry "move": [ entry "params": [ self, [ ] ], [ entry "line": 5, [ ] ] ], [ ] ] ], [ entry "line": 1, [ ] ] ] ], [ entry "Dog": [ entry "bases": [ "Animal", [ ] ], [ entry "methods": [ entry "jump": [ entry "params": [ self, [ ] ], [ entry "line": 8, [ ] ] ], [ ] ], [ entry "line": 7, [ ] ] ] ], [ ] ] ]

then Class Map at time 42 = [ entry "Animal": [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ entry "move": [ entry "params": [ self, [ ] ], [ entry "line": 5, [ ] ] ], [ ] ] ], [ entry "line": 1, [ ] ] ] ], [ entry "Dog": [ entry "bases": [ "Animal", [ ] ], [ entry "methods": [ entry "jump": [ entry "params": [ self, [ ] ], [ entry "line": 8, [ ] ] ], [ ] ], [ entry "line": 7, [ ] ] ] ], [ ] ] ]


Do Convert Stmt 42
if statement at line 6, tab 2 = self.x = self.x + 5, then statement at line 6, tab 2 = self."x" = __add__(self.x, 5)

Write Set Name Expr At on State 42
if the following are true:
  • the line at time 42 = 6
  • the tab at time 42 = 2
  • statement at line 6, tab 2 = self."x" = __add__(self.x, 5)
  • expression state at time 42 = "not_expr"

then the expression at time 43 = self."x" = __add__(self.x, 5)


Write Set Name Expr State At on State 42
if the following are true:
  • the line at time 42 = 6
  • the tab at time 42 = 2
  • statement at line 6, tab 2 = self."x" = __add__(self.x, 5)
  • expression state at time 42 = "not_expr"

then expression state at time 43 = "begin_expr"


Write Set Name Line At on State 42
if the following are true:
  • the line at time 42 = 6
  • the tab at time 42 = 2
  • statement at line 6, tab 2 = self."x" = __add__(self.x, 5)
  • expression state at time 42 = "not_expr"

then the line at time 43 = 6


Write Set Name Tab At on State 42
if the following are true:
  • the line at time 42 = 6
  • the tab at time 42 = 2
  • statement at line 6, tab 2 = self."x" = __add__(self.x, 5)
  • expression state at time 42 = "not_expr"

then the tab at time 43 = 2


Write Set Name Value Stack At on State 42
if the following are true:
  • the line at time 42 = 6
  • the tab at time 42 = 2
  • statement at line 6, tab 2 = self."x" = __add__(self.x, 5)
  • expression state at time 42 = "not_expr"

then Value Stack at time 43 = [ ]


Write Set Name Parent Stack At on State 42
if the following are true:
  • the line at time 42 = 6
  • the tab at time 42 = 2
  • statement at line 6, tab 2 = self."x" = __add__(self.x, 5)
  • expression state at time 42 = "not_expr"

then parent stack at time 43 = [ ]


Write Set Name Arg Stack At on State 42
if the following are true:
  • the line at time 42 = 6
  • the tab at time 42 = 2
  • statement at line 6, tab 2 = self."x" = __add__(self.x, 5)
  • expression state at time 42 = "not_expr"

then arguments stack at time 43 = [ ]


Write Stmt Object Store At Unchanged Expr42
if the following are true:
  • the line at time 42 = 6
  • the tab at time 42 = 2
  • statement at line 6, tab 2 = self."x" = __add__(self.x, 5)
  • expression state at time 42 = "not_expr"
  • Python Object Store at time 42 = [ Python object: [ entry "__class_name__": "Dog", [ entry "x": 0, [ entry "y": 0, [ ] ] ] ], [ ] ]

then Python Object Store at time 43 = [ Python object: [ entry "__class_name__": "Dog", [ entry "x": 0, [ entry "y": 0, [ ] ] ] ], [ ] ]


Write Stmt Control Map At Unchanged Expr42
if the following are true:
  • the line at time 42 = 6
  • the tab at time 42 = 2
  • statement at line 6, tab 2 = self."x" = __add__(self.x, 5)
  • expression state at time 42 = "not_expr"
  • Control Map at time 42 = [ entry 0: (pair ("class", "Dog")), [ entry 1: (pair ("method", "move")), [ ] ] ]

then Control Map at time 43 = [ entry 0: (pair ("class", "Dog")), [ entry 1: (pair ("method", "move")), [ ] ] ]


Write Stmt Variables At Unchanged 42
if the following are true:
  • the line at time 42 = 6
  • the tab at time 42 = 2
  • statement at line 6, tab 2 = self."x" = __add__(self.x, 5)
  • Variables Map at time 42 = [ entry self: (Python reference 0), [ ] ]

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


Write Stmt Stack At Unchanged 42
if the following are true:
  • the line at time 42 = 6
  • the tab at time 42 = 2
  • statement at line 6, tab 2 = self."x" = __add__(self.x, 5)
  • stack at time 42 = [ program context with variables: [ entry joe: (Python reference 0), [ ] ] and expression state: (expression state with parent stack: [ ] arguments: [ ] values: [ ] line: 11 tab: 0) and control map: [ entry 0: (pair ("class", "Dog")), [ ] ], [ ] ]

then stack at time 43 = [ program context with variables: [ entry joe: (Python reference 0), [ ] ] and expression state: (expression state with parent stack: [ ] arguments: [ ] values: [ ] line: 11 tab: 0) and control map: [ entry 0: (pair ("class", "Dog")), [ ] ], [ ] ]


Write Stmt Class Defs At Unchanged 42
if the following are true:
  • the line at time 42 = 6
  • the tab at time 42 = 2
  • statement at line 6, tab 2 = self."x" = __add__(self.x, 5)
  • Class Map at time 42 = [ entry "Animal": [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ entry "move": [ entry "params": [ self, [ ] ], [ entry "line": 5, [ ] ] ], [ ] ] ], [ entry "line": 1, [ ] ] ] ], [ entry "Dog": [ entry "bases": [ "Animal", [ ] ], [ entry "methods": [ entry "jump": [ entry "params": [ self, [ ] ], [ entry "line": 8, [ ] ] ], [ ] ], [ entry "line": 7, [ ] ] ] ], [ ] ] ]

then Class Map at time 43 = [ entry "Animal": [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ entry "move": [ entry "params": [ self, [ ] ], [ entry "line": 5, [ ] ] ], [ ] ] ], [ entry "line": 1, [ ] ] ] ], [ entry "Dog": [ entry "bases": [ "Animal", [ ] ], [ entry "methods": [ entry "jump": [ entry "params": [ self, [ ] ], [ entry "line": 8, [ ] ] ], [ ] ], [ entry "line": 7, [ ] ] ] ], [ ] ] ]


Get Begin Expr Value 43
if the following are true:
  • expression state at time 43 = "begin_expr"
  • the expression at time 43 = self."x" = __add__(self.x, 5)
  • Value Stack at time 43 = [ ]

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


Get Begin Expr Parent 43
if the following are true:
  • expression state at time 43 = "begin_expr"
  • the expression at time 43 = self."x" = __add__(self.x, 5)
  • parent stack at time 43 = [ ]

then parent stack at time 44 = [ self."x" = __add__(self.x, 5), [ ] ]


Get Begin Expr Params 43
if the following are true:
  • expression state at time 43 = "begin_expr"
  • the expression at time 43 = self."x" = __add__(self.x, 5)
  • arguments stack at time 43 = [ ]

then arguments stack at time 44 = [ [ __add__(self.x, 5), [ ] ], [ ] ]


Get Begin Expr Call State 43
if the following are true:
  • expression state at time 43 = "begin_expr"
  • the expression at time 43 = self."x" = __add__(self.x, 5)

then expression state at time 44 = "iterate_args"


Do Expr At Unchanged 43
if the following are true:
  • expression state at time 43 = "begin_expr"
  • the expression at time 43 = self."x" = __add__(self.x, 5)

then the expression at time 44 = self."x" = __add__(self.x, 5)


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

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


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

then the line at time 44 = 6


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

then the tab at time 44 = 2


Do Stack At Unchanged 43
if the following are true:
  • expression state at time 43 = "begin_expr"
  • stack at time 43 = [ program context with variables: [ entry joe: (Python reference 0), [ ] ] and expression state: (expression state with parent stack: [ ] arguments: [ ] values: [ ] line: 11 tab: 0) and control map: [ entry 0: (pair ("class", "Dog")), [ ] ], [ ] ]

then stack at time 44 = [ program context with variables: [ entry joe: (Python reference 0), [ ] ] and expression state: (expression state with parent stack: [ ] arguments: [ ] values: [ ] line: 11 tab: 0) and control map: [ entry 0: (pair ("class", "Dog")), [ ] ], [ ] ]


Do Object Store At Unchanged 43
if the following are true:
  • expression state at time 43 = "begin_expr"
  • Python Object Store at time 43 = [ Python object: [ entry "__class_name__": "Dog", [ entry "x": 0, [ entry "y": 0, [ ] ] ] ], [ ] ]

then Python Object Store at time 44 = [ Python object: [ entry "__class_name__": "Dog", [ entry "x": 0, [ entry "y": 0, [ ] ] ] ], [ ] ]


Do Control Map At Unchanged 43
if the following are true:
  • expression state at time 43 = "begin_expr"
  • Control Map at time 43 = [ entry 0: (pair ("class", "Dog")), [ entry 1: (pair ("method", "move")), [ ] ] ]

then Control Map at time 44 = [ entry 0: (pair ("class", "Dog")), [ entry 1: (pair ("method", "move")), [ ] ] ]


Do Class Defs At Unchanged 43
if the following are true:
  • expression state at time 43 = "begin_expr"
  • Class Map at time 43 = [ entry "Animal": [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ entry "move": [ entry "params": [ self, [ ] ], [ entry "line": 5, [ ] ] ], [ ] ] ], [ entry "line": 1, [ ] ] ] ], [ entry "Dog": [ entry "bases": [ "Animal", [ ] ], [ entry "methods": [ entry "jump": [ entry "params": [ self, [ ] ], [ entry "line": 8, [ ] ] ], [ ] ], [ entry "line": 7, [ ] ] ] ], [ ] ] ]

then Class Map at time 44 = [ entry "Animal": [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ ] ], [ entry "line": 2, [ ] ] ], [ entry "move": [ entry "params": [ self, [ ] ], [ entry "line": 5, [ ] ] ], [ ] ] ], [ entry "line": 1, [ ] ] ] ], [ entry "Dog": [ entry "bases": [ "Animal", [ ] ], [ entry "methods": [ entry "jump": [ entry "params": [ self, [ ] ], [ entry "line": 8, [ ] ] ], [ ] ], [ entry "line": 7, [ ] ] ] ], [ ] ] ]


Get Iterate Expr 44
if the following are true:
  • expression state at time 44 = "iterate_args"
  • arguments stack at time 44 = [ [ __add__(self.x, 5), [ ] ], [ ] ]

then the expression at time 45 = __add__(self.x, 5)


Get Iterate Params 44
if the following are true:
  • expression state at time 44 = "iterate_args"
  • arguments stack at time 44 = [ [ __add__(self.x, 5), [ ] ], [ ] ]

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


Get Iterate State 44
if the following are true:
  • expression state at time 44 = "iterate_args"
  • arguments stack at time 44 = [ [ __add__(self.x, 5), [ ] ], [ ] ]

then expression state at time 45 = "begin_expr"


Get Iterate Parent 44
if the following are true:
  • expression state at time 44 = "iterate_args"
  • arguments stack at time 44 = [ [ __add__(self.x, 5), [ ] ], [ ] ]
  • parent stack at time 44 = [ self."x" = __add__(self.x, 5), [ ] ]

then parent stack at time 45 = [ self."x" = __add__(self.x, 5), [ ] ]


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

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


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

then the line at time 45 = 6


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

then the tab at time 45 = 2


Do Stack At Unchanged 44
if the following are true:
  • expression state at time 44 = "iterate_args"
  • stack at time 44 = [ program context with variables: [ entry joe: (Python reference 0), [ ] ] and expression state: (expression state with parent stack: [ ] arguments: [ ] values: [ ] line: 11 tab: 0) and control map: [ entry 0: (pair ("class", "Dog")), [ ] ], [ ] ]

then stack at time 45 = [ program context with variables: [ entry joe: (Python reference 0), [ ] ] and expression state: (expression state with parent stack: [ ] arguments: [ ] values: [ ] line: 11 tab: 0) and control map: [ entry 0: (pair ("class", "Dog")), [ ] ], [ ] ]



Pages: 183 184 185 ... 193