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.

Assign Dict (10)

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 state at time t = "not_expr"

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

Assign Variable to Dict 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 dictionary elements)
expression state at time t = "end_expr"

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

Assign Variable to Dict 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 dictionary elements)
expression state at time t = "end_expr"

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

Assign Variable to Dict 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 dictionary elements)
expression state at time t = "end_expr"

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

Assign Variable to Dict 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 dictionary elements)
expression state at time t = "end_expr"

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

Assign Variable to Dict 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 dictionary elements)
expression state at time t = "end_expr"

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

Get Dictionary Item

if the following are true:

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

then Return Value at time (t + 1) = value at a in map entries

Set Entry (1)

if the following are true:

expression state at time t = "call_function_begin"
Value Stack at time t = [ [ value, [ key, [ Python reference idx, [ ] ] ] ], stack ]
the expression at time t = function call with name: "__setitem__" and arguments: [ obj, rest ]
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 Entry (2)

if the following are true:

expression state at time t = "call_function_begin"
Value Stack at time t = [ [ value, [ key, [ Python reference idx, [ ] ] ] ], stack ]
the expression at time t = function call with name: "__setitem__" and arguments: [ obj, rest ]
the element at index idx of stack (Python Object Store at time t) = Python dictionary entries

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

Set Item (1)

if the following are true:

expression state at time t = "call_function_begin"
Value Stack at time t = [ [ value, [ key, [ Python reference idx, [ ] ] ] ], stack ]
the expression at time t = function call with name: "__setitem__" and arguments: [ obj, rest ]
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 (2)

if the following are true:

expression state at time t = "call_function_begin"
Value Stack at time t = [ [ value, [ key, [ Python reference idx, [ ] ] ] ], stack ]
the expression at time t = function call with name: "__setitem__" and arguments: [ obj, rest ]
the element at index idx of stack (Python Object Store at time t) = Python list elements

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

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 state at time t = "not_expr"

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

Set Item Return

if the following are true:

expression state at time t = "call_function_begin"
parent stack at time t = [ x, y ]
the expression at time t = function call with name: "__setitem__" and arguments: args

then expression state at time (t + 1) = "return"

Set Item End

if the following are true:

expression state at time t = "call_function_begin"
parent stack at time t = [ ]
the expression at time t = function call with name: "__setitem__" and arguments: args

then expression state at time (t + 1) = "end_expr"

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)

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)

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

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

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

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

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

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

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

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

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

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 state at time t = "not_expr"

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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 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 Method Line (1)

if the following are true:

expression state at time t = "call_build_args"
Parameters List at time t = [ ]
the expression at time t = obj_name.method_name(args)
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 Method Line (2)

if the following are true:

expression state at time t = "call_build_args"
Parameters List at time t = [ ]
the expression at time t = obj_name.method_name(args)
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 Method Line (3)

if the following are true:

expression state at time t = "call_build_args"
Parameters List at time t = [ ]
the expression at time t = obj_name.method_name(args)
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)), [ ] ] ]

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 state at time t = "end_expr"

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

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 state at time t = "end_expr"

then expression state at time (t + 1) = "not_expr"

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 state at time t = "end_expr"

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

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 state at time t = "end_expr"

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

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 state at time t = "end_expr"

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

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 state at time t = "end_expr"

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

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 state at time t = "end_expr"

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

Method Call Ended (8)

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 state at time t = "end_expr"

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

Assign Variable to 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 state at time t = "end_expr"

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

Assign Variable to 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 state at time t = "end_expr"

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

Assign Variable to 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 state at time t = "end_expr"

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

Assign Variable to 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 state at time t = "end_expr"

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

Assign Variable to 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 state at time t = "end_expr"

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

Assign Variable to 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 state at time t = "end_expr"

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

Assign 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 state at time t = "not_expr"

then the expression at time (t + 1) = Python constructor with name: name and arguments: args

Assign 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 state at time t = "not_expr"

then expression state at time (t + 1) = "begin_expr"

Assign 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 state at time t = "not_expr"

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

Assign 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 state at time t = "not_expr"

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

Assign 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 state at time t = "not_expr"

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

Assign 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 state at time t = "not_expr"

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

Assign 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 state at time t = "not_expr"

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

Assign 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 state at time t = "not_expr"

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

Assign Constructor (9)

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 state at time t = "not_expr"

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

Assign Constructor (10)

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 state at time t = "not_expr"

then parent stack at time (t + 1) = [ ]

Assign Constructor (11)

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 state at time t = "not_expr"

then arguments stack at time (t + 1) = [ ]

Begin Constructor Elements (1)

if the following are true:

expression state at time t = "begin_expr"
the expression at time t = Python constructor with name: class_name and arguments: args

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

Begin Constructor Elements (2)

if the following are true:

expression state at time t = "begin_expr"
the expression at time t = Python constructor with name: class_name and arguments: args

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

Begin Constructor Elements (3)

if the following are true:

expression state at time t = "begin_expr"
the expression at time t = Python constructor with name: class_name and arguments: args

then arguments stack at time (t + 1) = [ args, arguments stack at time t ]

Begin Constructor Elements (4)

if the following are true:

expression state at time t = "begin_expr"
the expression at time t = Python constructor with name: class_name and arguments: args

then expression state at time (t + 1) = "iterate_args"

Unchanged on constructor function begin

if the following are true:

expression state at time t = "call_function_begin"
the expression at time t = Python constructor with name: class_name and arguments: args

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

Call constructor method begin (1)

if the following are true:

expression state at time t = "call_function_begin"
Value Stack at time t = [ evaluated, stack ]
the expression at time t = Python constructor with name: class_name and arguments: args

then expression state at time (t + 1) = "call_build_args"

Call constructor method begin (2)

if the following are true:

expression state at time t = "call_function_begin"
Value Stack at time t = [ evaluated, stack ]
the expression at time t = Python constructor with name: class_name and arguments: args

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

Call constructor method begin (3)

if the following are true:

expression state at time t = "call_function_begin"
Value Stack at time t = [ evaluated, stack ]
the expression at time t = Python constructor with name: class_name and arguments: args

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

Call init Method Begin Set Params

if the following are true:

expression state at time t = "call_function_begin"
the expression at time t = Python constructor with name: class_name and arguments: args
method parameters where the Class Map is (Class Map at time t), class name is class_name, and method name is "__init__" = params

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

Call Build Args Constructor (1)

if the following are true:

expression state at time t = "call_build_args"
the expression at time t = Python constructor with name: class_name and arguments: args
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 Build Args Constructor (2)

if the following are true:

expression state at time t = "call_build_args"
the expression at time t = Python constructor with name: class_name and arguments: args
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 Build Args Constructor (3)

if the following are true:

expression state at time t = "call_build_args"
the expression at time t = Python constructor with name: class_name and arguments: args
Function Variables Map at time t = [ ]
Parameters List at time t = [ self, p_rest ]

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

Call Build Args Constructor (4)

if the following are true:

expression state at time t = "call_build_args"
the expression at time t = Python constructor with name: class_name and arguments: args
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

Call Build Args Constructor (5)

if the following are true:

expression state at time t = "call_build_args"
the expression at time t = Python constructor with name: class_name and arguments: args
Function Variables Map at time t = [ ]
Parameters List at time t = [ self, p_rest ]

then expression state at time (t + 1) = "call_build_args"

Call Build Args Constructor (6)

if the following are true:

expression state at time t = "call_build_args"
the expression at time t = Python constructor with name: class_name and arguments: args
Function Variables Map at time t = [ ]
Parameters List at time t = [ self, p_rest ]

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

Call Build Args Constructor (7)

if the following are true:

expression state at time t = "call_build_args"
the expression at time t = Python constructor with name: class_name and arguments: args
Function Variables Map at time t = [ ]
Parameters List at time t = [ self, p_rest ]

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

Call Build Args Constructor (8)

if the following are true:

expression state at time t = "call_build_args"
the expression at time t = Python constructor with name: class_name and arguments: args
Function Variables Map at time t = [ ]
Parameters List at time t = [ self, p_rest ]

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

Call Constructor Line (1)

if the following are true:

expression state at time t = "call_build_args"
Parameters List at time t = [ ]
the expression at time t = Python constructor with name: class_name and arguments: args
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

Call Constructor Line (2)

if the following are true:

expression state at time t = "call_build_args"
Parameters List at time t = [ ]
the expression at time t = Python constructor with name: class_name and arguments: args
line number of method "__init__" of class class_name in (Class Map at time t) = line

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

Call Constructor Line (3)

if the following are true:

expression state at time t = "call_build_args"
Parameters List at time t = [ ]
the expression at time t = Python constructor with name: class_name and arguments: args
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__")), [ ] ] ]

Assign Variable to 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 state at time t = "end_expr"

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

Assign Variable to 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 state at time t = "end_expr"

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

Assign Variable to 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 state at time t = "end_expr"

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

Assign Variable to 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 state at time t = "end_expr"

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

Assign Variable to 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 state at time t = "end_expr"

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

Assign Variable to 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 state at time t = "end_expr"

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

Assign 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 state at time t = "not_expr"

then the expression at time (t + 1) = obj.attr

Assign 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 state at time t = "not_expr"

then expression state at time (t + 1) = "begin_expr"

Assign 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 state at time t = "not_expr"

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

11 12 13