Proofs

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

Do Line At Unchanged 51

if the following are true:

expression state at time 51 = "call_returned"
the line at time 51 = 8

then the line at time 52 = 8

Do Tab At Unchanged 51

if the following are true:

expression state at time 51 = "call_returned"
the tab at time 51 = 0

then the tab at time 52 = 0

Do Variables At Unchanged 51

if the following are true:

expression state at time 51 = "call_returned"
Variables Map at time 51 = [ ]

then Variables Map at time 52 = [ ]

Do Return Value At Unchanged 51

if the following are true:

expression state at time 51 = "call_returned"
Return Value at time 51 = Python reference 0

then Return Value at time 52 = Python reference 0

Do Stack At Unchanged 51

if the following are true:

expression state at time 51 = "call_returned"
stack at time 51 = [ ]

then stack at time 52 = [ ]

Do Parent Stack At Unchanged 51

if the following are true:

expression state at time 51 = "call_returned"
parent stack at time 51 = [ ]

then parent stack at time 52 = [ ]

Do Arg Stack At Unchanged 51

if the following are true:

expression state at time 51 = "call_returned"
arguments stack at time 51 = [ ]

then arguments stack at time 52 = [ ]

Do Object Store At Unchanged 51

if the following are true:

expression state at time 51 = "call_returned"
Python Object Store at time 51 = [ Python object: [ entry "__class_name__": "Person", [ entry "first_name": "John", [ entry "last_name": "Smith", [ entry "age": 25, [ ] ] ] ] ], [ ] ]

then Python Object Store at time 52 = [ Python object: [ entry "__class_name__": "Person", [ entry "first_name": "John", [ entry "last_name": "Smith", [ entry "age": 25, [ ] ] ] ] ], [ ] ]

Do Value Stack At Unchanged 51

if the following are true:

expression state at time 51 = "call_returned"
Value Stack at time 51 = [ ]

then Value Stack at time 52 = [ ]

Do Control Map At Unchanged 51

if the following are true:

expression state at time 51 = "call_returned"
Control Map at time 51 = [ entry 0: (pair ("class", "Person")), [ ] ]

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

Do Class Defs At Unchanged 51

if the following are true:

expression state at time 51 = "call_returned"
Class Map at time 51 = [ 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 52 = [ 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 52 0

result of storing (Python reference 0) at key: p in map: [ ] = [ entry p: (Python reference 0), [ ] ]

Assign Constructor to Variable Property Example

if the following are true:

the line at time 52 = 8
the tab at time 52 = 0
statement at line 8, tab 0 = p = Person("John", "Smith", 25)
expression state at time 52 = "end_expr"
Variables Map at time 52 = [ ]
Return Value at time 52 = Python reference 0

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

Write Increment T And Val Line At 52

if the following are true:

the line at time 52 = 8
the tab at time 52 = 0
statement at line 8, tab 0 = p = Person("John", "Smith", 25)
expression state at time 52 = "end_expr"

then the line at time 53 = 9

Write Stmt Tab At Unchanged Expr52

if the following are true:

the line at time 52 = 8
the tab at time 52 = 0
statement at line 8, tab 0 = p = Person("John", "Smith", 25)
expression state at time 52 = "end_expr"

then the tab at time 53 = 0

Write Stmt Object Store At Unchanged Expr52

if the following are true:

the line at time 52 = 8
the tab at time 52 = 0
statement at line 8, tab 0 = p = Person("John", "Smith", 25)
expression state at time 52 = "end_expr"
Python Object Store at time 52 = [ Python object: [ entry "__class_name__": "Person", [ entry "first_name": "John", [ entry "last_name": "Smith", [ entry "age": 25, [ ] ] ] ] ], [ ] ]

then Python Object Store at time 53 = [ Python object: [ entry "__class_name__": "Person", [ entry "first_name": "John", [ entry "last_name": "Smith", [ entry "age": 25, [ ] ] ] ] ], [ ] ]

Write Assign End Stack 52

if the following are true:

the line at time 52 = 8
the tab at time 52 = 0
statement at line 8, tab 0 = p = Person("John", "Smith", 25)
stack at time 52 = [ ]
expression state at time 52 = "end_expr"

then stack at time 53 = [ ]

Write End to Not Expr 52

if expression state at time 52 = "end_expr", then expression state at time 53 = "not_expr"

Write Stmt Control Map At Unchanged 52

if the following are true:

the line at time 52 = 8
the tab at time 52 = 0
statement at line 8, tab 0 = p = Person("John", "Smith", 25)
Control Map at time 52 = [ entry 0: (pair ("class", "Person")), [ ] ]

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

Write Stmt Class Defs At Unchanged 52

if the following are true:

the line at time 52 = 8
the tab at time 52 = 0
statement at line 8, tab 0 = p = Person("John", "Smith", 25)
Class Map at time 52 = [ 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 53 = [ 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 Set Name Expr At on State 53

if the following are true:

the line at time 53 = 9
the tab at time 53 = 0
statement at line 9, tab 0 = age = p.age_in_months()
expression state at time 53 = "not_expr"

then the expression at time 54 = p.age_in_months()

Write Set Name Expr State At on State 53

if the following are true:

the line at time 53 = 9
the tab at time 53 = 0
statement at line 9, tab 0 = age = p.age_in_months()
expression state at time 53 = "not_expr"

then expression state at time 54 = "begin_expr"

Write Set Name Line At on State 53

if the following are true:

the line at time 53 = 9
the tab at time 53 = 0
statement at line 9, tab 0 = age = p.age_in_months()
expression state at time 53 = "not_expr"

then the line at time 54 = 9

Write Set Name Tab At on State 53

if the following are true:

the line at time 53 = 9
the tab at time 53 = 0
statement at line 9, tab 0 = age = p.age_in_months()
expression state at time 53 = "not_expr"

then the tab at time 54 = 0

Write Set Name Value Stack At on State 53

if the following are true:

the line at time 53 = 9
the tab at time 53 = 0
statement at line 9, tab 0 = age = p.age_in_months()
expression state at time 53 = "not_expr"

then Value Stack at time 54 = [ ]

Write Set Name Parent Stack At on State 53

if the following are true:

the line at time 53 = 9
the tab at time 53 = 0
statement at line 9, tab 0 = age = p.age_in_months()
expression state at time 53 = "not_expr"

then parent stack at time 54 = [ ]

Write Set Name Arg Stack At on State 53

if the following are true:

the line at time 53 = 9
the tab at time 53 = 0
statement at line 9, tab 0 = age = p.age_in_months()
expression state at time 53 = "not_expr"

then arguments stack at time 54 = [ ]

Write Stmt Variables At Unchanged Expr53

if the following are true:

the line at time 53 = 9
the tab at time 53 = 0
statement at line 9, tab 0 = age = p.age_in_months()
expression state at time 53 = "not_expr"
Variables Map at time 53 = [ entry p: (Python reference 0), [ ] ]

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

Write Stmt Stack At Unchanged Expr53

if the following are true:

the line at time 53 = 9
the tab at time 53 = 0
statement at line 9, tab 0 = age = p.age_in_months()
expression state at time 53 = "not_expr"
stack at time 53 = [ ]

then stack at time 54 = [ ]

Write Stmt Object Store At Unchanged Expr53

if the following are true:

the line at time 53 = 9
the tab at time 53 = 0
statement at line 9, tab 0 = age = p.age_in_months()
expression state at time 53 = "not_expr"
Python Object Store at time 53 = [ Python object: [ entry "__class_name__": "Person", [ entry "first_name": "John", [ entry "last_name": "Smith", [ entry "age": 25, [ ] ] ] ] ], [ ] ]

then Python Object Store at time 54 = [ Python object: [ entry "__class_name__": "Person", [ entry "first_name": "John", [ entry "last_name": "Smith", [ entry "age": 25, [ ] ] ] ] ], [ ] ]

Write Stmt Control Map At Unchanged 53

if the following are true:

the line at time 53 = 9
the tab at time 53 = 0
statement at line 9, tab 0 = age = p.age_in_months()
Control Map at time 53 = [ entry 0: (pair ("class", "Person")), [ ] ]

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

Write Stmt Class Defs At Unchanged 53

if the following are true:

the line at time 53 = 9
the tab at time 53 = 0
statement at line 9, tab 0 = age = p.age_in_months()
Class Map at time 53 = [ 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 54 = [ 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, [ ] ] ] ], [ ] ]

Get Begin Expr Value 54

if the following are true:

expression state at time 54 = "begin_expr"
the expression at time 54 = p.age_in_months()
Value Stack at time 54 = [ ]

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

Get Begin Expr Parent 54

if the following are true:

expression state at time 54 = "begin_expr"
the expression at time 54 = p.age_in_months()
parent stack at time 54 = [ ]

then parent stack at time 55 = [ p.age_in_months(), [ ] ]

Push Method Arguments Example

if the following are true:

expression state at time 54 = "begin_expr"
the expression at time 54 = p.age_in_months()
arguments stack at time 54 = [ ]

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

Get Begin Expr Call State 54

if the following are true:

expression state at time 54 = "begin_expr"
the expression at time 54 = p.age_in_months()

then expression state at time 55 = "iterate_args"

Do Expr At Unchanged 54

if the following are true:

expression state at time 54 = "begin_expr"
the expression at time 54 = p.age_in_months()

then the expression at time 55 = p.age_in_months()

Do Variables At Unchanged 54

if the following are true:

expression state at time 54 = "begin_expr"
Variables Map at time 54 = [ entry p: (Python reference 0), [ ] ]

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

Do Line At Unchanged 54

if the following are true:

expression state at time 54 = "begin_expr"
the line at time 54 = 9

then the line at time 55 = 9

Do Tab At Unchanged 54

if the following are true:

expression state at time 54 = "begin_expr"
the tab at time 54 = 0

then the tab at time 55 = 0

Do Stack At Unchanged 54

if the following are true:

expression state at time 54 = "begin_expr"
stack at time 54 = [ ]

then stack at time 55 = [ ]

Do Object Store At Unchanged 54

if the following are true:

expression state at time 54 = "begin_expr"
Python Object Store at time 54 = [ Python object: [ entry "__class_name__": "Person", [ entry "first_name": "John", [ entry "last_name": "Smith", [ entry "age": 25, [ ] ] ] ] ], [ ] ]

then Python Object Store at time 55 = [ Python object: [ entry "__class_name__": "Person", [ entry "first_name": "John", [ entry "last_name": "Smith", [ entry "age": 25, [ ] ] ] ] ], [ ] ]

Do Control Map At Unchanged 54

if the following are true:

expression state at time 54 = "begin_expr"
Control Map at time 54 = [ entry 0: (pair ("class", "Person")), [ ] ]

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

Do Class Defs At Unchanged 54

if the following are true:

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

Get Iterate End State 55

if the following are true:

expression state at time 55 = "iterate_args"
arguments stack at time 55 = [ [ ], [ ] ]
parent stack at time 55 = [ p.age_in_months(), [ ] ]

then expression state at time 56 = "call_function_begin"

Get Iterate End Expr 55

if the following are true:

expression state at time 55 = "iterate_args"
arguments stack at time 55 = [ [ ], [ ] ]
parent stack at time 55 = [ p.age_in_months(), [ ] ]

then the expression at time 56 = p.age_in_months()

Get Iterate End Parent 55

if the following are true:

expression state at time 55 = "iterate_args"
arguments stack at time 55 = [ [ ], [ ] ]
parent stack at time 55 = [ p.age_in_months(), [ ] ]

then parent stack at time 56 = [ ]

Get Iterate End Params 55

if the following are true:

expression state at time 55 = "iterate_args"
arguments stack at time 55 = [ [ ], [ ] ]
parent stack at time 55 = [ p.age_in_months(), [ ] ]

then arguments stack at time 56 = [ ]

Do Value Stack At Unchanged 55

if the following are true:

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

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

Do Line At Unchanged 55

if the following are true:

expression state at time 55 = "iterate_args"
the line at time 55 = 9

then the line at time 56 = 9

Do Tab At Unchanged 55

if the following are true:

expression state at time 55 = "iterate_args"
the tab at time 55 = 0

then the tab at time 56 = 0

Do Stack At Unchanged 55

if the following are true:

expression state at time 55 = "iterate_args"
stack at time 55 = [ ]

then stack at time 56 = [ ]

Do Object Store At Unchanged 55

if the following are true:

expression state at time 55 = "iterate_args"
Python Object Store at time 55 = [ Python object: [ entry "__class_name__": "Person", [ entry "first_name": "John", [ entry "last_name": "Smith", [ entry "age": 25, [ ] ] ] ] ], [ ] ]

then Python Object Store at time 56 = [ Python object: [ entry "__class_name__": "Person", [ entry "first_name": "John", [ entry "last_name": "Smith", [ entry "age": 25, [ ] ] ] ] ], [ ] ]

Do Control Map At Unchanged 55

if the following are true:

expression state at time 55 = "iterate_args"
Control Map at time 55 = [ entry 0: (pair ("class", "Person")), [ ] ]

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

Do Variables At Unchanged 55

if the following are true:

expression state at time 55 = "iterate_args"
Variables Map at time 55 = [ entry p: (Python reference 0), [ ] ]

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

Do Class Defs At Unchanged 55

if the following are true:

expression state at time 55 = "iterate_args"
Class Map at time 55 = [ 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 56 = [ 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 Expr At Unchanged 56

if the following are true:

expression state at time 56 = "call_function_begin"
the expression at time 56 = p.age_in_months()

then the expression at time 57 = p.age_in_months()

Do Get Key Value 56 0

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

Get Key Value Variables At 56

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

Do Element At 56 0

the element at index 0 of stack [ Python object: [ entry "__class_name__": "Person", [ entry "first_name": "John", [ entry "last_name": "Smith", [ entry "age": 25, [ ] ] ] ] ], [ ] ] = Python object: [ entry "__class_name__": "Person", [ entry "first_name": "John", [ entry "last_name": "Smith", [ entry "age": 25, [ ] ] ] ] ]

Write Element At Object Store 56

if Python Object Store at time 56 = [ Python object: [ entry "__class_name__": "Person", [ entry "first_name": "John", [ entry "last_name": "Smith", [ entry "age": 25, [ ] ] ] ] ], [ ] ], then the element at index 0 of stack (Python Object Store at time 56) = Python object: [ entry "__class_name__": "Person", [ entry "first_name": "John", [ entry "last_name": "Smith", [ entry "age": 25, [ ] ] ] ] ]

Do Has Key 56 0

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, [ ] ] ] ], [ ] ] contains key "Person" = True

Write Call Function Begin Method Call Has 56

if Class Map at time 56 = [ 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 map (Class Map at time 56) contains key "Person" = True

Write Call Function Begin Method Call State 56

if the following are true:

expression state at time 56 = "call_function_begin"
the expression at time 56 = p.age_in_months()
value at p in map (Variables Map at time 56) = Python reference 0
the element at index 0 of stack (Python Object Store at time 56) = Python object: [ entry "__class_name__": "Person", [ entry "first_name": "John", [ entry "last_name": "Smith", [ entry "age": 25, [ ] ] ] ] ]
map (Class Map at time 56) contains key "Person" = True

then expression state at time 57 = "call_build_args"

Write Call Function Begin Tmp Vars 56

if expression state at time 56 = "call_function_begin", then Function Variables Map at time 57 = [ ]

Do Get Key Value 56 4

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 56 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 56 2

value at "age_in_months" 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, [ ] ], [ entry "line": 6, [ ] ] ]

Do Get Key Value 56 3

value at "params" in map [ entry "params": [ self, [ ] ], [ entry "line": 6, [ ] ] ] = [ self, [ ] ]

Prove Find Method Def 56

definition of method "age_in_months" 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, [ ] ], [ entry "line": 6, [ ] ] ]

Prove Find Method Def At 56

if Class Map at time 56 = [ 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 definition of method "age_in_months" of class "Person" in (Class Map at time 56) = [ entry "params": [ self, [ ] ], [ entry "line": 6, [ ] ] ]

Prove Find Method Params 56

if Class Map at time 56 = [ 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 method parameters where the Class Map is (Class Map at time 56), class name is "Person", and method name is "age_in_months" = [ self, [ ] ]

Copy Method Parameters Property Example

if the following are true:

expression state at time 56 = "call_function_begin"
the expression at time 56 = p.age_in_months()
value at p in map (Variables Map at time 56) = Python reference 0
the element at index 0 of stack (Python Object Store at time 56) = Python object: [ entry "__class_name__": "Person", [ entry "first_name": "John", [ entry "last_name": "Smith", [ entry "age": 25, [ ] ] ] ] ]
method parameters where the Class Map is (Class Map at time 56), class name is "Person", and method name is "age_in_months" = [ self, [ ] ]

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

Do Reverse 56 0

reverse of "[]" = reverse of remaining stack "[]" and already reversed stack [ ]

Push Self To Values Property Example

if the following are true:

expression state at time 56 = "call_function_begin"
Value Stack at time 56 = [ [ ], [ ] ]
the expression at time 56 = p.age_in_months()
value at p in map (Variables Map at time 56) = Python reference 0
the element at index 0 of stack (Python Object Store at time 56) = Python object: [ entry "__class_name__": "Person", [ entry "first_name": "John", [ entry "last_name": "Smith", [ entry "age": 25, [ ] ] ] ] ]
definition of method "age_in_months" of class "Person" in (Class Map at time 56) = [ entry "params": [ self, [ ] ], [ entry "line": 6, [ ] ] ]

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

Write Call Function Begin Method Call Object Store 56

if the following are true:

expression state at time 56 = "call_function_begin"
the expression at time 56 = p.age_in_months()
value at p in map (Variables Map at time 56) = Python reference 0
the element at index 0 of stack (Python Object Store at time 56) = Python object: [ entry "__class_name__": "Person", [ entry "first_name": "John", [ entry "last_name": "Smith", [ entry "age": 25, [ ] ] ] ] ]
method parameters where the Class Map is (Class Map at time 56), class name is "Person", and method name is "age_in_months" = [ self, [ ] ]
Python Object Store at time 56 = [ Python object: [ entry "__class_name__": "Person", [ entry "first_name": "John", [ entry "last_name": "Smith", [ entry "age": 25, [ ] ] ] ] ], [ ] ]

then Python Object Store at time 57 = [ Python object: [ entry "__class_name__": "Person", [ entry "first_name": "John", [ entry "last_name": "Smith", [ entry "age": 25, [ ] ] ] ] ], [ ] ]

Write Call Function Begin Value Stack 56

if the following are true:

expression state at time 56 = "call_function_begin"
Value Stack at time 56 = [ [ ], [ ] ]
the expression at time 56 = p.age_in_months()

then Value Stack at time 57 = [ ]

Do Arg Stack At Unchanged 56

if the following are true:

expression state at time 56 = "call_function_begin"
arguments stack at time 56 = [ ]

then arguments stack at time 57 = [ ]

Do Parent Stack At Unchanged 56

if the following are true:

expression state at time 56 = "call_function_begin"
parent stack at time 56 = [ ]

then parent stack at time 57 = [ ]

Do Control Map At Unchanged 56

if the following are true:

expression state at time 56 = "call_function_begin"
Control Map at time 56 = [ entry 0: (pair ("class", "Person")), [ ] ]

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

Do Variables At Unchanged 56

if the following are true:

expression state at time 56 = "call_function_begin"
Variables Map at time 56 = [ entry p: (Python reference 0), [ ] ]

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

Do Line At Unchanged 56

if the following are true:

expression state at time 56 = "call_function_begin"
the line at time 56 = 9

then the line at time 57 = 9

Do Tab At Unchanged 56

if the following are true:

expression state at time 56 = "call_function_begin"
the tab at time 56 = 0

then the tab at time 57 = 0

Do Stack At Unchanged 56

if the following are true:

expression state at time 56 = "call_function_begin"
stack at time 56 = [ ]

then stack at time 57 = [ ]

Do Class Defs At Unchanged 56

if the following are true:

expression state at time 56 = "call_function_begin"
Class Map at time 56 = [ 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 57 = [ 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 57 0

result of storing (Python reference 0) at key: self in map: [ ] = [ entry self: (Python reference 0), [ ] ]

Write Call Function Build Tmp 57

if the following are true:

expression state at time 57 = "call_build_args"
Function Variables Map at time 57 = [ ]
Parameters List at time 57 = [ self, [ ] ]
Argument Values at time 57 = [ Python reference 0, [ ] ]

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

Write Call Function Build Func Args 57

if the following are true:

expression state at time 57 = "call_build_args"
Parameters List at time 57 = [ self, [ ] ]
Argument Values at time 57 = [ Python reference 0, [ ] ]

then Parameters List at time 58 = [ ]

Write Call Function Build Values 57

if the following are true:

expression state at time 57 = "call_build_args"
Parameters List at time 57 = [ self, [ ] ]
Argument Values at time 57 = [ Python reference 0, [ ] ]

then Argument Values at time 58 = [ ]

Write Call Function Build State 57

if the following are true:

expression state at time 57 = "call_build_args"
Parameters List at time 57 = [ self, [ ] ]
Argument Values at time 57 = [ Python reference 0, [ ] ]

then expression state at time 58 = "call_build_args"

Write Call Function Build Variables 57

if the following are true:

expression state at time 57 = "call_build_args"
Parameters List at time 57 = [ self, [ ] ]
Argument Values at time 57 = [ Python reference 0, [ ] ]
Variables Map at time 57 = [ entry p: (Python reference 0), [ ] ]

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

Write Call Function Build Stack 57

if the following are true:

expression state at time 57 = "call_build_args"
Parameters List at time 57 = [ self, [ ] ]
Argument Values at time 57 = [ Python reference 0, [ ] ]
stack at time 57 = [ ]

then stack at time 58 = [ ]

Write Call Function Build Object Store 57

if the following are true:

expression state at time 57 = "call_build_args"
Parameters List at time 57 = [ self, [ ] ]
Argument Values at time 57 = [ Python reference 0, [ ] ]
Python Object Store at time 57 = [ Python object: [ entry "__class_name__": "Person", [ entry "first_name": "John", [ entry "last_name": "Smith", [ entry "age": 25, [ ] ] ] ] ], [ ] ]

then Python Object Store at time 58 = [ Python object: [ entry "__class_name__": "Person", [ entry "first_name": "John", [ entry "last_name": "Smith", [ entry "age": 25, [ ] ] ] ] ], [ ] ]