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