Proofs

if Python Object Store at time 61 = [ 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 61) = Python object: [ entry "__class_name__": "Dog", [ entry "x": 0, [ entry "y": 0, [ ] ] ] ]

if Variables Map at time 61 = [ entry self: (Python reference 0), [ ] ], then value at self in map (Variables Map at time 61) = Python reference 0

if the following are true:

• expression state at time 61 = "call_function_begin"
• Value Stack at time 61 = [ [ 5, [ ] ], [ ] ]
• the expression at time 61 = self."x" = __add__(self.x, 5)
• value at self in map (Variables Map at time 61) = Python reference 0
• Python Object Store at time 61 = [ Python object: [ entry "__class_name__": "Dog", [ entry "x": 0, [ entry "y": 0, [ ] ] ] ], [ ] ]
• the element at index 0 of stack (Python Object Store at time 61) = Python object: [ entry "__class_name__": "Dog", [ entry "x": 0, [ entry "y": 0, [ ] ] ] ]

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

if the following are true:

• expression state at time 61 = "call_function_begin"
• parent stack at time 61 = [ ]
• the expression at time 61 = self."x" = __add__(self.x, 5)

then expression state at time 62 = "end_expr"

if the following are true:

• expression state at time 61 = "call_function_begin"
• Value Stack at time 61 = [ [ 5, [ ] ], [ ] ]
• the expression at time 61 = self."x" = __add__(self.x, 5)

then Value Stack at time 62 = [ ]

if the following are true:

• expression state at time 61 = "call_function_begin"
• arguments stack at time 61 = [ ]

then arguments stack at time 62 = [ ]

if the following are true:

• expression state at time 61 = "call_function_begin"
• parent stack at time 61 = [ ]

then parent stack at time 62 = [ ]

if the following are true:

• expression state at time 61 = "call_function_begin"
• Control Map at time 61 = [ entry 0: (pair ("class", "Dog")), [ entry 1: (pair ("method", "move")), [ ] ] ]

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

if the following are true:

• expression state at time 61 = "call_function_begin"
• Variables Map at time 61 = [ entry self: (Python reference 0), [ ] ]

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

if the following are true:

• expression state at time 61 = "call_function_begin"
• the line at time 61 = 6

then the line at time 62 = 6

if the following are true:

• expression state at time 61 = "call_function_begin"
• the tab at time 61 = 2

then the tab at time 62 = 2

if the following are true:

• expression state at time 61 = "call_function_begin"
• stack at time 61 = [ 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 62 = [ 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")), [ ] ], [ ] ]

if the following are true:

• expression state at time 61 = "call_function_begin"
• Class Map at time 61 = [ 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 62 = [ 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, [ ] ] ] ], [ ] ] ]

if the following are true:

• the line at time 62 = 6
• the tab at time 62 = 2
• statement at line 6, tab 2 = self."x" = __add__(self.x, 5)
• expression state at time 62 = "end_expr"

then the line at time 63 = 7

if the following are true:

• the line at time 62 = 6
• the tab at time 62 = 2
• statement at line 6, tab 2 = self."x" = __add__(self.x, 5)
• expression state at time 62 = "end_expr"

then the tab at time 63 = 2

if the following are true:

• the line at time 62 = 6
• the tab at time 62 = 2
• statement at line 6, tab 2 = self."x" = __add__(self.x, 5)
• expression state at time 62 = "end_expr"
• Python Object Store at time 62 = [ Python object: [ entry "__class_name__": "Dog", [ entry "x": 5, [ entry "y": 0, [ ] ] ] ], [ ] ]

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

if the following are true:

• the line at time 62 = 6
• the tab at time 62 = 2
• statement at line 6, tab 2 = self."x" = __add__(self.x, 5)
• expression state at time 62 = "end_expr"
• Control Map at time 62 = [ entry 0: (pair ("class", "Dog")), [ entry 1: (pair ("method", "move")), [ ] ] ]

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

if the following are true:

• the line at time 62 = 6
• the tab at time 62 = 2
• statement at line 6, tab 2 = self."x" = __add__(self.x, 5)
• Variables Map at time 62 = [ entry self: (Python reference 0), [ ] ]

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

if the following are true:

• the line at time 62 = 6
• the tab at time 62 = 2
• statement at line 6, tab 2 = self."x" = __add__(self.x, 5)
• stack at time 62 = [ 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 63 = [ 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")), [ ] ], [ ] ]

if the following are true:

• the line at time 62 = 6
• the tab at time 62 = 2
• statement at line 6, tab 2 = self."x" = __add__(self.x, 5)
• Class Map at time 62 = [ 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 63 = [ 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, [ ] ] ] ], [ ] ] ]

if expression state at time 62 = "end_expr", then expression state at time 63 = "not_expr"

value at 1 in map [ entry 0: (pair ("class", "Dog")), [ entry 1: (pair ("method", "move")), [ ] ] ] = pair ("method", "move")

if Control Map at time 63 = [ entry 0: (pair ("class", "Dog")), [ entry 1: (pair ("method", "move")), [ ] ] ], then value at (2 - 1) in map (Control Map at time 63) = pair ("method", "move")

if the following are true:

• the line at time 63 = 7
• the tab at time 63 = 2
• statement at line 7, tab 0 = class Dog(Animal):
• Control Map at time 63 = [ entry 0: (pair ("class", "Dog")), [ entry 1: (pair ("method", "move")), [ ] ] ]
• not ("move" = "__init__")

then Return Value at time 64 = None

if the following are true:

• the line at time 63 = 7
• the tab at time 63 = 2
• statement at line 7, tab 0 = class Dog(Animal):
• Control Map at time 63 = [ entry 0: (pair ("class", "Dog")), [ entry 1: (pair ("method", "move")), [ ] ] ]
• stack at time 63 = [ 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 the line at time 64 = 11

if the following are true:

• the line at time 63 = 7
• the tab at time 63 = 2
• statement at line 7, tab 0 = class Dog(Animal):
• Control Map at time 63 = [ entry 0: (pair ("class", "Dog")), [ entry 1: (pair ("method", "move")), [ ] ] ]
• stack at time 63 = [ 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 the tab at time 64 = 0

if the following are true:

• the line at time 63 = 7
• the tab at time 63 = 2
• statement at line 7, tab 0 = class Dog(Animal):
• Control Map at time 63 = [ entry 0: (pair ("class", "Dog")), [ entry 1: (pair ("method", "move")), [ ] ] ]
• stack at time 63 = [ 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 expression state at time 64 = "call_returned"

if the following are true:

• the line at time 63 = 7
• the tab at time 63 = 2
• statement at line 7, tab 0 = class Dog(Animal):
• Control Map at time 63 = [ entry 0: (pair ("class", "Dog")), [ entry 1: (pair ("method", "move")), [ ] ] ]
• stack at time 63 = [ 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 parent stack at time 64 = [ ]

if the following are true:

• the line at time 63 = 7
• the tab at time 63 = 2
• statement at line 7, tab 0 = class Dog(Animal):
• Control Map at time 63 = [ entry 0: (pair ("class", "Dog")), [ entry 1: (pair ("method", "move")), [ ] ] ]
• stack at time 63 = [ 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 Variables Map at time 64 = [ entry joe: (Python reference 0), [ ] ]

if the following are true:

• the line at time 63 = 7
• the tab at time 63 = 2
• statement at line 7, tab 0 = class Dog(Animal):
• Control Map at time 63 = [ entry 0: (pair ("class", "Dog")), [ entry 1: (pair ("method", "move")), [ ] ] ]
• stack at time 63 = [ 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 arguments stack at time 64 = [ ]

if the following are true:

• the line at time 63 = 7
• the tab at time 63 = 2
• statement at line 7, tab 0 = class Dog(Animal):
• Control Map at time 63 = [ entry 0: (pair ("class", "Dog")), [ entry 1: (pair ("method", "move")), [ ] ] ]
• stack at time 63 = [ 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 Value Stack at time 64 = [ ]

if the following are true:

• the line at time 63 = 7
• the tab at time 63 = 2
• statement at line 7, tab 0 = class Dog(Animal):
• Control Map at time 63 = [ entry 0: (pair ("class", "Dog")), [ entry 1: (pair ("method", "move")), [ ] ] ]
• stack at time 63 = [ 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 64 = [ ]

if the following are true:

• the line at time 63 = 7
• the tab at time 63 = 2
• statement at line 7, tab 0 = class Dog(Animal):
• Control Map at time 63 = [ entry 0: (pair ("class", "Dog")), [ entry 1: (pair ("method", "move")), [ ] ] ]
• stack at time 63 = [ 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 Control Map at time 64 = [ entry 0: (pair ("class", "Dog")), [ ] ]

if the following are true:

• the line at time 63 = 7
• the tab at time 63 = 2
• statement at line 7, tab 0 = class Dog(Animal):
• Control Map at time 63 = [ entry 0: (pair ("class", "Dog")), [ entry 1: (pair ("method", "move")), [ ] ] ]
• Python Object Store at time 63 = [ Python object: [ entry "__class_name__": "Dog", [ entry "x": 5, [ entry "y": 0, [ ] ] ] ], [ ] ]

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

if the following are true:

• the line at time 63 = 7
• the tab at time 63 = 2
• statement at line 7, tab 0 = class Dog(Animal):
• Control Map at time 63 = [ entry 0: (pair ("class", "Dog")), [ entry 1: (pair ("method", "move")), [ ] ] ]
• Class Map at time 63 = [ 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 64 = [ 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, [ ] ] ] ], [ ] ] ]

if the following are true:

• expression state at time 64 = "call_returned"
• parent stack at time 64 = [ ]

then expression state at time 65 = "end_expr"

if the following are true:

• expression state at time 64 = "call_returned"
• the line at time 64 = 11

then the line at time 65 = 11

if the following are true:

• expression state at time 64 = "call_returned"
• the tab at time 64 = 0

then the tab at time 65 = 0

if the following are true:

• expression state at time 64 = "call_returned"
• Variables Map at time 64 = [ entry joe: (Python reference 0), [ ] ]

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

if the following are true:

• expression state at time 64 = "call_returned"
• Return Value at time 64 = None

then Return Value at time 65 = None

if the following are true:

• expression state at time 64 = "call_returned"
• stack at time 64 = [ ]

then stack at time 65 = [ ]

if the following are true:

• expression state at time 64 = "call_returned"
• parent stack at time 64 = [ ]

then parent stack at time 65 = [ ]

if the following are true:

• expression state at time 64 = "call_returned"
• arguments stack at time 64 = [ ]

then arguments stack at time 65 = [ ]

if the following are true:

• expression state at time 64 = "call_returned"
• Python Object Store at time 64 = [ Python object: [ entry "__class_name__": "Dog", [ entry "x": 5, [ entry "y": 0, [ ] ] ] ], [ ] ]

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

if the following are true:

• expression state at time 64 = "call_returned"
• Value Stack at time 64 = [ ]

then Value Stack at time 65 = [ ]

if the following are true:

• expression state at time 64 = "call_returned"
• Control Map at time 64 = [ entry 0: (pair ("class", "Dog")), [ ] ]

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

if the following are true:

• expression state at time 64 = "call_returned"
• Class Map at time 64 = [ 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 65 = [ 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, [ ] ] ] ], [ ] ] ]

if the following are true:

• the line at time 65 = 11
• the tab at time 65 = 0
• statement at line 11, tab 0 = joe.move()
• expression state at time 65 = "end_expr"

then the line at time 66 = 12

if the following are true:

• the line at time 65 = 11
• the tab at time 65 = 0
• statement at line 11, tab 0 = joe.move()
• expression state at time 65 = "end_expr"

then the tab at time 66 = 0

if the following are true:

• the line at time 65 = 11
• the tab at time 65 = 0
• statement at line 11, tab 0 = joe.move()
• expression state at time 65 = "end_expr"
• Control Map at time 65 = [ entry 0: (pair ("class", "Dog")), [ ] ]

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

if the following are true:

• the line at time 65 = 11
• the tab at time 65 = 0
• statement at line 11, tab 0 = joe.move()
• expression state at time 65 = "end_expr"
• Python Object Store at time 65 = [ Python object: [ entry "__class_name__": "Dog", [ entry "x": 5, [ entry "y": 0, [ ] ] ] ], [ ] ]

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

if the following are true:

• the line at time 65 = 11
• the tab at time 65 = 0
• statement at line 11, tab 0 = joe.move()
• expression state at time 65 = "end_expr"
• Variables Map at time 65 = [ entry joe: (Python reference 0), [ ] ]

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

if the following are true:

• the line at time 65 = 11
• the tab at time 65 = 0
• statement at line 11, tab 0 = joe.move()
• expression state at time 65 = "end_expr"
• stack at time 65 = [ ]

then stack at time 66 = [ ]

if the following are true:

• the line at time 65 = 11
• the tab at time 65 = 0
• statement at line 11, tab 0 = joe.move()
• Class Map at time 65 = [ 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 66 = [ 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, [ ] ] ] ], [ ] ] ]

if expression state at time 65 = "end_expr", then expression state at time 66 = "not_expr"

if the following are true:

• the line at time 66 = 12
• the tab at time 66 = 0
• statement at line 12, tab 0 = joe.jump()
• expression state at time 66 = "not_expr"

then the expression at time 67 = joe.jump()

if the following are true:

• the line at time 66 = 12
• the tab at time 66 = 0
• statement at line 12, tab 0 = joe.jump()
• expression state at time 66 = "not_expr"

then expression state at time 67 = "begin_expr"

if the following are true:

• the line at time 66 = 12
• the tab at time 66 = 0
• statement at line 12, tab 0 = joe.jump()
• expression state at time 66 = "not_expr"

then the line at time 67 = 12

if the following are true:

• the line at time 66 = 12
• the tab at time 66 = 0
• statement at line 12, tab 0 = joe.jump()
• expression state at time 66 = "not_expr"

then the tab at time 67 = 0

if the following are true:

• the line at time 66 = 12
• the tab at time 66 = 0
• statement at line 12, tab 0 = joe.jump()
• expression state at time 66 = "not_expr"

then Value Stack at time 67 = [ ]

if the following are true:

• the line at time 66 = 12
• the tab at time 66 = 0
• statement at line 12, tab 0 = joe.jump()
• expression state at time 66 = "not_expr"

then parent stack at time 67 = [ ]

if the following are true:

• the line at time 66 = 12
• the tab at time 66 = 0
• statement at line 12, tab 0 = joe.jump()
• expression state at time 66 = "not_expr"

then arguments stack at time 67 = [ ]

if the following are true:

• the line at time 66 = 12
• the tab at time 66 = 0
• statement at line 12, tab 0 = joe.jump()
• expression state at time 66 = "not_expr"
• Python Object Store at time 66 = [ Python object: [ entry "__class_name__": "Dog", [ entry "x": 5, [ entry "y": 0, [ ] ] ] ], [ ] ]

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

if the following are true:

• the line at time 66 = 12
• the tab at time 66 = 0
• statement at line 12, tab 0 = joe.jump()
• expression state at time 66 = "not_expr"
• Control Map at time 66 = [ entry 0: (pair ("class", "Dog")), [ ] ]

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

if the following are true:

• the line at time 66 = 12
• the tab at time 66 = 0
• statement at line 12, tab 0 = joe.jump()
• expression state at time 66 = "not_expr"
• Variables Map at time 66 = [ entry joe: (Python reference 0), [ ] ]

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

if the following are true:

• the line at time 66 = 12
• the tab at time 66 = 0
• statement at line 12, tab 0 = joe.jump()
• expression state at time 66 = "not_expr"
• stack at time 66 = [ ]

then stack at time 67 = [ ]

if the following are true:

• the line at time 66 = 12
• the tab at time 66 = 0
• statement at line 12, tab 0 = joe.jump()
• Class Map at time 66 = [ 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 67 = [ 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, [ ] ] ] ], [ ] ] ]

if the following are true:

• expression state at time 67 = "begin_expr"
• the expression at time 67 = joe.jump()
• Value Stack at time 67 = [ ]

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

if the following are true:

• expression state at time 67 = "begin_expr"
• the expression at time 67 = joe.jump()
• parent stack at time 67 = [ ]

then parent stack at time 68 = [ joe.jump(), [ ] ]

if the following are true:

• expression state at time 67 = "begin_expr"
• the expression at time 67 = joe.jump()
• arguments stack at time 67 = [ ]

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

if the following are true:

• expression state at time 67 = "begin_expr"
• the expression at time 67 = joe.jump()

then expression state at time 68 = "iterate_args"

if the following are true:

• expression state at time 67 = "begin_expr"
• the expression at time 67 = joe.jump()

then the expression at time 68 = joe.jump()

if the following are true:

• expression state at time 67 = "begin_expr"
• Variables Map at time 67 = [ entry joe: (Python reference 0), [ ] ]

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

if the following are true:

• expression state at time 67 = "begin_expr"
• the line at time 67 = 12

then the line at time 68 = 12

if the following are true:

• expression state at time 67 = "begin_expr"
• the tab at time 67 = 0

then the tab at time 68 = 0

if the following are true:

• expression state at time 67 = "begin_expr"
• stack at time 67 = [ ]

then stack at time 68 = [ ]

if the following are true:

• expression state at time 67 = "begin_expr"
• Python Object Store at time 67 = [ Python object: [ entry "__class_name__": "Dog", [ entry "x": 5, [ entry "y": 0, [ ] ] ] ], [ ] ]

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

if the following are true:

• expression state at time 67 = "begin_expr"
• Control Map at time 67 = [ entry 0: (pair ("class", "Dog")), [ ] ]

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

if the following are true:

• expression state at time 67 = "begin_expr"
• Class Map at time 67 = [ 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 68 = [ 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, [ ] ] ] ], [ ] ] ]

if the following are true:

• expression state at time 68 = "iterate_args"
• arguments stack at time 68 = [ [ ], [ ] ]
• parent stack at time 68 = [ joe.jump(), [ ] ]

then expression state at time 69 = "call_function_begin"

if the following are true:

• expression state at time 68 = "iterate_args"
• arguments stack at time 68 = [ [ ], [ ] ]
• parent stack at time 68 = [ joe.jump(), [ ] ]

then the expression at time 69 = joe.jump()

if the following are true:

• expression state at time 68 = "iterate_args"
• arguments stack at time 68 = [ [ ], [ ] ]
• parent stack at time 68 = [ joe.jump(), [ ] ]

then parent stack at time 69 = [ ]

if the following are true:

• expression state at time 68 = "iterate_args"
• arguments stack at time 68 = [ [ ], [ ] ]
• parent stack at time 68 = [ joe.jump(), [ ] ]

then arguments stack at time 69 = [ ]

if the following are true:

• expression state at time 68 = "iterate_args"
• Value Stack at time 68 = [ [ ], [ ] ]

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

if the following are true:

• expression state at time 68 = "iterate_args"
• the line at time 68 = 12

then the line at time 69 = 12

if the following are true:

• expression state at time 68 = "iterate_args"
• the tab at time 68 = 0

then the tab at time 69 = 0

if the following are true:

• expression state at time 68 = "iterate_args"
• stack at time 68 = [ ]

then stack at time 69 = [ ]

if the following are true:

• expression state at time 68 = "iterate_args"
• Python Object Store at time 68 = [ Python object: [ entry "__class_name__": "Dog", [ entry "x": 5, [ entry "y": 0, [ ] ] ] ], [ ] ]

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

if the following are true:

• expression state at time 68 = "iterate_args"
• Control Map at time 68 = [ entry 0: (pair ("class", "Dog")), [ ] ]

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

if the following are true:

• expression state at time 68 = "iterate_args"
• Variables Map at time 68 = [ entry joe: (Python reference 0), [ ] ]

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

if the following are true:

• expression state at time 68 = "iterate_args"
• Class Map at time 68 = [ 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 69 = [ 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, [ ] ] ] ], [ ] ] ]

if the following are true:

• expression state at time 69 = "call_function_begin"
• the expression at time 69 = joe.jump()

then the expression at time 70 = joe.jump()

value at joe in map [ entry joe: (Python reference 0), [ ] ] = Python reference 0

if Variables Map at time 69 = [ entry joe: (Python reference 0), [ ] ], then value at joe in map (Variables Map at time 69) = Python reference 0

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

if Python Object Store at time 69 = [ Python object: [ entry "__class_name__": "Dog", [ entry "x": 5, [ entry "y": 0, [ ] ] ] ], [ ] ], then the element at index 0 of stack (Python Object Store at time 69) = Python object: [ entry "__class_name__": "Dog", [ entry "x": 5, [ entry "y": 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

if Class Map at time 69 = [ 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 69) contains key "Dog" = True

if the following are true:

• expression state at time 69 = "call_function_begin"
• the expression at time 69 = joe.jump()
• value at joe in map (Variables Map at time 69) = Python reference 0
• the element at index 0 of stack (Python Object Store at time 69) = Python object: [ entry "__class_name__": "Dog", [ entry "x": 5, [ entry "y": 0, [ ] ] ] ]
• map (Class Map at time 69) contains key "Dog" = True

then expression state at time 70 = "call_build_args"

if expression state at time 69 = "call_function_begin", then Function Variables Map at time 70 = [ ]