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.

Push Method Return Value (7)

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 Python Object Store at time (t + 1) = Python Object Store at time t

Push Method Return Value (8)

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 Context Stack at time (t + 1) = Context Stack at time t

Push Method Return Value (9)

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 the line at time (t + 1) = the line at time t

Push Method Return Value (10)

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 the tab at time (t + 1) = the tab at time t

Python Method Call Ended (1)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = obj.mn(args)
Expression Stack at time t = [ [ ], [ ] ]

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

Python Method Call Ended (2)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = obj.mn(args)
Expression Stack at time t = [ [ ], [ ] ]

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

Python Method Call Ended (3)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = obj.mn(args)
Expression Stack at time t = [ [ ], [ ] ]

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

Python Method Call Ended (4)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = obj.mn(args)
Expression Stack at time t = [ [ ], [ ] ]

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

Python Method Call Ended (5)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = obj.mn(args)
Expression Stack at time t = [ [ ], [ ] ]

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

Python Method Call Ended (6)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = obj.mn(args)
Expression Stack at time t = [ [ ], [ ] ]

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

Python Method Call Ended (7)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = obj.mn(args)
Expression Stack at time t = [ [ ], [ ] ]

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

Assign Variable to Python Method Call Result (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 (obj_name.method_name(args))
Expression Stack at time t = [ [ ], [ ] ]
Value Stack at time t = [ [ value, [ ] ], [ ] ]

then Variables Map at time (t + 1) = result of storing value at key: x in map: (Variables Map at time t)

Assign Variable to Python Method Call Result (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 (obj_name.method_name(args))
Expression Stack at time t = [ [ ], [ ] ]
Value Stack at time t = [ [ value, [ ] ], [ ] ]

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

Assign Variable to Python Method Call Result (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 (obj_name.method_name(args))
Expression Stack at time t = [ [ ], [ ] ]
Value Stack at time t = [ [ value, [ ] ], [ ] ]

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

Assign Variable to Python Method Call Result (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 (obj_name.method_name(args))
Expression Stack at time t = [ [ ], [ ] ]
Value Stack at time t = [ [ value, [ ] ], [ ] ]

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

Assign Variable to Python Method Call Result (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 (obj_name.method_name(args))
Expression Stack at time t = [ [ ], [ ] ]
Value Stack at time t = [ [ value, [ ] ], [ ] ]

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

Assign Variable to Python Method Call Result (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 (obj_name.method_name(args))
Expression Stack at time t = [ [ ], [ ] ]
Value Stack at time t = [ [ value, [ ] ], [ ] ]

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

Assign Python Constructor (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 constructor with name: name and arguments: args)
Expression Stack at time t = [ ]

then Expression Stack at time (t + 1) = [ [ Python constructor with name: name and arguments: args, [ ] ], [ ] ]

Assign Python Constructor (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 constructor with name: name and arguments: args)
Expression Stack at time t = [ ]

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

Assign Python Constructor (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 constructor with name: name and arguments: args)
Expression Stack at time t = [ ]

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

Assign Python Constructor (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 constructor with name: name and arguments: args)
Expression Stack at time t = [ ]

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

Assign Python Constructor (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 constructor with name: name and arguments: args)
Expression Stack at time t = [ ]

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

Assign Python Constructor (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 constructor with name: name and arguments: args)
Expression Stack at time t = [ ]

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

Assign Python Constructor (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 constructor with name: name and arguments: args)
Expression Stack at time t = [ ]

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

Assign Python Constructor (8)

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 constructor with name: name and arguments: args)
Expression Stack at time t = [ ]

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

Begin Python Constructor Elements (1)

if Expression Stack at time t = [ [ Python constructor with name: class_name and arguments: args, ys ], rest ], then Value Stack at time (t + 1) = [ [ ], Value Stack at time t ]

Begin Python Constructor Elements (2)

if Expression Stack at time t = [ [ Python constructor with name: class_name and arguments: args, ys ], rest ], then Expression Stack at time (t + 1) = [ args, [ [ Python constructor with name: class_name and arguments: args, ys ], rest ] ]

Begin Python Constructor Elements (3)

if Expression Stack at time t = [ [ Python constructor with name: class_name and arguments: args, ys ], rest ], then Parameters List at time (t + 1) = None

Begin Python Constructor Elements (4)

if Expression Stack at time t = [ [ Python constructor with name: class_name and arguments: args, ys ], rest ], then the line at time (t + 1) = the line at time t

Begin Python Constructor Elements (5)

if Expression Stack at time t = [ [ Python constructor with name: class_name and arguments: args, ys ], rest ], then the tab at time (t + 1) = the tab at time t

Begin Python Constructor Elements (6)

if Expression Stack at time t = [ [ Python constructor with name: class_name and arguments: args, ys ], rest ], then Variables Map at time (t + 1) = Variables Map at time t

Begin Python Constructor Elements (7)

if Expression Stack at time t = [ [ Python constructor with name: class_name and arguments: args, ys ], rest ], then Control Map at time (t + 1) = Control Map at time t

Begin Python Constructor Elements (8)

if Expression Stack at time t = [ [ Python constructor with name: class_name and arguments: args, ys ], rest ], then Python Object Store at time (t + 1) = Python Object Store at time t

Begin Python Constructor Elements (9)

if Expression Stack at time t = [ [ Python constructor with name: class_name and arguments: args, ys ], rest ], then Context Stack at time (t + 1) = Context Stack at time t

Call Python constructor method begin (1)

if the following are true:

Expression Stack at time t = [ [ ], [ [ Python constructor with name: class_name and arguments: args, ys ], rest ] ]
Value Stack at time t = [ evaluated, stack ]
method parameters where the Class Map is (Class Map at time t), class name is class_name, and method name is "__init__" = params
Parameters List at time t = None

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

Call Python constructor method begin (2)

if the following are true:

Expression Stack at time t = [ [ ], [ [ Python constructor with name: class_name and arguments: args, ys ], rest ] ]
Value Stack at time t = [ evaluated, stack ]
method parameters where the Class Map is (Class Map at time t), class name is class_name, and method name is "__init__" = params
Parameters List at time t = None

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

Call Python constructor method begin (3)

if the following are true:

Expression Stack at time t = [ [ ], [ [ Python constructor with name: class_name and arguments: args, ys ], rest ] ]
Value Stack at time t = [ evaluated, stack ]
method parameters where the Class Map is (Class Map at time t), class name is class_name, and method name is "__init__" = params
Parameters List at time t = None

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

Call Python constructor method begin (4)

if the following are true:

Expression Stack at time t = [ [ ], [ [ Python constructor with name: class_name and arguments: args, ys ], rest ] ]
Value Stack at time t = [ evaluated, stack ]
method parameters where the Class Map is (Class Map at time t), class name is class_name, and method name is "__init__" = params
Parameters List at time t = None

then Argument Values at time (t + 1) = reverse of evaluated

Call Python constructor method begin (5)

if the following are true:

Expression Stack at time t = [ [ ], [ [ Python constructor with name: class_name and arguments: args, ys ], rest ] ]
Value Stack at time t = [ evaluated, stack ]
method parameters where the Class Map is (Class Map at time t), class name is class_name, and method name is "__init__" = params
Parameters List at time t = None

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

Call Python constructor method begin (6)

if the following are true:

Expression Stack at time t = [ [ ], [ [ Python constructor with name: class_name and arguments: args, ys ], rest ] ]
Value Stack at time t = [ evaluated, stack ]
method parameters where the Class Map is (Class Map at time t), class name is class_name, and method name is "__init__" = params
Parameters List at time t = None

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

Call Python constructor method begin (7)

if the following are true:

Expression Stack at time t = [ [ ], [ [ Python constructor with name: class_name and arguments: args, ys ], rest ] ]
Value Stack at time t = [ evaluated, stack ]
method parameters where the Class Map is (Class Map at time t), class name is class_name, and method name is "__init__" = params
Parameters List at time t = None

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

Call Python constructor method begin (8)

if the following are true:

Expression Stack at time t = [ [ ], [ [ Python constructor with name: class_name and arguments: args, ys ], rest ] ]
Value Stack at time t = [ evaluated, stack ]
method parameters where the Class Map is (Class Map at time t), class name is class_name, and method name is "__init__" = params
Parameters List at time t = None

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

Call Python constructor method begin (9)

if the following are true:

Expression Stack at time t = [ [ ], [ [ Python constructor with name: class_name and arguments: args, ys ], rest ] ]
Value Stack at time t = [ evaluated, stack ]
method parameters where the Class Map is (Class Map at time t), class name is class_name, and method name is "__init__" = params
Parameters List at time t = None

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

Call Python constructor method begin (10)

if the following are true:

Expression Stack at time t = [ [ ], [ [ Python constructor with name: class_name and arguments: args, ys ], rest ] ]
Value Stack at time t = [ evaluated, stack ]
method parameters where the Class Map is (Class Map at time t), class name is class_name, and method name is "__init__" = params
Parameters List at time t = None

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

Call Python constructor method begin (11)

if the following are true:

Expression Stack at time t = [ [ ], [ [ Python constructor with name: class_name and arguments: args, ys ], rest ] ]
Value Stack at time t = [ evaluated, stack ]
method parameters where the Class Map is (Class Map at time t), class name is class_name, and method name is "__init__" = params
Parameters List at time t = None

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

Call Python Build Args Constructor (1)

if the following are true:

Expression Stack at time t = [ [ ], [ [ Python constructor with name: class_name and arguments: args, ys ], rest ] ]
Function Variables Map at time t = [ ]
Parameters List at time t = [ self, p_rest ]

then Function Variables Map at time (t + 1) = [ entry self: (Python reference (length of stack (Python Object Store at time t))), [ ] ]

Call Python Build Args Constructor (2)

if the following are true:

Expression Stack at time t = [ [ ], [ [ Python constructor with name: class_name and arguments: args, ys ], rest ] ]
Function Variables Map at time t = [ ]
Parameters List at time t = [ self, p_rest ]

then Python Object Store at time (t + 1) = result of appending (Python object: [ entry "__class_name__": class_name, [ ] ]) to (Python Object Store at time t)

Call Python Build Args Constructor (3)

if the following are true:

Expression Stack at time t = [ [ ], [ [ Python constructor with name: class_name and arguments: args, ys ], rest ] ]
Function Variables Map at time t = [ ]
Parameters List at time t = [ self, p_rest ]

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

Call Python Build Args Constructor (4)

if the following are true:

Expression Stack at time t = [ [ ], [ [ Python constructor with name: class_name and arguments: args, ys ], rest ] ]
Function Variables Map at time t = [ ]
Parameters List at time t = [ self, p_rest ]

then Argument Values at time (t + 1) = Argument Values at time t

Jump To Constructor (1)

if the following are true:

Parameters List at time t = [ ]
Expression Stack at time t = [ [ ], [ [ Python constructor with name: class_name and arguments: args, ys ], rest ] ]
line number of method "__init__" of class class_name in (Class Map at time t) = line

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

Jump To Constructor (2)

if the following are true:

Parameters List at time t = [ ]
Expression Stack at time t = [ [ ], [ [ Python constructor with name: class_name and arguments: args, ys ], rest ] ]
line number of method "__init__" of class class_name in (Class Map at time t) = line

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

Jump To Constructor (3)

if the following are true:

Parameters List at time t = [ ]
Expression Stack at time t = [ [ ], [ [ Python constructor with name: class_name and arguments: args, ys ], rest ] ]
line number of method "__init__" 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", "__init__")), [ ] ] ]

Push Return Value (1)

if the following are true:

Return Value at time t = [ r, [ ] ]
Expression Stack at time t = [ [ ], [ [ Python constructor with name: clss_name and arguments: 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 Return Value (2)

if the following are true:

Return Value at time t = [ r, [ ] ]
Expression Stack at time t = [ [ ], [ [ Python constructor with name: clss_name and arguments: args, ys ], rest ] ]
Value Stack at time t = [ next_level, other_levels ]

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

Push Return Value (3)

if the following are true:

Return Value at time t = [ r, [ ] ]
Expression Stack at time t = [ [ ], [ [ Python constructor with name: clss_name and arguments: args, ys ], rest ] ]
Value Stack at time t = [ next_level, other_levels ]

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

Push Return Value (4)

if the following are true:

Return Value at time t = [ r, [ ] ]
Expression Stack at time t = [ [ ], [ [ Python constructor with name: clss_name and arguments: args, ys ], rest ] ]
Value Stack at time t = [ next_level, other_levels ]

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

Push Return Value (5)

if the following are true:

Return Value at time t = [ r, [ ] ]
Expression Stack at time t = [ [ ], [ [ Python constructor with name: clss_name and arguments: 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 Return Value (6)

if the following are true:

Return Value at time t = [ r, [ ] ]
Expression Stack at time t = [ [ ], [ [ Python constructor with name: clss_name and arguments: args, ys ], rest ] ]
Value Stack at time t = [ next_level, other_levels ]

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

Push Return Value (7)

if the following are true:

Return Value at time t = [ r, [ ] ]
Expression Stack at time t = [ [ ], [ [ Python constructor with name: clss_name and arguments: args, ys ], rest ] ]
Value Stack at time t = [ next_level, other_levels ]

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

Push Return Value (8)

if the following are true:

Return Value at time t = [ r, [ ] ]
Expression Stack at time t = [ [ ], [ [ Python constructor with name: clss_name and arguments: args, ys ], rest ] ]
Value Stack at time t = [ next_level, other_levels ]

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

Push Return Value (9)

if the following are true:

Return Value at time t = [ r, [ ] ]
Expression Stack at time t = [ [ ], [ [ Python constructor with name: clss_name and arguments: args, ys ], rest ] ]
Value Stack at time t = [ next_level, other_levels ]

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

Push Return Value (10)

if the following are true:

Return Value at time t = [ r, [ ] ]
Expression Stack at time t = [ [ ], [ [ Python constructor with name: clss_name and arguments: args, ys ], rest ] ]
Value Stack at time t = [ next_level, other_levels ]

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

Assign Variable to Python Constructor Result (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 constructor with name: class_name and arguments: args)
Expression Stack at time t = [ [ ], [ ] ]
Value Stack at time t = [ [ value, [ ] ], [ ] ]

then Variables Map at time (t + 1) = result of storing value at key: x in map: (Variables Map at time t)

Assign Variable to Python Constructor Result (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 constructor with name: class_name and arguments: args)
Expression Stack at time t = [ [ ], [ ] ]
Value Stack at time t = [ [ value, [ ] ], [ ] ]

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

Assign Variable to Python Constructor Result (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 constructor with name: class_name and arguments: args)
Expression Stack at time t = [ [ ], [ ] ]
Value Stack at time t = [ [ value, [ ] ], [ ] ]

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

Assign Variable to Python Constructor Result (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 constructor with name: class_name and arguments: args)
Expression Stack at time t = [ [ ], [ ] ]
Value Stack at time t = [ [ value, [ ] ], [ ] ]

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

Assign Variable to Python Constructor Result (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 constructor with name: class_name and arguments: args)
Expression Stack at time t = [ [ ], [ ] ]
Value Stack at time t = [ [ value, [ ] ], [ ] ]

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

Assign Variable to Python Constructor Result (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 constructor with name: class_name and arguments: args)
Expression Stack at time t = [ [ ], [ ] ]
Value Stack at time t = [ [ value, [ ] ], [ ] ]

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

Assign Python Get Attribute (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 (obj.attr)
Expression Stack at time t = [ ]

then Expression Stack at time (t + 1) = [ [ obj.attr, [ ] ], [ ] ]

Assign Python Get Attribute (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 (obj.attr)
Expression Stack at time t = [ ]

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

Assign Python Get Attribute (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 (obj.attr)
Expression Stack at time t = [ ]

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

Assign Python Get Attribute (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 (obj.attr)
Expression Stack at time t = [ ]

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

Assign Python Get Attribute (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 (obj.attr)
Expression Stack at time t = [ ]

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

Assign Python Get Attribute (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 (obj.attr)
Expression Stack at time t = [ ]

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

Assign Python Get Attribute (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 (obj.attr)
Expression Stack at time t = [ ]

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

Assign Python Get Attribute (8)

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 (obj.attr)
Expression Stack at time t = [ ]

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

Assign Variable to Python Get Attribute Result (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 (obj.attr)
Expression Stack at time t = [ [ ], [ ] ]
Value Stack at time t = [ [ value, [ ] ], [ ] ]

then Variables Map at time (t + 1) = result of storing value at key: x in map: (Variables Map at time t)

Assign Variable to Python Get Attribute Result (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 (obj.attr)
Expression Stack at time t = [ [ ], [ ] ]
Value Stack at time t = [ [ value, [ ] ], [ ] ]

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

Assign Variable to Python Get Attribute Result (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 (obj.attr)
Expression Stack at time t = [ [ ], [ ] ]
Value Stack at time t = [ [ value, [ ] ], [ ] ]

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

Assign Variable to Python Get Attribute Result (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 (obj.attr)
Expression Stack at time t = [ [ ], [ ] ]
Value Stack at time t = [ [ value, [ ] ], [ ] ]

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

Assign Variable to Python Get Attribute Result (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 (obj.attr)
Expression Stack at time t = [ [ ], [ ] ]
Value Stack at time t = [ [ value, [ ] ], [ ] ]

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

Assign Variable to Python Get Attribute Result (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 (obj.attr)
Expression Stack at time t = [ [ ], [ ] ]
Value Stack at time t = [ [ value, [ ] ], [ ] ]

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

Begin Python Get Attribute (1)

if Expression Stack at time t = [ [ obj.attr, ys ], rest ], then Value Stack at time (t + 1) = [ [ ], Value Stack at time t ]

Begin Python Get Attribute (2)

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

Begin Python Get Attribute (3)

if Expression Stack at time t = [ [ obj.attr, ys ], rest ], then Parameters List at time (t + 1) = None

Begin Python Get Attribute (4)

if Expression Stack at time t = [ [ obj.attr, ys ], rest ], then the line at time (t + 1) = the line at time t

Begin Python Get Attribute (5)

if Expression Stack at time t = [ [ obj.attr, ys ], rest ], then the tab at time (t + 1) = the tab at time t

Begin Python Get Attribute (6)

if Expression Stack at time t = [ [ obj.attr, ys ], rest ], then Variables Map at time (t + 1) = Variables Map at time t

Begin Python Get Attribute (7)

if Expression Stack at time t = [ [ obj.attr, ys ], rest ], then Control Map at time (t + 1) = Control Map at time t

Begin Python Get Attribute (8)

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

Begin Python Get Attribute (9)

if Expression Stack at time t = [ [ obj.attr, ys ], rest ], then Context Stack at time (t + 1) = Context Stack at time t

Python Get Attribute Return Value

if the following are true:

Expression Stack at time t = [ [ ], [ [ obj.attr, ys ], rest ] ]
Value Stack at time t = [ [ Python reference index, [ ] ], [ next_level, other_levels ] ]
the element at index index of stack (Python Object Store at time t) = Python object: attributes

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

On Python Get Attribute (1)

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

On Python Get Attribute (2)

if Expression Stack at time t = [ [ ], [ [ obj.attr, ys ], rest ] ], then the line at time (t + 1) = the line at time t

On Python Get Attribute (3)

if Expression Stack at time t = [ [ ], [ [ obj.attr, ys ], rest ] ], then the tab at time (t + 1) = the tab at time t

On Python Get Attribute (4)

if Expression Stack at time t = [ [ ], [ [ obj.attr, ys ], rest ] ], then Variables Map at time (t + 1) = Variables Map at time t

On Python Get Attribute (5)

if Expression Stack at time t = [ [ ], [ [ obj.attr, ys ], rest ] ], then Control Map at time (t + 1) = Control Map at time t

On Python Get Attribute (6)

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

On Python Get Attribute (7)

if Expression Stack at time t = [ [ ], [ [ obj.attr, ys ], rest ] ], then Context Stack at time (t + 1) = Context Stack at time t

Begin Python Set Attribute (1)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = obj.key = value
Expression Stack at time t = [ ]

then Expression Stack at time (t + 1) = [ [ obj.key = value, [ ] ], [ ] ]

3 4 5