Conditional Properties

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

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

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

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:
• 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) = 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 state at time (t + 1) = "not_expr"

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

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

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

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) = 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 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
• 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
• 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 state at time (t + 1) = expression state 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 '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) = 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 stack at time (t + 1) = 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 state at time (t + 1) = expression state 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_map
• map methods_map contains key method_name = False

then definition of method method_name of class class_name in class_defs = definition of method method_name of base classes (value at "bases" in map class_def) in class_defs

• value at first_base in map class_defs = class_def
• value at "methods" in map class_def = methods_map
• map methods_map contains key method_name = False

then definition of method method_name of base classes [ first_base, rest ] in class_defs = definition of method method_name of base classes rest in class_defs

• definition of method method_name of class class_name in class_defs = method_map
• value at "params" in map method_map = params

then method parameters where the Class Map is class_defs, class name is class_name, and method name is method_name = params

• definition of method method_name of class class_name in class_defs = method_map
• value at "line" in map method_map = line

then line number of method method_name of class class_name in class_defs = line

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

• 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 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

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

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

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 ("while", while_line)

then the line at time (t + 1) = while_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 ("while", while_line)

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) = pair ("while", while_line)

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) = pair ("while", while_line)

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) = pair ("while", while_line)

then Expression Stack at time (t + 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) = pair ("while", while_line)

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 ("while", while_line)

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 ("while", while_line)

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) = pair ("while", while_line)

then the line at time (t + 1) = while_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) = pair ("while", while_line)

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) = pair ("while", while_line)

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) = pair ("while", while_line)

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) = pair ("while", while_line)

then Expression Stack at time (t + 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) = pair ("while", while_line)

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) = pair ("while", while_line)

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) = pair ("while", while_line)

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

then Expression Stack at time (t + 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) = pair ("if", if_value)

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

• 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) = pair ("if", if_value)

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) = pair ("if", if_value)

then Expression Stack at time (t + 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) = pair ("if", if_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
• number of lines = i - 1
• value at (j - 1) in map (Control Map at time t) = pair ("if", if_value)

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) = pair ("if", if_value)

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) = pair ("if", if_value)

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

• the line at time t = i
• the tab at time t = j
• "break" state at t = "breaking"
• value at (j - 1) in map (Control Map at time t) = control_value
• control_value describes a loop = True

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

• the line at time t = i
• the tab at time t = j
• "break" state at t = "breaking"
• value at (j - 1) in map (Control Map at time t) = control_value
• control_value describes a loop = True

then "break" state at (t + 1) = "not_breaking"

• the line at time t = i
• the tab at time t = j
• "break" state at t = "breaking"
• value at (j - 1) in map (Control Map at time t) = control_value
• control_value describes a loop = False

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

• the line at time t = i
• the tab at time t = j
• "break" state at t = "breaking"
• value at (j - 1) in map (Control Map at time t) = control_value
• control_value describes a loop = False

then "break" state at (t + 1) = "breaking"

• the line at time t = i
• the tab at time t = j
• "continue" state at t = "continuing"
• value at (j - 1) in map (Control Map at time t) = control_value
• control_value describes a loop = True

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

• the line at time t = i
• the tab at time t = j
• "continue" state at t = "continuing"
• value at (j - 1) in map (Control Map at time t) = control_value
• control_value describes a loop = True

then "continue" state at (t + 1) = "not_continuing"

• the line at time t = i
• the tab at time t = j
• "continue" state at t = "continuing"
• value at (j - 1) in map (Control Map at time t) = control_value
• control_value describes a loop = False

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

• the line at time t = i
• the tab at time t = j
• "continue" state at t = "continuing"
• value at (j - 1) in map (Control Map at time t) = control_value
• control_value describes a loop = False

then "continue" state at (t + 1) = "continuing"

• the line at time t = i
• the tab at time t = j
• statement at line i, tab j = c
• c is constant

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 = c
• c is constant

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 = c
• c is constant

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 = c
• c is constant

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 = c
• c is constant

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

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