Conditional Properties

• 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 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 Stack at time t = [ ]

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 Stack at time t = [ ]

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 Stack at time t = [ ]

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 Stack at time t = [ ]

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
• Expression Stack at time t = [ ]

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
• Expression Stack at time t = [ ]

then Context Stack at time (t + 1) = Context 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 Stack at time t = [ [ ], [ [ obj.attribute = val, ys ], rest ] ]
• Value Stack at time t = [ [ value, [ Python reference idx, [ ] ] ], [ next_level, other_levels ] ]
• 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 Stack at time t = [ [ ], [ [ obj.attribute = val, ys ], rest ] ]
• Value Stack at time t = [ [ value, [ Python reference idx, [ ] ] ], [ next_level, other_levels ] ]
• the element at index idx of stack (Python Object Store at time t) = Python object: entries

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

• the line at time t = i
• the tab at time t = j
• statement at line i, tab j = x.y = z
• Expression Stack at time t = [ [ ], [ ] ]

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 Stack at time t = [ [ ], [ ] ]

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 Stack at time t = [ [ ], [ ] ]

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

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 Stack at time t = [ [ ], [ ] ]

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 Stack at time t = [ [ ], [ ] ]

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 Stack at time t = [ [ ], [ ] ]

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 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)
• Context Stack at time t = [ program context with variables: varis and expression state: (expression state with expression stack: expr_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)
• Context Stack at time t = [ program context with variables: varis and expression state: (expression state with expression stack: expr_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)
• Context Stack at time t = [ program context with variables: varis and expression state: (expression state with expression stack: expr_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)
• Context Stack at time t = [ program context with variables: varis and expression state: (expression state with expression stack: expr_stack values: value_stack line: line tab: tab) and control map: control_map, rest ]

then Expression Stack at time (t + 1) = expr_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)
• Context Stack at time t = [ program context with variables: varis and expression state: (expression state with expression stack: expr_stack values: value_stack line: line tab: tab) and control map: control_map, rest ]

then Context 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)
• Context Stack at time t = [ program context with variables: varis and expression state: (expression state with expression stack: expr_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)
• Context Stack at time t = [ program context with variables: varis and expression state: (expression state with expression stack: expr_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, [ ] ]

• 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 Stack at time t = [ ]

then Expression Stack 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 Stack at time t = [ ]

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 Stack at time t = [ ]

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 Stack at time t = [ ]

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 Stack at time t = [ ]

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 Stack at time t = [ ]

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 Stack at time t = [ ]

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:
• iterable is a variable

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

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 Stack at time t = [ [ ], [ ] ]

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 Stack at time t = [ [ ], [ ] ]

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 Stack at time t = [ [ ], [ ] ]

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 Stack at time t = [ [ ], [ ] ]

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 Stack at time t = [ [ ], [ ] ]

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 Stack at time t = [ [ ], [ ] ]

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

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_ex:
• Expression Stack at time t = [ [ ], [ ] ]
• Value Stack at time t = [ [ Python reference index, [ ] ], v_stack ]
• 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 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_ex:
• value at j in map (Control Map at time t) = trio ("for", i, [ elem, rest ])

then Context Stack at time (t + 1) = Context 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_ex:
• value at j in map (Control Map at time t) = trio ("for", i, [ elem, rest ])

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_ex:
• value at j in map (Control Map at time t) = trio ("for", i, [ ])

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, [ ])

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_ex:
• value at j in map (Control Map at time t) = trio ("for", i, [ ])

then Control Map at time (t + 1) = result of deleting the entry with key j from 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, [ ])

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_ex:
• value at j in map (Control Map at time t) = trio ("for", i, [ ])

then Expression 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_ex:
• value at j in map (Control Map at time t) = trio ("for", i, [ ])

then Context Stack at time (t + 1) = Context 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_ex:
• value at j in map (Control Map at time t) = trio ("for", i, [ ])

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) = trio ("for", for_line, iterable)

then the line at time (t + 1) = for_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) = trio ("for", for_line, iterable)

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 k = s
• k < j
• value at (j - 1) in map (Control Map at time t) = trio ("for", for_line, iterable)

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 k = s
• k < j
• value at (j - 1) in map (Control Map at time t) = trio ("for", for_line, iterable)

then Context Stack at time (t + 1) = Context 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) = trio ("for", for_line, iterable)

then Expression Stack at time (t + 1) = Expression 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) = trio ("for", for_line, iterable)

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) = trio ("for", for_line, iterable)

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 k = s
• k < j
• value at (j - 1) in map (Control Map at time t) = trio ("for", for_line, iterable)

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

• the line at time t = i
• the tab at time t = j
• number of lines = i - 1
• value at (j - 1) in map (Control Map at time t) = trio ("for", for_line, iterable)

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

• the line at time t = i
• the tab at time t = j
• number of lines = i - 1
• value at (j - 1) in map (Control Map at time t) = trio ("for", for_line, iterable)

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

• the line at time t = i
• the tab at time t = j
• number of lines = i - 1
• value at (j - 1) in map (Control Map at time t) = trio ("for", for_line, iterable)

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

• the line at time t = i
• the tab at time t = j
• number of lines = i - 1
• value at (j - 1) in map (Control Map at time t) = trio ("for", for_line, iterable)

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

• the line at time t = i
• the tab at time t = j
• number of lines = i - 1
• value at (j - 1) in map (Control Map at time t) = trio ("for", for_line, iterable)

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

• the line at time t = i
• the tab at time t = j
• number of lines = i - 1
• value at (j - 1) in map (Control Map at time t) = trio ("for", for_line, iterable)

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

• the line at time t = i
• the tab at time t = j
• number of lines = i - 1
• value at (j - 1) in map (Control Map at time t) = trio ("for", for_line, iterable)

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
• number of lines = i - 1
• value at (j - 1) in map (Control Map at time t) = trio ("for", for_line, iterable)

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

• the line at time t = i
• the tab at time t = j
• number of lines = i - 1
• value at (j - 1) in map (Control Map at time t) = trio ("for", for_line, iterable)

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

• the line at time t = i
• the tab at time t = j
• number of lines = i - 1
• value at (j - 1) in map (Control Map at time t) = trio ("for", for_line, iterable)

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

• value at class_name in map class_defs = class_def
• value at "methods" in map class_def = methods
• value at method_name in map methods = method_map

then definition of method method_name of class class_name in class_defs = method_map

• the line at time t = i
• the tab at time t = j
• statement at line i, tab k = s
• k > j

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 k = s
• k > j

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

• the line at time t = i
• the tab at time t = j
• statement at line i, tab k = s
• k > j

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 k = s
• k > j

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 k = s
• k > j

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 k = s
• k > j

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

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