Conditional Properties

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

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

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

• 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 Value Stack at time (t + 1) = [ ]

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

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

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

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

• 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 = "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)

• 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 = "end_expr"

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

• 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 = "end_expr"

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

• 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 = "end_expr"

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

• 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 = "end_expr"

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

• 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 = "end_expr"

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

• expression state at time t = "begin_expr"
• the expression at time t = obj.attr

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

• expression state at time t = "begin_expr"
• the expression at time t = obj.attr

then parent stack at time (t + 1) = [ obj.attr, parent stack at time t ]

• expression state at time t = "begin_expr"
• the expression at time t = obj.attr

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

• expression state at time t = "begin_expr"
• the expression at time t = obj.attr

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

• expression state at time t = "call_function_begin"
• the expression at time t = obj.attr

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

• expression state at time t = "call_function_begin"
• the expression at time t = obj.attr
• Value Stack at time t = [ [ Python reference index, [ ] ], v_stack ]

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

• expression state at time t = "call_function_begin"
• the expression at time t = obj.attr
• Value Stack at time t = [ [ Python reference index, [ ] ], v_stack ]
• the element at index index of stack (Python Object Store at time t) = Python object: attributes

then Return Value at time (t + 1) = value at attr in map attributes

• expression state at time t = "call_function_begin"
• parent stack at time t = [ x, y ]
• the expression at time t = obj.attr

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

• expression state at time t = "call_function_begin"
• parent stack at time t = [ ]
• the expression at time t = obj.attr

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

• the line at time t = i
• the tab at time t = j
• statement at line i, tab j = obj.key = value
• expression state at time t = "not_expr"

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

• the line at time t = i
• the tab at time t = j
• statement at line i, tab j = obj.key = value
• expression state at time t = "not_expr"

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

• the line at time t = i
• the tab at time t = j
• statement at line i, tab j = obj.key = value
• expression state at time t = "not_expr"

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

• the line at time t = i
• the tab at time t = j
• statement at line i, tab j = obj.key = value
• expression state at time t = "not_expr"

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

• the line at time t = i
• the tab at time t = j
• statement at line i, tab j = obj.key = value
• expression state at time t = "not_expr"

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

• the line at time t = i
• the tab at time t = j
• statement at line i, tab j = obj.key = value
• expression state at time t = "not_expr"

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

• the line at time t = i
• the tab at time t = j
• statement at line i, tab j = obj.key = value
• expression state at time t = "not_expr"

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

• the line at time t = i
• the tab at time t = j
• statement at line i, tab j = obj.key = value
• expression state at time t = "not_expr"

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

• the line at time t = i
• the tab at time t = j
• statement at line i, tab j = obj.key = value
• expression state at time t = "not_expr"

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

• the line at time t = i
• the tab at time t = j
• statement at line i, tab j = obj.key = value

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

• the line at time t = i
• the tab at time t = j
• statement at line i, tab j = obj.key = value

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

• the line at time t = i
• the tab at time t = j
• statement at line i, tab j = obj.key = value

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

• the line at time t = i
• the tab at time t = j
• statement at line i, tab j = obj.key = value

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

• the line at time t = i
• the tab at time t = j
• statement at line i, tab j = obj.key = value

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

• expression state at time t = "begin_expr"
• the expression at time t = obj.key = value

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

• expression state at time t = "begin_expr"
• the expression at time t = obj.key = value

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

• expression state at time t = "begin_expr"
• the expression at time t = obj.key = value

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

• expression state at time t = "begin_expr"
• the expression at time t = obj.key = value

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

• expression state at time t = "call_function_begin"
• Value Stack at time t = [ [ value, [ Python reference idx, [ ] ] ], stack ]
• the expression at time t = obj.attribute = val
• the element at index idx of stack (Python Object Store at time t) = Python object: entries

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

• expression state at time t = "call_function_begin"
• Value Stack at time t = [ values, stack ]
• the expression at time t = x.y = z

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

• expression state at time t = "call_function_begin"
• parent stack at time t = [ ]
• the expression at time t = obj.attr = args

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

• the line at time t = i
• the tab at time t = j
• statement at line i, tab j = x.y = z
• expression state at time t = "end_expr"

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

• the line at time t = i
• the tab at time t = j
• statement at line i, tab j = x.y = z
• expression state at time t = "end_expr"

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

• the line at time t = i
• the tab at time t = j
• statement at line i, tab j = x.y = z
• expression state at time t = "end_expr"

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

• the line at time t = i
• the tab at time t = j
• statement at line i, tab j = x.y = z
• expression state at time t = "end_expr"

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

• the line at time t = i
• the tab at time t = j
• statement at line i, tab j = x.y = z
• expression state at time t = "end_expr"

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

• the line at time t = i
• the tab at time t = j
• statement at line i, tab j = x.y = z
• expression state at time t = "end_expr"

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

• the line at time t = i
• the tab at time t = j
• statement at line i, tab j = x.y = z
• expression state at time t = "end_expr"

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

• the line at time t = i
• the tab at time t = j
• statement at line i, tab j = x.y = z
• expression state at time t = "end_expr"

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

• the line at time t = i
• the tab at time t = j
• statement at line i, tab j = x.y = z
• expression state at time t = "end_expr"

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

• 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 ("method", method_name)

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

• 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 ("method", method_name)

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

• 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 ("method", method_name)

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

• 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 ("method", method_name)

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

• 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 ("method", mname)
• stack at time t = [ program context with variables: varis and expression state: (expression state with parent stack: parent_stack arguments: arg_stack values: value_stack line: line tab: tab) and control map: control_map, rest ]

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

• 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 ("method", mname)
• stack at time t = [ program context with variables: varis and expression state: (expression state with parent stack: parent_stack arguments: arg_stack values: value_stack line: line tab: tab) and control map: control_map, rest ]

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

• 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 ("method", mname)
• stack at time t = [ program context with variables: varis and expression state: (expression state with parent stack: parent_stack arguments: arg_stack values: value_stack line: line tab: tab) and control map: control_map, rest ]

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

• 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 ("method", mname)
• stack at time t = [ program context with variables: varis and expression state: (expression state with parent stack: parent_stack arguments: arg_stack values: value_stack line: line tab: tab) and control map: control_map, rest ]

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

• 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 ("method", mname)
• stack at time t = [ program context with variables: varis and expression state: (expression state with parent stack: parent_stack arguments: arg_stack values: value_stack line: line tab: tab) and control map: control_map, rest ]

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

• 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 ("method", mname)
• stack at time t = [ program context with variables: varis and expression state: (expression state with parent stack: parent_stack arguments: arg_stack values: value_stack line: line tab: tab) and control map: control_map, rest ]

then stack at time (t + 1) = rest

• 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 ("method", mname)
• stack at time t = [ program context with variables: varis and expression state: (expression state with parent stack: parent_stack arguments: arg_stack values: value_stack line: line tab: tab) and control map: control_map, rest ]

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

• 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 ("method", mname)
• stack at time t = [ program context with variables: varis and expression state: (expression state with parent stack: parent_stack arguments: arg_stack values: value_stack line: line tab: tab) and control map: control_map, rest ]

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

• 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 ("method", mname)
• stack at time t = [ program context with variables: varis and expression state: (expression state with parent stack: parent_stack arguments: arg_stack values: value_stack line: line tab: tab) and control map: control_map, rest ]

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

• 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 ("method", "__init__")

then Return Value at time (t + 1) = value at self in map (Variables Map at time t)

• 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 ("method", method_name)
• not (method_name = "__init__")

then Return Value at time (t + 1) = None

• value at j in map map_a = block
• not (the first token in block = "for")

then map map_a does not contain a for loop entry at line: i and tab: j

• value at j in map map_a = trio ("for", line, ex)
• not (line = i)

then map map_a does not contain a for loop entry at line: i and tab: j

• the line at time t = i
• the tab at time t = j
• statement at line i, tab j = for target in iterable:
• map (Control Map at time t) does not contain a for loop entry at line: i and tab: j
• expression state at time t = "not_expr"

then the expression at time (t + 1) = iterable

• the line at time t = i
• the tab at time t = j
• statement at line i, tab j = for target in iterable:
• map (Control Map at time t) does not contain a for loop entry at line: i and tab: j
• expression state at time t = "not_expr"

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

• the line at time t = i
• the tab at time t = j
• statement at line i, tab j = for target in iterable:
• map (Control Map at time t) does not contain a for loop entry at line: i and tab: j
• expression state at time t = "not_expr"

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

• the line at time t = i
• the tab at time t = j
• statement at line i, tab j = for target in iterable:
• map (Control Map at time t) does not contain a for loop entry at line: i and tab: j
• expression state at time t = "not_expr"

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

• the line at time t = i
• the tab at time t = j
• statement at line i, tab j = for target in iterable:
• map (Control Map at time t) does not contain a for loop entry at line: i and tab: j
• expression state at time t = "not_expr"

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

• the line at time t = i
• the tab at time t = j
• statement at line i, tab j = for target in iterable:
• map (Control Map at time t) does not contain a for loop entry at line: i and tab: j
• expression state at time t = "not_expr"

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

• the line at time t = i
• the tab at time t = j
• statement at line i, tab j = for target in iterable:
• map (Control Map at time t) does not contain a for loop entry at line: i and tab: j
• expression state at time t = "not_expr"

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

• the line at time t = i
• the tab at time t = j
• statement at line i, tab j = for target in iterable:
• map (Control Map at time t) does not contain a for loop entry at line: i and tab: j
• expression state at time t = "not_expr"

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

• the line at time t = i
• the tab at time t = j
• statement at line i, tab j = for target in iterable:
• map (Control Map at time t) does not contain a for loop entry at line: i and tab: j
• expression state at time t = "not_expr"

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

• the line at time t = i
• the tab at time t = j
• statement at line i, tab j = for target in iterable:
• map (Control Map at time t) does not contain a for loop entry at line: i and tab: j
• expression state at time t = "not_expr"

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

• the line at time t = i
• the tab at time t = j
• statement at line i, tab j = for target in iterable:
• map (Control Map at time t) does not contain a for loop entry at line: i and tab: j
• expression state at time t = "not_expr"

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

• the line at time t = i
• the tab at time t = j
• statement at line i, tab j = for target in iterable:
• iterable is a variable

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

• the line at time t = i
• the tab at time t = j
• statement at line i, tab j = for target in iterable:
• iterable is a variable

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

• the line at time t = i
• the tab at time t = j
• statement at line i, tab j = for target in iterable:
• iterable is a variable

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

• the line at time t = i
• the tab at time t = j
• statement at line i, tab j = for target in iterable:
• iterable is a variable

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

• the line at time t = i
• the tab at time t = j
• statement at line i, tab j = for target in iterable:
• expression state at time t = "end_expr"

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

• the line at time t = i
• the tab at time t = j
• statement at line i, tab j = for target in iterable:
• expression state at time t = "end_expr"

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

• the line at time t = i
• the tab at time t = j
• statement at line i, tab j = for target in iterable:
• expression state at time t = "end_expr"

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

• the line at time t = i
• the tab at time t = j
• statement at line i, tab j = for target in iterable:
• expression state at time t = "end_expr"

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

• the line at time t = i
• the tab at time t = j
• statement at line i, tab j = for target in iterable:
• expression state at time t = "end_expr"

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

• the line at time t = i
• the tab at time t = j
• statement at line i, tab j = for target in iterable:
• expression state at time t = "end_expr"

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

• the line at time t = i
• the tab at time t = j
• statement at line i, tab j = for target in iterable:
• expression state at time t = "end_expr"

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

• the line at time t = i
• the tab at time t = j
• statement at line i, tab j = for target in iterable:
• expression state at time t = "end_expr"

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

• the line at time t = i
• the tab at time t = j
• statement at line i, tab j = for target in iterable_ex:
• expression state at time t = "end_expr"
• Return Value at time t = Python reference index
• the element at index index of stack (Python Object Store at time t) = Python list elements

then Control Map at time (t + 1) = result of storing (trio ("for", i, elements)) at key: j in map: (Control Map at time t)

• the line at time t = i
• the tab at time t = j
• statement at line i, tab j = for target in iterable_ex:
• value at j in map (Control Map at time t) = trio ("for", i, [ elem, rest ])

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

• the line at time t = i
• the tab at time t = j
• statement at line i, tab j = for target in iterable_ex:
• value at j in map (Control Map at time t) = trio ("for", i, [ elem, rest ])

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

• the line at time t = i
• the tab at time t = j
• statement at line i, tab j = for target in iterable_ex:
• value at j in map (Control Map at time t) = trio ("for", i, [ elem, rest ])

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

• the line at time t = i
• the tab at time t = j
• statement at line i, tab j = for target in iterable_ex:
• value at j in map (Control Map at time t) = trio ("for", i, [ elem, rest ])

then Control Map at time (t + 1) = result of storing (trio ("for", i, rest)) at key: j in map: (Control Map at time t)

• the line at time t = i
• the tab at time t = j
• statement at line i, tab j = for target in iterable_ex:
• value at j in map (Control Map at time t) = trio ("for", i, [ elem, rest ])

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