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