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.

Assign Variable to Constructor Result (2)

if the following are true:

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 (Python constructor with name: class_name and arguments: args)
expression state at time t = "end_expr"

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

Assign Variable to Constructor Result (3)

if the following are true:

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 (Python constructor with name: class_name and arguments: args)
expression state at time t = "end_expr"

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

Assign Variable to Constructor Result (4)

if the following are true:

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 (Python constructor with name: class_name and arguments: args)
expression state at time t = "end_expr"

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

Assign Variable to Constructor Result (5)

if the following are true:

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 (Python constructor with name: class_name and arguments: args)
expression state at time t = "end_expr"

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

Assign Variable to Constructor Result (6)

if the following are true:

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 (Python constructor with name: class_name and arguments: args)
expression state at time t = "end_expr"

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

Assign Get Attribute (1)

if the following are true:

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 expression at time (t + 1) = obj.attr

Assign Get Attribute (2)

if the following are true:

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 expression state at time (t + 1) = "begin_expr"

Assign Get Attribute (3)

if the following are true:

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

Assign Get Attribute (4)

if the following are true:

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

Assign Get Attribute (5)

if the following are true:

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

Assign Get Attribute (6)

if the following are true:

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

Assign Get Attribute (7)

if the following are true:

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

Assign Get Attribute (8)

if the following are true:

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

Assign Get Attribute (9)

if the following are true:

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

Assign Get Attribute (10)

if the following are true:

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

Assign Get Attribute (11)

if the following are true:

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

Assign Variable to Get Attribute Result (1)

if the following are true:

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)

Assign Variable to Get Attribute Result (2)

if the following are true:

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

Assign Variable to Get Attribute Result (3)

if the following are true:

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

Assign Variable to Get Attribute Result (4)

if the following are true:

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

Assign Variable to Get Attribute Result (5)

if the following are true:

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

Assign Variable to Get Attribute Result (6)

if the following are true:

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

Begin Get Attribute (1)

if the following are true:

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 ]

Begin Get Attribute (2)

if the following are true:

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 ]

Begin Get Attribute (3)

if the following are true:

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 ]

Begin Get Attribute (4)

if the following are true:

expression state at time t = "begin_expr"
the expression at time t = obj.attr

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

Get Attribute Object Store

if the following are true:

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

Get Attribute Value Stack

if the following are true:

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

Get Attribute Return Value

if the following are true:

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

Get Attribute Go Parent

if the following are true:

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"

Get Attriburte Go End

if the following are true:

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"

Begin Set Attribute (1)

if the following are true:

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

Begin Set Attribute (2)

if the following are true:

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"

Begin Set Attribute (3)

if the following are true:

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

Begin Set Attribute (4)

if the following are true:

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

Begin Set Attribute (5)

if the following are true:

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

Begin Set Attribute (6)

if the following are true:

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

Begin Set Attribute (7)

if the following are true:

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

Begin Set Attribute (8)

if the following are true:

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

Begin Set Attribute (9)

if the following are true:

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

Set Attribute Unchanged (1)

if the following are true:

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

Set Attribute Unchanged (2)

if the following are true:

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

Set Attribute Unchanged (3)

if the following are true:

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

Set Attribute Unchanged (4)

if the following are true:

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

Set Attribute Unchanged (5)

if the following are true:

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

Begin Set Attribute Arguments (1)

if the following are true:

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 ]

Begin Set Attribute Arguments (2)

if the following are true:

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 ]

Begin Set Attribute Arguments (3)

if the following are true:

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 ]

Begin Set Attribute Arguments (4)

if the following are true:

expression state at time t = "begin_expr"
the expression at time t = obj.key = value

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

Set Attribute

if the following are true:

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)

Set Attribute Value Stack

if the following are true:

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

Set Attribute End

if the following are true:

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"

Set Attribute Ended (1)

if the following are true:

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

Set Attribute Ended (2)

if the following are true:

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

Set Attribute Ended (3)

if the following are true:

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

Set Attribute Ended (4)

if the following are true:

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

Set Attribute Ended (5)

if the following are true:

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

Set Attribute Ended (6)

if the following are true:

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

Set Attribute Ended (7)

if the following are true:

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

Set Attribute Ended (8)

if the following are true:

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

Set Attribute Ended (9)

if the following are true:

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

Return from method unchanged (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 ("method", method_name)

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

Return from method unchanged (2)

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 ("method", method_name)

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

Return from method unchanged (3)

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 ("method", method_name)

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

Return from method unchanged (4)

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 ("method", method_name)

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

Method call finished restore stack (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 ("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

Method call finished restore stack (2)

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

Method call finished restore stack (3)

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

Method call finished restore stack (4)

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

Method call finished restore stack (5)

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

Method call finished restore stack (6)

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

Method call finished restore stack (7)

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

Method call finished restore stack (8)

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

Method call finished restore stack (9)

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

Constructor call return value

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 ("method", "__init__")

then Return Value at time (t + 1) = value at self in map (Variables Map at time t)

Method call return value

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 ("method", method_name)
not (method_name = "__init__")

then Return Value at time (t + 1) = None

Is Not For Since No Key

if map map_a contains key j = False, then map map_a does not contain a for loop entry at line: i and tab: j

Is Not For

if the following are true:

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

Is Not Current For

if the following are true:

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

Start For Loop Iterable Evaluation (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:
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

Start For Loop Iterable Evaluation (2)

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

Start For Loop Iterable Evaluation (3)

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

Start For Loop Iterable Evaluation (4)

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

Start For Loop Iterable Evaluation (5)

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

Start For Loop Iterable Evaluation (6)

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

Start For Loop Iterable Evaluation (7)

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

Start For Loop Iterable Evaluation (8)

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

Start For Loop Iterable Evaluation (9)

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

Start For Loop Iterable Evaluation (10)

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

Start For Loop Iterable Evaluation (11)

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