Conditional Properties

In each statement, if the test expression is true, then the conclusion expression is also assumed to be true. Conditional properties are used to prove theorems.

Begin PyDict Elements (3)

if Expression Stack at time t = [ [ Python dictionary entries, ys ], rest ], then Parameters List at time (t + 1) = None

Begin PyDict Elements (4)

if Expression Stack at time t = [ [ Python dictionary entries, ys ], rest ], then the line at time (t + 1) = the line at time t

Begin PyDict Elements (5)

if Expression Stack at time t = [ [ Python dictionary entries, ys ], rest ], then the tab at time (t + 1) = the tab at time t

Begin PyDict Elements (6)

if Expression Stack at time t = [ [ Python dictionary entries, ys ], rest ], then Variables Map at time (t + 1) = Variables Map at time t

Begin PyDict Elements (7)

if Expression Stack at time t = [ [ Python dictionary entries, ys ], rest ], then Control Map at time (t + 1) = Control Map at time t

Begin PyDict Elements (8)

if Expression Stack at time t = [ [ Python dictionary entries, ys ], rest ], then Python Object Store at time (t + 1) = Python Object Store at time t

Begin PyDict Elements (9)

if Expression Stack at time t = [ [ Python dictionary entries, ys ], rest ], then Context Stack at time (t + 1) = Context Stack at time t

Call Func PyDict (1)

if the following are true:

Expression Stack at time t = [ [ ], [ [ Python dictionary entries, ys ], rest ] ]
Value Stack at time t = [ values, [ next_level, other_levels ] ]

then Value Stack at time (t + 1) = [ [ Python reference (length of stack (Python Object Store at time t)), next_level ], other_levels ]

Call Func PyDict (2)

if the following are true:

Expression Stack at time t = [ [ ], [ [ Python dictionary entries, ys ], rest ] ]
Value Stack at time t = [ values, [ next_level, other_levels ] ]

then Python Object Store at time (t + 1) = result of appending (Python dictionary (reverse of values)) to (Python Object Store at time t)

Call Func PyDict Effect (1)

if Expression Stack at time t = [ [ ], [ [ Python dictionary entries, ys ], rest ] ], then Expression Stack at time (t + 1) = [ ys, rest ]

Call Func PyDict Effect (2)

if Expression Stack at time t = [ [ ], [ [ Python dictionary entries, ys ], rest ] ], then the line at time (t + 1) = the line at time t

Call Func PyDict Effect (3)

if Expression Stack at time t = [ [ ], [ [ Python dictionary entries, ys ], rest ] ], then the tab at time (t + 1) = the tab at time t

Call Func PyDict Effect (4)

if Expression Stack at time t = [ [ ], [ [ Python dictionary entries, ys ], rest ] ], then Variables Map at time (t + 1) = Variables Map at time t

Call Func PyDict Effect (5)

if Expression Stack at time t = [ [ ], [ [ Python dictionary entries, ys ], rest ] ], then Control Map at time (t + 1) = Control Map at time t

Call Func PyDict Effect (6)

if Expression Stack at time t = [ [ ], [ [ Python dictionary entries, ys ], rest ] ], then Context Stack at time (t + 1) = Context Stack at time t

Begin PyDict Entry Elements (1)

if Expression Stack at time t = [ [ entry key: value, ys ], rest ], then Expression Stack at time (t + 1) = [ [ key, [ value, [ ] ] ], [ [ entry key: value, ys ], rest ] ]

Begin PyDict Entry Elements (2)

if Expression Stack at time t = [ [ entry key: value, ys ], rest ], then Value Stack at time (t + 1) = [ [ ], Value Stack at time t ]

Begin PyDict Entry Elements (3)

if Expression Stack at time t = [ [ entry key: value, ys ], rest ], then Parameters List at time (t + 1) = None

Begin PyDict Entry Elements (4)

if Expression Stack at time t = [ [ entry key: value, ys ], rest ], then the line at time (t + 1) = the line at time t

Begin PyDict Entry Elements (5)

if Expression Stack at time t = [ [ entry key: value, ys ], rest ], then the tab at time (t + 1) = the tab at time t

Begin PyDict Entry Elements (6)

if Expression Stack at time t = [ [ entry key: value, ys ], rest ], then Variables Map at time (t + 1) = Variables Map at time t

Begin PyDict Entry Elements (7)

if Expression Stack at time t = [ [ entry key: value, ys ], rest ], then Control Map at time (t + 1) = Control Map at time t

Begin PyDict Entry Elements (8)

if Expression Stack at time t = [ [ entry key: value, ys ], rest ], then Python Object Store at time (t + 1) = Python Object Store at time t

Begin PyDict Entry Elements (9)

if Expression Stack at time t = [ [ entry key: value, ys ], rest ], then Context Stack at time (t + 1) = Context Stack at time t

Call Func PyDict Entry

if the following are true:

Expression Stack at time t = [ [ ], [ [ entry key: value, ys ], rest ] ]
Value Stack at time t = [ [ evaluated_value, [ evaluated_key, [ ] ] ], [ next_level, other_levels ] ]

then Value Stack at time (t + 1) = [ [ entry evaluated_key: evaluated_value, next_level ], other_levels ]

When PyDict Entry Is Evaluated (1)

if Expression Stack at time t = [ [ ], [ [ entry key: value, ys ], rest ] ], then Expression Stack at time (t + 1) = [ ys, rest ]

When PyDict Entry Is Evaluated (2)

if Expression Stack at time t = [ [ ], [ [ entry key: value, ys ], rest ] ], then the line at time (t + 1) = the line at time t

When PyDict Entry Is Evaluated (3)

if Expression Stack at time t = [ [ ], [ [ entry key: value, ys ], rest ] ], then the tab at time (t + 1) = the tab at time t

When PyDict Entry Is Evaluated (4)

if Expression Stack at time t = [ [ ], [ [ entry key: value, ys ], rest ] ], then Variables Map at time (t + 1) = Variables Map at time t

When PyDict Entry Is Evaluated (5)

if Expression Stack at time t = [ [ ], [ [ entry key: value, ys ], rest ] ], then Control Map at time (t + 1) = Control Map at time t

When PyDict Entry Is Evaluated (6)

if Expression Stack at time t = [ [ ], [ [ entry key: value, ys ], rest ] ], then Context Stack at time (t + 1) = Context Stack at time t

When PyDict Entry Is Evaluated (7)

if Expression Stack at time t = [ [ ], [ [ entry key: value, ys ], rest ] ], then Python Object Store at time (t + 1) = Python Object Store at time t

Assign PyDict (1)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = assign statement with target x and expression (Python dictionary elements)
Expression Stack at time t = [ ]

then Expression Stack at time (t + 1) = [ [ Python dictionary elements, [ ] ], [ ] ]

Assign PyDict (2)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = assign statement with target x and expression (Python dictionary elements)
Expression Stack at time t = [ ]

then the line at time (t + 1) = i

Assign PyDict (3)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = assign statement with target x and expression (Python dictionary elements)
Expression Stack at time t = [ ]

then the tab at time (t + 1) = j

Assign PyDict (4)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = assign statement with target x and expression (Python dictionary elements)
Expression Stack at time t = [ ]

then Variables Map at time (t + 1) = Variables Map at time t

Assign PyDict (5)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = assign statement with target x and expression (Python dictionary elements)
Expression Stack at time t = [ ]

then Context Stack at time (t + 1) = Context Stack at time t

Assign PyDict (6)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = assign statement with target x and expression (Python dictionary elements)
Expression Stack at time t = [ ]

then Value Stack at time (t + 1) = [ [ ], [ ] ]

Assign PyDict (7)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = assign statement with target x and expression (Python dictionary elements)
Expression Stack at time t = [ ]

then Python Object Store at time (t + 1) = Python Object Store at time t

Get PyDict Item Value

if the following are true:

Expression Stack at time t = [ [ ], [ [ function call with name: "__getitem__" and arguments: args, ys ], rest ] ]
Value Stack at time t = [ [ a, [ Python reference idx, [ ] ] ], [ next_level, other_levels ] ]
the element at index idx of stack (Python Object Store at time t) = Python dictionary entries

then Value Stack at time (t + 1) = [ [ value at a in map entries, next_level ], other_levels ]

Set PyDict Entry (1)

if the following are true:

Expression Stack at time t = [ [ ], [ [ function call with name: "__setitem__" and arguments: args, ys ], rest ] ]
Value Stack at time t = [ [ value, [ key, [ Python reference idx, [ ] ] ] ], [ next_level, other_levels ] ]
the element at index idx of stack (Python Object Store at time t) = Python dictionary entries

then Python Object Store at time (t + 1) = result of storing (Python dictionary (result of storing value at key: key in map: entries)) at index idx of stack (Python Object Store at time t)

Set PyDict Entry (2)

if the following are true:

Expression Stack at time t = [ [ ], [ [ function call with name: "__setitem__" and arguments: args, ys ], rest ] ]
Value Stack at time t = [ [ value, [ key, [ Python reference idx, [ ] ] ] ], [ next_level, other_levels ] ]
the element at index idx of stack (Python Object Store at time t) = Python dictionary entries

then Value Stack at time (t + 1) = [ [ None, next_level ], other_levels ]

Set Item On PyList (1)

if the following are true:

Expression Stack at time t = [ [ ], [ [ function call with name: "__setitem__" and arguments: args, ys ], rest ] ]
Value Stack at time t = [ [ value, [ key, [ Python reference idx, [ ] ] ] ], [ next_level, other_levels ] ]
the element at index idx of stack (Python Object Store at time t) = Python list elements

then Python Object Store at time (t + 1) = result of storing (Python list (result of storing value at index key of stack elements)) at index idx of stack (Python Object Store at time t)

Set Item On PyList (2)

if the following are true:

Expression Stack at time t = [ [ ], [ [ function call with name: "__setitem__" and arguments: args, ys ], rest ] ]
Value Stack at time t = [ [ value, [ key, [ Python reference idx, [ ] ] ] ], [ next_level, other_levels ] ]
the element at index idx of stack (Python Object Store at time t) = Python list elements

then Value Stack at time (t + 1) = [ [ None, next_level ], other_levels ]

Python setitem unchanged

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = function call with name: "__setitem__" and arguments: args
Expression Stack at time t = [ ]

then Python Object Store at time (t + 1) = Python Object Store at time t

When Python setitem Is Evaluated (1)

if Expression Stack at time t = [ [ ], [ [ function call with name: "__setitem__" and arguments: args, ys ], rest ] ], then Expression Stack at time (t + 1) = [ ys, rest ]

When Python setitem Is Evaluated (2)

if Expression Stack at time t = [ [ ], [ [ function call with name: "__setitem__" and arguments: args, ys ], rest ] ], then the line at time (t + 1) = the line at time t

When Python setitem Is Evaluated (3)

if Expression Stack at time t = [ [ ], [ [ function call with name: "__setitem__" and arguments: args, ys ], rest ] ], then the tab at time (t + 1) = the tab at time t

When Python setitem Is Evaluated (4)

if Expression Stack at time t = [ [ ], [ [ function call with name: "__setitem__" and arguments: args, ys ], rest ] ], then Variables Map at time (t + 1) = Variables Map at time t

When Python setitem Is Evaluated (5)

if Expression Stack at time t = [ [ ], [ [ function call with name: "__setitem__" and arguments: args, ys ], rest ] ], then Control Map at time (t + 1) = Control Map at time t

When Python setitem Is Evaluated (6)

if Expression Stack at time t = [ [ ], [ [ function call with name: "__setitem__" and arguments: args, ys ], rest ] ], then Context Stack at time (t + 1) = Context Stack at time t

Python Class Definition (1)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = a class named name with bases: bases

then Class Map at time (t + 1) = result of storing [ entry "bases": bases, [ entry "methods": [ ], [ entry "line": i, [ ] ] ] ] at key: name in map: (Class Map at time t)

Python Class Definition (2)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = a class named name with bases: bases

then Control Map at time (t + 1) = result of storing (pair ("class", name)) at key: j in map: (Control Map at time t)

Python Class Definition (3)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = a class named name with bases: bases

then the line at time (t + 1) = i + 1

Python Class Definition (4)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = a class named name with bases: bases

then the tab at time (t + 1) = j + 1

Python Class Definition (5)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = a class named name with bases: bases

then Variables Map at time (t + 1) = Variables Map at time t

Python Class Definition (6)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = a class named name with bases: bases

then Context Stack at time (t + 1) = Context Stack at time t

Python Class Definition (7)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = a class named name with bases: bases

then "if" map at time (t + 1) = "if" map at time t

Python Class Definition (8)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = a class named name with bases: bases

then 'while stack' at time (t + 1) = 'while stack' at time t

Python Class Definition (9)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = a class named name with bases: bases

then Python Object Store at time (t + 1) = Python Object Store at time t

Python Class Definition Ended (1)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab k = s
k < j
value at (j - 1) in map (Control Map at time t) = pair ("class", class_name)

then the line at time (t + 1) = the line at time t

Python Class Definition Ended (2)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab k = s
k < j
value at (j - 1) in map (Control Map at time t) = pair ("class", class_name)

then the tab at time (t + 1) = j - 1

Python Class Definition Ended (3)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab k = s
k < j
value at (j - 1) in map (Control Map at time t) = pair ("class", class_name)

then Expression Stack at time t = [ ]

Python Class Definition Ended (4)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab k = s
k < j
value at (j - 1) in map (Control Map at time t) = pair ("class", class_name)

then Control Map at time (t + 1) = Control Map at time t

Python Class Definition Ended (5)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab k = s
k < j
value at (j - 1) in map (Control Map at time t) = pair ("class", class_name)

then Variables Map at time (t + 1) = Variables Map at time t

Python Class Definition Ended (6)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab k = s
k < j
value at (j - 1) in map (Control Map at time t) = pair ("class", class_name)

then Context Stack at time (t + 1) = Context Stack at time t

Python Class Definition Ended (7)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab k = s
k < j
value at (j - 1) in map (Control Map at time t) = pair ("class", class_name)

then "if" map at time (t + 1) = "if" map at time t

Python Class Definition Ended (8)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab k = s
k < j
value at (j - 1) in map (Control Map at time t) = pair ("class", class_name)

then Expression Stack at time (t + 1) = Expression Stack at time t

Python Class Definition Ended (9)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab k = s
k < j
value at (j - 1) in map (Control Map at time t) = pair ("class", class_name)

then Python Object Store at time (t + 1) = Python Object Store at time t

Python Class Definition Ended (10)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab k = s
k < j
value at (j - 1) in map (Control Map at time t) = pair ("class", class_name)

then 'while stack' at time (t + 1) = 'while stack' at time t

Python Class Definition Ended (11)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab k = s
k < j
value at (j - 1) in map (Control Map at time t) = pair ("class", class_name)

then Class Map at time (t + 1) = Class Map at time t

Python Method Definition line and tab (1)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = a method named method_name with parameters params

then the line at time (t + 1) = i + 1

Python Method Definition line and tab (2)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = a method named method_name with parameters params

then the tab at time (t + 1) = j

Python Method Definition line and tab (3)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = a method named method_name with parameters params

then Variables Map at time (t + 1) = Variables Map at time t

Python Method Definition line and tab (4)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = a method named method_name with parameters params

then Context Stack at time (t + 1) = Context Stack at time t

Python Method Definition line and tab (5)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = a method named method_name with parameters params

then "if" map at time (t + 1) = "if" map at time t

Python Method Definition line and tab (6)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = a method named method_name with parameters params

then 'while stack' at time (t + 1) = 'while stack' at time t

Python Method Definition line and tab (7)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = a method named method_name with parameters params

then Python Object Store at time (t + 1) = Python Object Store at time t

Python Method Definition line and tab (8)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = a method named method_name with parameters params

then Control Map at time (t + 1) = Control Map at time t

New Python method definition

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = a method named method_name with parameters params
value at class_name in map (Class Map at time t) = class_map
value at "methods" in map class_map = methods_map

then Class Map at time (t + 1) = result of storing (result of storing (result of storing [ entry "params": params, [ entry "line": i, [ ] ] ] at key: method_name in map: methods_map) at key: "methods" in map: class_map) at key: class_name in map: (Class Map at time t)

Call Python Method Begin Set Params (1)

if the following are true:

Expression Stack at time t = [ [ ], [ [ obj_name.method_name(args), ys ], rest ] ]
value at obj_name in map (Variables Map at time t) = Python reference index
the element at index index of stack (Python Object Store at time t) = Python object: [ entry "__class_name__": class_name, e_rest ]
method parameters where the Class Map is (Class Map at time t), class name is class_name, and method name is method_name = params
Parameters List at time t = None
Value Stack at time t = [ values, v_stack ]

then Parameters List at time (t + 1) = params

Call Python Method Begin Set Params (2)

if the following are true:

Expression Stack at time t = [ [ ], [ [ obj_name.method_name(args), ys ], rest ] ]
value at obj_name in map (Variables Map at time t) = Python reference index
the element at index index of stack (Python Object Store at time t) = Python object: [ entry "__class_name__": class_name, e_rest ]
method parameters where the Class Map is (Class Map at time t), class name is class_name, and method name is method_name = params
Parameters List at time t = None
Value Stack at time t = [ values, v_stack ]

then Value Stack at time (t + 1) = v_stack

Call Python Method Begin Set Params (3)

if the following are true:

Expression Stack at time t = [ [ ], [ [ obj_name.method_name(args), ys ], rest ] ]
value at obj_name in map (Variables Map at time t) = Python reference index
the element at index index of stack (Python Object Store at time t) = Python object: [ entry "__class_name__": class_name, e_rest ]
method parameters where the Class Map is (Class Map at time t), class name is class_name, and method name is method_name = params
Parameters List at time t = None
Value Stack at time t = [ values, v_stack ]

then Function Variables Map at time (t + 1) = [ ]

Call Python Method Begin Set Params (4)

if the following are true:

Expression Stack at time t = [ [ ], [ [ obj_name.method_name(args), ys ], rest ] ]
value at obj_name in map (Variables Map at time t) = Python reference index
the element at index index of stack (Python Object Store at time t) = Python object: [ entry "__class_name__": class_name, e_rest ]
method parameters where the Class Map is (Class Map at time t), class name is class_name, and method name is method_name = params
Parameters List at time t = None
Value Stack at time t = [ values, v_stack ]

then Argument Values at time (t + 1) = [ Python reference index, reverse of values ]

Call Python Method Begin Set Params (5)

if the following are true:

Expression Stack at time t = [ [ ], [ [ obj_name.method_name(args), ys ], rest ] ]
value at obj_name in map (Variables Map at time t) = Python reference index
the element at index index of stack (Python Object Store at time t) = Python object: [ entry "__class_name__": class_name, e_rest ]
method parameters where the Class Map is (Class Map at time t), class name is class_name, and method name is method_name = params
Parameters List at time t = None
Value Stack at time t = [ values, v_stack ]

then Expression Stack at time (t + 1) = Expression Stack at time t

Call Python Method Begin Set Params (6)

if the following are true:

Expression Stack at time t = [ [ ], [ [ obj_name.method_name(args), ys ], rest ] ]
value at obj_name in map (Variables Map at time t) = Python reference index
the element at index index of stack (Python Object Store at time t) = Python object: [ entry "__class_name__": class_name, e_rest ]
method parameters where the Class Map is (Class Map at time t), class name is class_name, and method name is method_name = params
Parameters List at time t = None
Value Stack at time t = [ values, v_stack ]

then Variables Map at time (t + 1) = Variables Map at time t

Call Python Method Begin Set Params (7)

if the following are true:

Expression Stack at time t = [ [ ], [ [ obj_name.method_name(args), ys ], rest ] ]
value at obj_name in map (Variables Map at time t) = Python reference index
the element at index index of stack (Python Object Store at time t) = Python object: [ entry "__class_name__": class_name, e_rest ]
method parameters where the Class Map is (Class Map at time t), class name is class_name, and method name is method_name = params
Parameters List at time t = None
Value Stack at time t = [ values, v_stack ]

then Control Map at time (t + 1) = Control Map at time t

Call Python Method Begin Set Params (8)

if the following are true:

Expression Stack at time t = [ [ ], [ [ obj_name.method_name(args), ys ], rest ] ]
value at obj_name in map (Variables Map at time t) = Python reference index
the element at index index of stack (Python Object Store at time t) = Python object: [ entry "__class_name__": class_name, e_rest ]
method parameters where the Class Map is (Class Map at time t), class name is class_name, and method name is method_name = params
Parameters List at time t = None
Value Stack at time t = [ values, v_stack ]

then Python Object Store at time (t + 1) = Python Object Store at time t

Call Python Method Begin Set Params (9)

if the following are true:

Expression Stack at time t = [ [ ], [ [ obj_name.method_name(args), ys ], rest ] ]
value at obj_name in map (Variables Map at time t) = Python reference index
the element at index index of stack (Python Object Store at time t) = Python object: [ entry "__class_name__": class_name, e_rest ]
method parameters where the Class Map is (Class Map at time t), class name is class_name, and method name is method_name = params
Parameters List at time t = None
Value Stack at time t = [ values, v_stack ]

then Context Stack at time (t + 1) = Context Stack at time t

Call Python Method Begin Set Params (10)

if the following are true:

Expression Stack at time t = [ [ ], [ [ obj_name.method_name(args), ys ], rest ] ]
value at obj_name in map (Variables Map at time t) = Python reference index
the element at index index of stack (Python Object Store at time t) = Python object: [ entry "__class_name__": class_name, e_rest ]
method parameters where the Class Map is (Class Map at time t), class name is class_name, and method name is method_name = params
Parameters List at time t = None
Value Stack at time t = [ values, v_stack ]

then the line at time (t + 1) = the line at time t

Call Python Method Begin Set Params (11)

if the following are true:

Expression Stack at time t = [ [ ], [ [ obj_name.method_name(args), ys ], rest ] ]
value at obj_name in map (Variables Map at time t) = Python reference index
the element at index index of stack (Python Object Store at time t) = Python object: [ entry "__class_name__": class_name, e_rest ]
method parameters where the Class Map is (Class Map at time t), class name is class_name, and method name is method_name = params
Parameters List at time t = None
Value Stack at time t = [ values, v_stack ]

then the tab at time (t + 1) = the tab at time t

Call Python Method Line (1)

if the following are true:

Parameters List at time t = [ ]
Expression Stack at time t = [ [ ], [ [ obj_name.method_name(args), ys ], rest ] ]
value at obj_name in map (Variables Map at time t) = Python reference index
the element at index index of stack (Python Object Store at time t) = Python object: [ entry "__class_name__": class_name, e_rest ]
line number of method method_name of class class_name in (Class Map at time t) = line

then the line at time (t + 1) = line + 1

Call Python Method Line (2)

if the following are true:

Parameters List at time t = [ ]
Expression Stack at time t = [ [ ], [ [ obj_name.method_name(args), ys ], rest ] ]
value at obj_name in map (Variables Map at time t) = Python reference index
the element at index index of stack (Python Object Store at time t) = Python object: [ entry "__class_name__": class_name, e_rest ]
line number of method method_name of class class_name in (Class Map at time t) = line

then the tab at time (t + 1) = 2

Call Python Method Line (3)

if the following are true:

Parameters List at time t = [ ]
Expression Stack at time t = [ [ ], [ [ obj_name.method_name(args), ys ], rest ] ]
value at obj_name in map (Variables Map at time t) = Python reference index
the element at index index of stack (Python Object Store at time t) = Python object: [ entry "__class_name__": class_name, e_rest ]
line number of method method_name of class class_name in (Class Map at time t) = line

then Control Map at time (t + 1) = [ entry 0: (pair ("class", class_name)), [ entry 1: (pair ("method", method_name)), [ ] ] ]

Push Method Return Value (1)

if the following are true:

Return Value at time t = [ r, [ ] ]
Expression Stack at time t = [ [ ], [ [ name.method(args), ys ], rest ] ]
Value Stack at time t = [ next_level, other_levels ]

then Value Stack at time (t + 1) = [ [ r, next_level ], other_levels ]

Push Method Return Value (2)

if the following are true:

Return Value at time t = [ r, [ ] ]
Expression Stack at time t = [ [ ], [ [ name.method(args), ys ], rest ] ]
Value Stack at time t = [ next_level, other_levels ]

then Expression Stack at time (t + 1) = [ ys, rest ]

Push Method Return Value (3)

if the following are true:

Return Value at time t = [ r, [ ] ]
Expression Stack at time t = [ [ ], [ [ name.method(args), ys ], rest ] ]
Value Stack at time t = [ next_level, other_levels ]

then Return Value at time (t + 1) = [ ]

Push Method Return Value (4)

if the following are true:

Return Value at time t = [ r, [ ] ]
Expression Stack at time t = [ [ ], [ [ name.method(args), ys ], rest ] ]
Value Stack at time t = [ next_level, other_levels ]

then Parameters List at time (t + 1) = None

Push Method Return Value (5)

if the following are true:

Return Value at time t = [ r, [ ] ]
Expression Stack at time t = [ [ ], [ [ name.method(args), ys ], rest ] ]
Value Stack at time t = [ next_level, other_levels ]

then Variables Map at time (t + 1) = Variables Map at time t

Push Method Return Value (6)

if the following are true:

Return Value at time t = [ r, [ ] ]
Expression Stack at time t = [ [ ], [ [ name.method(args), ys ], rest ] ]
Value Stack at time t = [ next_level, other_levels ]

then Control Map at time (t + 1) = Control Map at time t

2 3 4