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 Arg Stack At Unchanged 20
if the following are true:
  • expression state at time 20 = "call_function_begin"
  • arguments stack at time 20 = [ ]

then arguments stack at time 21 = [ ]


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

then parent stack at time 21 = [ ]


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

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


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

then Variables Map at time 21 = [ ]


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

then the line at time 21 = 8


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

then the tab at time 21 = 0


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

then stack at time 21 = [ ]


Do Class Defs At Unchanged 20
if the following are true:
  • expression state at time 20 = "call_function_begin"
  • Class Map at time 20 = [ entry "Person": [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ first_name, [ last_name, [ age, [ ] ] ] ] ], [ entry "line": 2, [ ] ] ], [ entry "age_in_months": [ entry "params": [ self, [ ] ], [ entry "line": 6, [ ] ] ], [ ] ] ], [ entry "line": 1, [ ] ] ] ], [ ] ]

then Class Map at time 21 = [ entry "Person": [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ first_name, [ last_name, [ age, [ ] ] ] ] ], [ entry "line": 2, [ ] ] ], [ entry "age_in_months": [ entry "params": [ self, [ ] ], [ entry "line": 6, [ ] ] ], [ ] ] ], [ entry "line": 1, [ ] ] ] ], [ ] ]


Do Len At 21
length of stack [ ] = 0

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

Build Constructor Arguments Property Example
if the following are true:
  • expression state at time 21 = "call_build_args"
  • the expression at time 21 = Person("John", "Smith", 25)
  • Function Variables Map at time 21 = [ ]
  • Parameters List at time 21 = [ self, [ first_name, [ last_name, [ age, [ ] ] ] ] ]
  • Python Object Store at time 21 = [ ]

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


Pop Constructor Self Parameter Property Example
if the following are true:
  • expression state at time 21 = "call_build_args"
  • the expression at time 21 = Person("John", "Smith", 25)
  • Function Variables Map at time 21 = [ ]
  • Parameters List at time 21 = [ self, [ first_name, [ last_name, [ age, [ ] ] ] ] ]

then Parameters List at time 22 = [ first_name, [ last_name, [ age, [ ] ] ] ]


Write Call Build Constructor Unchanged Values At 21
if the following are true:
  • expression state at time 21 = "call_build_args"
  • the expression at time 21 = Person("John", "Smith", 25)
  • Function Variables Map at time 21 = [ ]
  • Parameters List at time 21 = [ self, [ first_name, [ last_name, [ age, [ ] ] ] ] ]
  • Argument Values at time 21 = [ "John", [ "Smith", [ 25, [ ] ] ] ]

then Argument Values at time 22 = [ "John", [ "Smith", [ 25, [ ] ] ] ]


Do Reverse 21 0
reverse of [ ] = [ ]

Do Reverse 21 1
reverse of [ Python object: [ entry "__class_name__": "Person", [ ] ], [ ] ] = [ Python object: [ entry "__class_name__": "Person", [ ] ], [ ] ]

Do Append 21
result of appending (Python object: [ entry "__class_name__": "Person", [ ] ]) to [ ] = [ Python object: [ entry "__class_name__": "Person", [ ] ], [ ] ]

Create And Store Object Property Example
if the following are true:
  • expression state at time 21 = "call_build_args"
  • the expression at time 21 = Person("John", "Smith", 25)
  • Function Variables Map at time 21 = [ ]
  • Parameters List at time 21 = [ self, [ first_name, [ last_name, [ age, [ ] ] ] ] ]
  • Python Object Store at time 21 = [ ]

then Python Object Store at time 22 = [ Python object: [ entry "__class_name__": "Person", [ ] ], [ ] ]


Write Call Build Constructor State 21
if the following are true:
  • expression state at time 21 = "call_build_args"
  • the expression at time 21 = Person("John", "Smith", 25)
  • Function Variables Map at time 21 = [ ]
  • Parameters List at time 21 = [ self, [ first_name, [ last_name, [ age, [ ] ] ] ] ]

then expression state at time 22 = "call_build_args"


Write Call Build Constructor Unchanged Variables At 21
if the following are true:
  • expression state at time 21 = "call_build_args"
  • the expression at time 21 = Person("John", "Smith", 25)
  • Function Variables Map at time 21 = [ ]
  • Parameters List at time 21 = [ self, [ first_name, [ last_name, [ age, [ ] ] ] ] ]
  • Variables Map at time 21 = [ ]

then Variables Map at time 22 = [ ]


Write Call Build Constructor Unchanged Stack At 21
if the following are true:
  • expression state at time 21 = "call_build_args"
  • the expression at time 21 = Person("John", "Smith", 25)
  • Function Variables Map at time 21 = [ ]
  • Parameters List at time 21 = [ self, [ first_name, [ last_name, [ age, [ ] ] ] ] ]
  • stack at time 21 = [ ]

then stack at time 22 = [ ]


Write Call Build Constructor Unchanged Control Map At 21
if the following are true:
  • expression state at time 21 = "call_build_args"
  • the expression at time 21 = Person("John", "Smith", 25)
  • Function Variables Map at time 21 = [ ]
  • Parameters List at time 21 = [ self, [ first_name, [ last_name, [ age, [ ] ] ] ] ]
  • Control Map at time 21 = [ entry 0: (pair ("class", "Person")), [ ] ]

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


Write Call Function Build Line At 21
if the following are true:
  • expression state at time 21 = "call_build_args"
  • Parameters List at time 21 = [ self, [ first_name, [ last_name, [ age, [ ] ] ] ] ]
  • the line at time 21 = 8

then the line at time 22 = 8


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

then the tab at time 22 = 0


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

then Value Stack at time 22 = [ ]


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

then arguments stack at time 22 = [ ]


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

then parent stack at time 22 = [ ]


Do Expr At Unchanged 21
if the following are true:
  • expression state at time 21 = "call_build_args"
  • the expression at time 21 = Person("John", "Smith", 25)

then the expression at time 22 = Person("John", "Smith", 25)


Do Class Defs At Unchanged 21
if the following are true:
  • expression state at time 21 = "call_build_args"
  • Class Map at time 21 = [ entry "Person": [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ first_name, [ last_name, [ age, [ ] ] ] ] ], [ entry "line": 2, [ ] ] ], [ entry "age_in_months": [ entry "params": [ self, [ ] ], [ entry "line": 6, [ ] ] ], [ ] ] ], [ entry "line": 1, [ ] ] ] ], [ ] ]

then Class Map at time 22 = [ entry "Person": [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ first_name, [ last_name, [ age, [ ] ] ] ] ], [ entry "line": 2, [ ] ] ], [ entry "age_in_months": [ entry "params": [ self, [ ] ], [ entry "line": 6, [ ] ] ], [ ] ] ], [ entry "line": 1, [ ] ] ] ], [ ] ]


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

Write Call Function Build Tmp 22
if the following are true:
  • expression state at time 22 = "call_build_args"
  • Function Variables Map at time 22 = [ entry self: (Python reference 0), [ ] ]
  • Parameters List at time 22 = [ first_name, [ last_name, [ age, [ ] ] ] ]
  • Argument Values at time 22 = [ "John", [ "Smith", [ 25, [ ] ] ] ]

then Function Variables Map at time 23 = [ entry self: (Python reference 0), [ entry first_name: "John", [ ] ] ]


Write Call Function Build Func Args 22
if the following are true:
  • expression state at time 22 = "call_build_args"
  • Parameters List at time 22 = [ first_name, [ last_name, [ age, [ ] ] ] ]
  • Argument Values at time 22 = [ "John", [ "Smith", [ 25, [ ] ] ] ]

then Parameters List at time 23 = [ last_name, [ age, [ ] ] ]


Write Call Function Build Values 22
if the following are true:
  • expression state at time 22 = "call_build_args"
  • Parameters List at time 22 = [ first_name, [ last_name, [ age, [ ] ] ] ]
  • Argument Values at time 22 = [ "John", [ "Smith", [ 25, [ ] ] ] ]

then Argument Values at time 23 = [ "Smith", [ 25, [ ] ] ]


Write Call Function Build State 22
if the following are true:
  • expression state at time 22 = "call_build_args"
  • Parameters List at time 22 = [ first_name, [ last_name, [ age, [ ] ] ] ]
  • Argument Values at time 22 = [ "John", [ "Smith", [ 25, [ ] ] ] ]

then expression state at time 23 = "call_build_args"


Write Call Function Build Variables 22
if the following are true:
  • expression state at time 22 = "call_build_args"
  • Parameters List at time 22 = [ first_name, [ last_name, [ age, [ ] ] ] ]
  • Argument Values at time 22 = [ "John", [ "Smith", [ 25, [ ] ] ] ]
  • Variables Map at time 22 = [ ]

then Variables Map at time 23 = [ ]


Write Call Function Build Stack 22
if the following are true:
  • expression state at time 22 = "call_build_args"
  • Parameters List at time 22 = [ first_name, [ last_name, [ age, [ ] ] ] ]
  • Argument Values at time 22 = [ "John", [ "Smith", [ 25, [ ] ] ] ]
  • stack at time 22 = [ ]

then stack at time 23 = [ ]


Write Call Function Build Object Store 22
if the following are true:
  • expression state at time 22 = "call_build_args"
  • Parameters List at time 22 = [ first_name, [ last_name, [ age, [ ] ] ] ]
  • Argument Values at time 22 = [ "John", [ "Smith", [ 25, [ ] ] ] ]
  • Python Object Store at time 22 = [ Python object: [ entry "__class_name__": "Person", [ ] ], [ ] ]

then Python Object Store at time 23 = [ Python object: [ entry "__class_name__": "Person", [ ] ], [ ] ]


Write Call Function Build Control Map 22
if the following are true:
  • expression state at time 22 = "call_build_args"
  • Parameters List at time 22 = [ first_name, [ last_name, [ age, [ ] ] ] ]
  • Argument Values at time 22 = [ "John", [ "Smith", [ 25, [ ] ] ] ]
  • Control Map at time 22 = [ entry 0: (pair ("class", "Person")), [ ] ]

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


Write Call Function Build Line At 22
if the following are true:
  • expression state at time 22 = "call_build_args"
  • Parameters List at time 22 = [ first_name, [ last_name, [ age, [ ] ] ] ]
  • the line at time 22 = 8

then the line at time 23 = 8


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

then the tab at time 23 = 0


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

then Value Stack at time 23 = [ ]


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

then arguments stack at time 23 = [ ]


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

then parent stack at time 23 = [ ]


Do Expr At Unchanged 22
if the following are true:
  • expression state at time 22 = "call_build_args"
  • the expression at time 22 = Person("John", "Smith", 25)

then the expression at time 23 = Person("John", "Smith", 25)


Do Class Defs At Unchanged 22
if the following are true:
  • expression state at time 22 = "call_build_args"
  • Class Map at time 22 = [ entry "Person": [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ first_name, [ last_name, [ age, [ ] ] ] ] ], [ entry "line": 2, [ ] ] ], [ entry "age_in_months": [ entry "params": [ self, [ ] ], [ entry "line": 6, [ ] ] ], [ ] ] ], [ entry "line": 1, [ ] ] ] ], [ ] ]

then Class Map at time 23 = [ entry "Person": [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ first_name, [ last_name, [ age, [ ] ] ] ] ], [ entry "line": 2, [ ] ] ], [ entry "age_in_months": [ entry "params": [ self, [ ] ], [ entry "line": 6, [ ] ] ], [ ] ] ], [ entry "line": 1, [ ] ] ] ], [ ] ]


Do Set Key Value 23 0
result of storing "Smith" at key: last_name in map: [ entry self: (Python reference 0), [ entry first_name: "John", [ ] ] ] = [ entry self: (Python reference 0), [ entry first_name: "John", [ entry last_name: "Smith", [ ] ] ] ]

Write Call Function Build Tmp 23
if the following are true:
  • expression state at time 23 = "call_build_args"
  • Function Variables Map at time 23 = [ entry self: (Python reference 0), [ entry first_name: "John", [ ] ] ]
  • Parameters List at time 23 = [ last_name, [ age, [ ] ] ]
  • Argument Values at time 23 = [ "Smith", [ 25, [ ] ] ]

then Function Variables Map at time 24 = [ entry self: (Python reference 0), [ entry first_name: "John", [ entry last_name: "Smith", [ ] ] ] ]


Write Call Function Build Func Args 23
if the following are true:
  • expression state at time 23 = "call_build_args"
  • Parameters List at time 23 = [ last_name, [ age, [ ] ] ]
  • Argument Values at time 23 = [ "Smith", [ 25, [ ] ] ]

then Parameters List at time 24 = [ age, [ ] ]


Write Call Function Build Values 23
if the following are true:
  • expression state at time 23 = "call_build_args"
  • Parameters List at time 23 = [ last_name, [ age, [ ] ] ]
  • Argument Values at time 23 = [ "Smith", [ 25, [ ] ] ]

then Argument Values at time 24 = [ 25, [ ] ]


Write Call Function Build State 23
if the following are true:
  • expression state at time 23 = "call_build_args"
  • Parameters List at time 23 = [ last_name, [ age, [ ] ] ]
  • Argument Values at time 23 = [ "Smith", [ 25, [ ] ] ]

then expression state at time 24 = "call_build_args"


Write Call Function Build Variables 23
if the following are true:
  • expression state at time 23 = "call_build_args"
  • Parameters List at time 23 = [ last_name, [ age, [ ] ] ]
  • Argument Values at time 23 = [ "Smith", [ 25, [ ] ] ]
  • Variables Map at time 23 = [ ]

then Variables Map at time 24 = [ ]


Write Call Function Build Stack 23
if the following are true:
  • expression state at time 23 = "call_build_args"
  • Parameters List at time 23 = [ last_name, [ age, [ ] ] ]
  • Argument Values at time 23 = [ "Smith", [ 25, [ ] ] ]
  • stack at time 23 = [ ]

then stack at time 24 = [ ]


Write Call Function Build Object Store 23
if the following are true:
  • expression state at time 23 = "call_build_args"
  • Parameters List at time 23 = [ last_name, [ age, [ ] ] ]
  • Argument Values at time 23 = [ "Smith", [ 25, [ ] ] ]
  • Python Object Store at time 23 = [ Python object: [ entry "__class_name__": "Person", [ ] ], [ ] ]

then Python Object Store at time 24 = [ Python object: [ entry "__class_name__": "Person", [ ] ], [ ] ]


Write Call Function Build Control Map 23
if the following are true:
  • expression state at time 23 = "call_build_args"
  • Parameters List at time 23 = [ last_name, [ age, [ ] ] ]
  • Argument Values at time 23 = [ "Smith", [ 25, [ ] ] ]
  • Control Map at time 23 = [ entry 0: (pair ("class", "Person")), [ ] ]

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


Write Call Function Build Line At 23
if the following are true:
  • expression state at time 23 = "call_build_args"
  • Parameters List at time 23 = [ last_name, [ age, [ ] ] ]
  • the line at time 23 = 8

then the line at time 24 = 8


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

then the tab at time 24 = 0


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

then Value Stack at time 24 = [ ]


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

then arguments stack at time 24 = [ ]


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

then parent stack at time 24 = [ ]


Do Expr At Unchanged 23
if the following are true:
  • expression state at time 23 = "call_build_args"
  • the expression at time 23 = Person("John", "Smith", 25)

then the expression at time 24 = Person("John", "Smith", 25)


Do Class Defs At Unchanged 23
if the following are true:
  • expression state at time 23 = "call_build_args"
  • Class Map at time 23 = [ entry "Person": [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ first_name, [ last_name, [ age, [ ] ] ] ] ], [ entry "line": 2, [ ] ] ], [ entry "age_in_months": [ entry "params": [ self, [ ] ], [ entry "line": 6, [ ] ] ], [ ] ] ], [ entry "line": 1, [ ] ] ] ], [ ] ]

then Class Map at time 24 = [ entry "Person": [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ first_name, [ last_name, [ age, [ ] ] ] ] ], [ entry "line": 2, [ ] ] ], [ entry "age_in_months": [ entry "params": [ self, [ ] ], [ entry "line": 6, [ ] ] ], [ ] ] ], [ entry "line": 1, [ ] ] ] ], [ ] ]


Do Set Key Value 24 0
result of storing 25 at key: age in map: [ entry self: (Python reference 0), [ entry first_name: "John", [ entry last_name: "Smith", [ ] ] ] ] = [ entry self: (Python reference 0), [ entry first_name: "John", [ entry last_name: "Smith", [ entry age: 25, [ ] ] ] ] ]

Write Call Function Build Tmp 24
if the following are true:
  • expression state at time 24 = "call_build_args"
  • Function Variables Map at time 24 = [ entry self: (Python reference 0), [ entry first_name: "John", [ entry last_name: "Smith", [ ] ] ] ]
  • Parameters List at time 24 = [ age, [ ] ]
  • Argument Values at time 24 = [ 25, [ ] ]

then Function Variables Map at time 25 = [ entry self: (Python reference 0), [ entry first_name: "John", [ entry last_name: "Smith", [ entry age: 25, [ ] ] ] ] ]


Write Call Function Build Func Args 24
if the following are true:
  • expression state at time 24 = "call_build_args"
  • Parameters List at time 24 = [ age, [ ] ]
  • Argument Values at time 24 = [ 25, [ ] ]

then Parameters List at time 25 = [ ]


Write Call Function Build Values 24
if the following are true:
  • expression state at time 24 = "call_build_args"
  • Parameters List at time 24 = [ age, [ ] ]
  • Argument Values at time 24 = [ 25, [ ] ]

then Argument Values at time 25 = [ ]


Write Call Function Build State 24
if the following are true:
  • expression state at time 24 = "call_build_args"
  • Parameters List at time 24 = [ age, [ ] ]
  • Argument Values at time 24 = [ 25, [ ] ]

then expression state at time 25 = "call_build_args"


Write Call Function Build Variables 24
if the following are true:
  • expression state at time 24 = "call_build_args"
  • Parameters List at time 24 = [ age, [ ] ]
  • Argument Values at time 24 = [ 25, [ ] ]
  • Variables Map at time 24 = [ ]

then Variables Map at time 25 = [ ]


Write Call Function Build Stack 24
if the following are true:
  • expression state at time 24 = "call_build_args"
  • Parameters List at time 24 = [ age, [ ] ]
  • Argument Values at time 24 = [ 25, [ ] ]
  • stack at time 24 = [ ]

then stack at time 25 = [ ]


Write Call Function Build Object Store 24
if the following are true:
  • expression state at time 24 = "call_build_args"
  • Parameters List at time 24 = [ age, [ ] ]
  • Argument Values at time 24 = [ 25, [ ] ]
  • Python Object Store at time 24 = [ Python object: [ entry "__class_name__": "Person", [ ] ], [ ] ]

then Python Object Store at time 25 = [ Python object: [ entry "__class_name__": "Person", [ ] ], [ ] ]


Write Call Function Build Control Map 24
if the following are true:
  • expression state at time 24 = "call_build_args"
  • Parameters List at time 24 = [ age, [ ] ]
  • Argument Values at time 24 = [ 25, [ ] ]
  • Control Map at time 24 = [ entry 0: (pair ("class", "Person")), [ ] ]

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


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

then the line at time 25 = 8


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

then the tab at time 25 = 0


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

then Value Stack at time 25 = [ ]


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

then arguments stack at time 25 = [ ]


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

then parent stack at time 25 = [ ]


Do Expr At Unchanged 24
if the following are true:
  • expression state at time 24 = "call_build_args"
  • the expression at time 24 = Person("John", "Smith", 25)

then the expression at time 25 = Person("John", "Smith", 25)


Do Class Defs At Unchanged 24
if the following are true:
  • expression state at time 24 = "call_build_args"
  • Class Map at time 24 = [ entry "Person": [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ first_name, [ last_name, [ age, [ ] ] ] ] ], [ entry "line": 2, [ ] ] ], [ entry "age_in_months": [ entry "params": [ self, [ ] ], [ entry "line": 6, [ ] ] ], [ ] ] ], [ entry "line": 1, [ ] ] ] ], [ ] ]

then Class Map at time 25 = [ entry "Person": [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ first_name, [ last_name, [ age, [ ] ] ] ] ], [ entry "line": 2, [ ] ] ], [ entry "age_in_months": [ entry "params": [ self, [ ] ], [ entry "line": 6, [ ] ] ], [ ] ] ], [ entry "line": 1, [ ] ] ] ], [ ] ]


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

then stack at time 26 = [ program context with variables: [ ] and expression state: (expression state with parent stack: [ ] arguments: [ ] values: [ ] line: 8 tab: 0) and control map: [ entry 0: (pair ("class", "Person")), [ ] ], [ ] ]


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

then Variables Map at time 26 = [ entry self: (Python reference 0), [ entry first_name: "John", [ entry last_name: "Smith", [ entry age: 25, [ ] ] ] ] ]


Do Get Key Value 25 0
value at "Person" in map [ entry "Person": [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ first_name, [ last_name, [ age, [ ] ] ] ] ], [ entry "line": 2, [ ] ] ], [ entry "age_in_months": [ entry "params": [ self, [ ] ], [ entry "line": 6, [ ] ] ], [ ] ] ], [ entry "line": 1, [ ] ] ] ], [ ] ] = [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ first_name, [ last_name, [ age, [ ] ] ] ] ], [ entry "line": 2, [ ] ] ], [ entry "age_in_months": [ entry "params": [ self, [ ] ], [ entry "line": 6, [ ] ] ], [ ] ] ], [ entry "line": 1, [ ] ] ] ]

Do Get Key Value 25 1
value at "methods" in map [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ first_name, [ last_name, [ age, [ ] ] ] ] ], [ entry "line": 2, [ ] ] ], [ entry "age_in_months": [ entry "params": [ self, [ ] ], [ entry "line": 6, [ ] ] ], [ ] ] ], [ entry "line": 1, [ ] ] ] ] = [ entry "__init__": [ entry "params": [ self, [ first_name, [ last_name, [ age, [ ] ] ] ] ], [ entry "line": 2, [ ] ] ], [ entry "age_in_months": [ entry "params": [ self, [ ] ], [ entry "line": 6, [ ] ] ], [ ] ] ]

Do Get Key Value 25 2
value at "__init__" in map [ entry "__init__": [ entry "params": [ self, [ first_name, [ last_name, [ age, [ ] ] ] ] ], [ entry "line": 2, [ ] ] ], [ entry "age_in_months": [ entry "params": [ self, [ ] ], [ entry "line": 6, [ ] ] ], [ ] ] ] = [ entry "params": [ self, [ first_name, [ last_name, [ age, [ ] ] ] ] ], [ entry "line": 2, [ ] ] ]

Do Get Key Value 25 3
value at "line" in map [ entry "params": [ self, [ first_name, [ last_name, [ age, [ ] ] ] ] ], [ entry "line": 2, [ ] ] ] = 2

Prove Find Method Def 25
definition of method "__init__" of class "Person" in [ entry "Person": [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ first_name, [ last_name, [ age, [ ] ] ] ] ], [ entry "line": 2, [ ] ] ], [ entry "age_in_months": [ entry "params": [ self, [ ] ], [ entry "line": 6, [ ] ] ], [ ] ] ], [ entry "line": 1, [ ] ] ] ], [ ] ] = [ entry "params": [ self, [ first_name, [ last_name, [ age, [ ] ] ] ] ], [ entry "line": 2, [ ] ] ]

Prove Find Method Line 25
if Class Map at time 25 = [ entry "Person": [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ first_name, [ last_name, [ age, [ ] ] ] ] ], [ entry "line": 2, [ ] ] ], [ entry "age_in_months": [ entry "params": [ self, [ ] ], [ entry "line": 6, [ ] ] ], [ ] ] ], [ entry "line": 1, [ ] ] ] ], [ ] ], then line number of method "__init__" of class "Person" in (Class Map at time 25) = 2

Jump To Constructor Property Example
if the following are true:
  • expression state at time 25 = "call_build_args"
  • Parameters List at time 25 = [ ]
  • the expression at time 25 = Person("John", "Smith", 25)
  • line number of method "__init__" of class "Person" in (Class Map at time 25) = 2

then the line at time 26 = 3


Jump To Constructor Tab Property Example
if the following are true:
  • expression state at time 25 = "call_build_args"
  • Parameters List at time 25 = [ ]
  • the expression at time 25 = Person("John", "Smith", 25)
  • line number of method "__init__" of class "Person" in (Class Map at time 25) = 2

then the tab at time 26 = 2


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

then expression state at time 26 = "not_expr"


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

then Python Object Store at time 26 = [ Python object: [ entry "__class_name__": "Person", [ ] ], [ ] ]


Jump To Constructor Push Property Example
if the following are true:
  • expression state at time 25 = "call_build_args"
  • Parameters List at time 25 = [ ]
  • the expression at time 25 = Person("John", "Smith", 25)
  • line number of method "__init__" of class "Person" in (Class Map at time 25) = 2

then Control Map at time 26 = [ entry 0: (pair ("class", "Person")), [ entry 1: (pair ("method", "__init__")), [ ] ] ]


Do Class Defs At Unchanged 25
if the following are true:
  • expression state at time 25 = "call_build_args"
  • Class Map at time 25 = [ entry "Person": [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ first_name, [ last_name, [ age, [ ] ] ] ] ], [ entry "line": 2, [ ] ] ], [ entry "age_in_months": [ entry "params": [ self, [ ] ], [ entry "line": 6, [ ] ] ], [ ] ] ], [ entry "line": 1, [ ] ] ] ], [ ] ]

then Class Map at time 26 = [ entry "Person": [ entry "bases": [ ], [ entry "methods": [ entry "__init__": [ entry "params": [ self, [ first_name, [ last_name, [ age, [ ] ] ] ] ], [ entry "line": 2, [ ] ] ], [ entry "age_in_months": [ entry "params": [ self, [ ] ], [ entry "line": 6, [ ] ] ], [ ] ] ], [ entry "line": 1, [ ] ] ] ], [ ] ]


Set Attribute Conversion Property Example
if statement at line 3, tab 2 = self.first_name = first_name, then statement at line 3, tab 2 = self."first_name" = first_name

Set Attribute Initial Property Example
if the following are true:
  • the line at time 26 = 3
  • the tab at time 26 = 2
  • statement at line 3, tab 2 = self."first_name" = first_name
  • expression state at time 26 = "not_expr"

then the expression at time 27 = self."first_name" = first_name


Write Set Name Expr State At on State 26
if the following are true:
  • the line at time 26 = 3
  • the tab at time 26 = 2
  • statement at line 3, tab 2 = self."first_name" = first_name
  • expression state at time 26 = "not_expr"

then expression state at time 27 = "begin_expr"


Write Set Name Line At on State 26
if the following are true:
  • the line at time 26 = 3
  • the tab at time 26 = 2
  • statement at line 3, tab 2 = self."first_name" = first_name
  • expression state at time 26 = "not_expr"

then the line at time 27 = 3


Write Set Name Tab At on State 26
if the following are true:
  • the line at time 26 = 3
  • the tab at time 26 = 2
  • statement at line 3, tab 2 = self."first_name" = first_name
  • expression state at time 26 = "not_expr"

then the tab at time 27 = 2


Write Set Name Value Stack At on State 26
if the following are true:
  • the line at time 26 = 3
  • the tab at time 26 = 2
  • statement at line 3, tab 2 = self."first_name" = first_name
  • expression state at time 26 = "not_expr"

then Value Stack at time 27 = [ ]


Write Set Name Parent Stack At on State 26
if the following are true:
  • the line at time 26 = 3
  • the tab at time 26 = 2
  • statement at line 3, tab 2 = self."first_name" = first_name
  • expression state at time 26 = "not_expr"

then parent stack at time 27 = [ ]


Write Set Name Arg Stack At on State 26
if the following are true:
  • the line at time 26 = 3
  • the tab at time 26 = 2
  • statement at line 3, tab 2 = self."first_name" = first_name
  • expression state at time 26 = "not_expr"

then arguments stack at time 27 = [ ]


Write Stmt Object Store At Unchanged Expr26
if the following are true:
  • the line at time 26 = 3
  • the tab at time 26 = 2
  • statement at line 3, tab 2 = self."first_name" = first_name
  • expression state at time 26 = "not_expr"
  • Python Object Store at time 26 = [ Python object: [ entry "__class_name__": "Person", [ ] ], [ ] ]

then Python Object Store at time 27 = [ Python object: [ entry "__class_name__": "Person", [ ] ], [ ] ]


Write Stmt Control Map At Unchanged Expr26
if the following are true:
  • the line at time 26 = 3
  • the tab at time 26 = 2
  • statement at line 3, tab 2 = self."first_name" = first_name
  • expression state at time 26 = "not_expr"
  • Control Map at time 26 = [ entry 0: (pair ("class", "Person")), [ entry 1: (pair ("method", "__init__")), [ ] ] ]

then Control Map at time 27 = [ entry 0: (pair ("class", "Person")), [ entry 1: (pair ("method", "__init__")), [ ] ] ]



Pages: 171 172 173 ... 193