Conditional Properties

if the following are true:

• 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

if the following are true:

• 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

if the following are true:

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

if the following are true:

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

if the following are true:

• 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

if the following are true:

• 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

if the following are true:

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

if the following are true:

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

if the following are true:

• 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

if the following are true:

• 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

if the following are true:

• 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

if the following are true:

• 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

if the following are true:

• 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

if the following are true:

• 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

if the following are true:

• 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

if the following are true:

• 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

if the following are true:

• 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

if the following are true:

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

if the following are true:

• 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

if the following are true:

• 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

if the following are true:

• 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

if the following are true:

• 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

if the following are true:

• 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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

if the following are true:

• 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

if the following are true:

• 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

if the following are true:

• 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

if the following are true:

• 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

if the following are true:

• 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

if the following are true:

• 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

if the following are true:

• 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

if the following are true:

• 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

if the following are true:

• 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

if the following are true:

• 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

if value at method_name in map (value at "methods" in map (value at class_name in map class_defs)) = method_map, then definition of method method_name of class class_name and base classes in class_defs = method_map

if value at method_name in map (value at "methods" in map (value at class_name in map class_defs)) = method_map, then definition of method method_name of class class_name in class_defs = method_map

if the following are true:

• 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 and base classes in class_defs = definition of method method_name in base classes (value at "bases" in map class_def) in class_defs

if definition of method method_name of class first_base and base classes in class_defs = method_map, then definition of method method_name in base classes [ first_base, rest ] in class_defs = method_map

if the following are true:

• 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 in base classes [ first_base, rest ] in class_defs = definition of method method_name in base classes rest in class_defs

if the following are true:

• definition of method method_name of class class_name and base classes 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

if the following are true:

• definition of method method_name of class class_name and base classes 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

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

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

then Expression Stack at time (t + 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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

if the following are true:

• 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

if the following are true:

• 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

if the following are true:

• 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

if the following are true:

• 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

if the following are true:

• 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) = [ ]

if the following are true:

• 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

if the following are true:

• 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

if the following are true:

• 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

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

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

if the following are true:

• 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

if the following are true:

• 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

if the following are true:

• 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) = [ ]

if the following are true:

• 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

if the following are true:

• 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

if the following are true:

• 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

if the following are true:

• 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

if the following are true:

• 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

if the following are true:

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

if the following are true:

• 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

if the following are true:

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

if "break" state at t = "breaking", then the tab at time (t + 1) = (the tab at time t) - 1

if "break" state at t = "breaking", then Python Object Store at time (t + 1) = Python Object Store at time t

if "break" state at t = "breaking", then Class Map at time (t + 1) = Class Map at time t

if "break" state at t = "breaking", then Variables Map at time (t + 1) = Variables Map at time t

if "break" state at t = "breaking", then Context Stack at time (t + 1) = Context Stack at time t

if "break" state at t = "breaking", then Control Map at time (t + 1) = Control Map at time t

if the following are true:

• 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

if the following are true:

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

if the following are true:

• 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

if the following are true:

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

if "continue" state at t = "continuing", then the tab at time (t + 1) = (the tab at time t) - 1

if "continue" state at t = "continuing", then Expression Stack at time (t + 1) = [ ]

if "continue" state at t = "continuing", then Python Object Store at time (t + 1) = Python Object Store at time t

if "continue" state at t = "continuing", then Class Map at time (t + 1) = Class Map at time t