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 List 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 list elements)
expression state at time t = "end_expr"

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

Assign Variable to List 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 list elements)
expression state at time t = "end_expr"

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

Method Call Begin (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_name.method_name(args)
expression state at time t = "not_expr"

then the expression at time (t + 1) = obj_name.method_name(args)

Method Call Begin (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_name.method_name(args)
expression state at time t = "not_expr"

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

Method Call Begin (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_name.method_name(args)
expression state at time t = "not_expr"

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

Method Call Begin (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_name.method_name(args)
expression state at time t = "not_expr"

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

Method Call Begin (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_name.method_name(args)
expression state at time t = "not_expr"

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

Method Call Begin (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_name.method_name(args)
expression state at time t = "not_expr"

then parent stack at time (t + 1) = [ ]

Method Call Begin (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_name.method_name(args)
expression state at time t = "not_expr"

then arguments stack at time (t + 1) = [ ]

Method Call Begin (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_name.method_name(args)
expression state at time t = "not_expr"

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

Method Call Begin (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_name.method_name(args)
expression state at time t = "not_expr"

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

Method Call Begin (10)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = obj_name.method_name(args)
expression state at time t = "not_expr"

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

Method Call Begin (11)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = obj_name.method_name(args)
expression state at time t = "not_expr"

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

Method Call Begin (12)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = obj_name.method_name(args)
expression state at time t = "not_expr"

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

Method Call Begin (13)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = obj_name.method_name(args)
expression state at time t = "not_expr"

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

Unchanged on method Call

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = obj_name.method_name(args)

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

Assign Method Call Begin (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 target and expression (obj_name.method_name(args))
expression state at time t = "not_expr"

then the expression at time (t + 1) = obj_name.method_name(args)

Assign Method Call Begin (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 target and expression (obj_name.method_name(args))
expression state at time t = "not_expr"

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

Assign Method Call Begin (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 target and expression (obj_name.method_name(args))
expression state at time t = "not_expr"

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

Assign Method Call Begin (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 target and expression (obj_name.method_name(args))
expression state at time t = "not_expr"

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

Assign Method Call Begin (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 target and expression (obj_name.method_name(args))
expression state at time t = "not_expr"

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

Assign Method Call Begin (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 target and expression (obj_name.method_name(args))
expression state at time t = "not_expr"

then parent stack at time (t + 1) = [ ]

Assign Method Call Begin (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 target and expression (obj_name.method_name(args))
expression state at time t = "not_expr"

then arguments stack at time (t + 1) = [ ]

Assign Method Call Begin (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 target and expression (obj_name.method_name(args))
expression state at time t = "not_expr"

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

Assign Method Call Begin (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 target and expression (obj_name.method_name(args))
expression state at time t = "not_expr"

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

Assign Method Call Begin (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 target and expression (obj_name.method_name(args))
expression state at time t = "not_expr"

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

Assign Method Call Begin (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 target and expression (obj_name.method_name(args))
expression state at time t = "not_expr"

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

Assign Method Call Begin (12)

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 target and expression (obj_name.method_name(args))
expression state at time t = "not_expr"

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

Assign Method Call Begin (13)

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 target and expression (obj_name.method_name(args))
expression state at time t = "not_expr"

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

Begin Method Arguments (1)

if the following are true:

expression state at time t = "begin_expr"
the expression at time t = obj_name.method_name(args)

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

Begin Method Arguments (2)

if the following are true:

expression state at time t = "begin_expr"
the expression at time t = obj_name.method_name(args)

then parent stack at time (t + 1) = [ obj_name.method_name(args), parent stack at time t ]

Begin Method Arguments (3)

if the following are true:

expression state at time t = "begin_expr"
the expression at time t = obj_name.method_name(args)

then arguments stack at time (t + 1) = [ args, arguments stack at time t ]

Begin Method Arguments (4)

if the following are true:

expression state at time t = "begin_expr"
the expression at time t = obj_name.method_name(args)

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

Append 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 = obj.method_name(args)

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

Append Value

if the following are true:

expression state at time t = "call_function_begin"
Value Stack at time t = [ [ value, [ ] ], stack ]
the expression at time t = obj.append(x)
value at obj in map (Variables Map at time t) = Python reference idx
the element at index idx of stack (Python Object Store at time t) = Python list entries

then Python Object Store at time (t + 1) = result of storing (Python list (result of appending value to entries)) at index idx of stack (Python Object Store at time t)

Method Call 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."append"(args)

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

Unchanged on method call (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."append"(el)

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

Unchanged on method call (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."append"(el)

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

Unchanged on method call (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."append"(el)

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

Unchanged on method call (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."append"(el)

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

Method Call Begin

if the following are true:

expression state at time t = "call_function_begin"
the expression at time t = obj_name.method_name(args)
value at obj_name in map (Variables Map at time t) = Python reference index
the element at index index of stack (Python Object Store at time t) = Python object: [ entry "__class_name__": class_name, e_rest ]
map (Class Map at time t) contains key class_name = True

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

Call Method Begin Set Params (1)

if the following are true:

expression state at time t = "call_function_begin"
the expression at time t = obj_name.method_name(args)
value at obj_name in map (Variables Map at time t) = Python reference index
the element at index index of stack (Python Object Store at time t) = Python object: [ entry "__class_name__": class_name, e_rest ]
method parameters where the Class Map is (Class Map at time t), class name is class_name, and method name is method_name = params

then Parameters List at time (t + 1) = params

Call Method Begin Set Params (2)

if the following are true:

expression state at time t = "call_function_begin"
the expression at time t = obj_name.method_name(args)
value at obj_name in map (Variables Map at time t) = Python reference index
the element at index index of stack (Python Object Store at time t) = Python object: [ entry "__class_name__": class_name, e_rest ]
method parameters where the Class Map is (Class Map at time t), class name is class_name, and method name is method_name = params

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

Call Method Values (1)

if the following are true:

expression state at time t = "call_function_begin"
the expression at time t = obj_name.method_name(args)
value at obj_name in map (Variables Map at time t) = Python reference index
the element at index index of stack (Python Object Store at time t) = Python object: [ entry "__class_name__": class_name, e_rest ]
Value Stack at time t = [ values, v_stack ]
definition of method method_name of class class_name in (Class Map at time t) = method_map

then Argument Values at time (t + 1) = [ Python reference index, reverse of values ]

Call Method Values (2)

if the following are true:

expression state at time t = "call_function_begin"
the expression at time t = obj_name.method_name(args)
value at obj_name in map (Variables Map at time t) = Python reference index
the element at index index of stack (Python Object Store at time t) = Python object: [ entry "__class_name__": class_name, e_rest ]
Value Stack at time t = [ values, v_stack ]
definition of method method_name of class class_name in (Class Map at time t) = method_map

then Value Stack at time (t + 1) = v_stack

getitem unchanged

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = function call with name: "__getitem__" and arguments: args
expression state at time t = "not_expr"

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

Get Item Return Value

if the following are true:

expression state at time t = "call_function_begin"
Value Stack at time t = [ [ a, [ Python reference idx, [ ] ] ], stack ]
the expression at time t = function call with name: "__getitem__" and arguments: args
the element at index idx of stack (Python Object Store at time t) = Python list entries

then Return Value at time (t + 1) = the element at index a of stack entries

Get Item Object Store

if the following are true:

expression state at time t = "call_function_begin"
the expression at time t = function call with name: "__getitem__" and arguments: args

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

Get Item Return

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 = function call with name: "__getitem__" and arguments: args

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

Get Item End

if the following are true:

expression state at time t = "call_function_begin"
parent stack at time t = [ ]
the expression at time t = function call with name: "__getitem__" and arguments: args

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

get length unchanged

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = function call with name: "len" and arguments: args
expression state at time t = "not_expr"

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

Get Python Length

if the following are true:

expression state at time t = "call_function_begin"
Value Stack at time t = [ [ Python reference idx, [ ] ], stack ]
the expression at time t = function call with name: "len" and arguments: args
the element at index idx of stack (Python Object Store at time t) = Python list entries

then Return Value at time (t + 1) = length of stack entries

Get Python Length Return

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 = function call with name: "len" and arguments: args

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

Get Python Length End

if the following are true:

expression state at time t = "call_function_begin"
parent stack at time t = [ ]
the expression at time t = function call with name: "len" and arguments: args

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

get Python length object store

if the following are true:

expression state at time t = "call_function_begin"
the expression at time t = function call with name: "len" and arguments: args

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

Pop from list objects (1)

if the following are true:

expression state at time t = "call_function_begin"
Value Stack at time t = [ [ a, [ ] ], stack ]
the expression at time t = name."pop"(args)
value at obj in map (Variables Map at time t) = Python reference idx
the element at index idx of stack (Python Object Store at time t) = Python list entries

then Python Object Store at time (t + 1) = result of storing (Python list (stack after popping a value from stack entries at index a)) at index idx of stack (Python Object Store at time t)

Pop from list objects (2)

if the following are true:

expression state at time t = "call_function_begin"
Value Stack at time t = [ [ a, [ ] ], stack ]
the expression at time t = name."pop"(args)
value at obj in map (Variables Map at time t) = Python reference idx
the element at index idx of stack (Python Object Store at time t) = Python list entries

then Return Value at time (t + 1) = the element at index a of stack entries

Pop From List Return

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."pop"(args)

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

Pop From List 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."pop"(args)

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

contains unchanged

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = function call with name: "__contains__" and arguments: args
expression state at time t = "not_expr"

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

contains call unchanged

if the following are true:

expression state at time t = "call_function_begin"
the expression at time t = function call with name: "__contains__" and arguments: args

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

Contains Item

if the following are true:

expression state at time t = "call_function_begin"
Value Stack at time t = [ [ a, [ Python reference idx, [ ] ] ], stack ]
the expression at time t = function call with name: "__contains__" and arguments: args
the element at index idx of stack (Python Object Store at time t) = Python list entries

then Return Value at time (t + 1) = stack entries contains a

Contains Item Return

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 = function call with name: "__contains__" and arguments: args

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

Contains Item End

if the following are true:

expression state at time t = "call_function_begin"
parent stack at time t = [ ]
the expression at time t = function call with name: "__contains__" and arguments: args

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

Begin Dict (1)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = Python dictionary entries
expression state at time t = "not_expr"

then the expression at time (t + 1) = Python dictionary entries

Begin Dict (2)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = Python dictionary entries
expression state at time t = "not_expr"

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

Begin Dict (3)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = Python dictionary entries
expression state at time t = "not_expr"

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

Begin Dict (4)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = Python dictionary entries
expression state at time t = "not_expr"

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

Begin Dict (5)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = Python dictionary entries
expression state at time t = "not_expr"

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

Begin Dict (6)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = Python dictionary entries
expression state at time t = "not_expr"

then parent stack at time (t + 1) = [ ]

Begin Dict (7)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = Python dictionary entries
expression state at time t = "not_expr"

then arguments stack at time (t + 1) = [ ]

Begin Dict (8)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = Python dictionary entries
expression state at time t = "not_expr"

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

Begin Dict (9)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = Python dictionary entries
expression state at time t = "not_expr"

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

Begin Dict Elements (1)

if the following are true:

expression state at time t = "begin_expr"
the expression at time t = Python dictionary entries

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

Begin Dict Elements (2)

if the following are true:

expression state at time t = "begin_expr"
the expression at time t = Python dictionary entries

then parent stack at time (t + 1) = [ Python dictionary entries, parent stack at time t ]

Begin Dict Elements (3)

if the following are true:

expression state at time t = "begin_expr"
the expression at time t = Python dictionary entries

then arguments stack at time (t + 1) = [ entries, arguments stack at time t ]

Begin Dict Elements (4)

if the following are true:

expression state at time t = "begin_expr"
the expression at time t = Python dictionary entries

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

Call Func Dictionary (1)

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 = Python dictionary elements

then Return Value at time (t + 1) = Python reference (length of stack (Python Object Store at time t))

Call Func Dictionary (2)

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 = Python dictionary elements

then Python Object Store at time (t + 1) = result of appending (Python dictionary (reverse of values)) to (Python Object Store at time t)

Call Func Dictionary (3)

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 = Python dictionary elements

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

Call Dictionary Return

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 = Python dictionary elements

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

Call Dictionary End

if the following are true:

expression state at time t = "call_function_begin"
parent stack at time t = [ ]
the expression at time t = Python dictionary elements

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

Begin Entry Elements (1)

if the following are true:

expression state at time t = "begin_expr"
the expression at time t = entry key: value

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

Begin Entry Elements (2)

if the following are true:

expression state at time t = "begin_expr"
the expression at time t = entry key: value

then parent stack at time (t + 1) = [ entry key: value, parent stack at time t ]

Begin Entry Elements (3)

if the following are true:

expression state at time t = "begin_expr"
the expression at time t = entry key: value

then arguments stack at time (t + 1) = [ [ key, [ value, [ ] ] ], arguments stack at time t ]

Begin Entry Elements (4)

if the following are true:

expression state at time t = "begin_expr"
the expression at time t = entry key: value

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

entry object store unchanged

if the following are true:

expression state at time t = "call_function_begin"
the expression at time t = entry key: value

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

Call Func Entry (1)

if the following are true:

expression state at time t = "call_function_begin"
Value Stack at time t = [ [ evaluated_value, [ evaluated_key, [ ] ] ], stack ]
the expression at time t = entry key: value

then Return Value at time (t + 1) = entry evaluated_key: evaluated_value

Call Func Entry (2)

if the following are true:

expression state at time t = "call_function_begin"
Value Stack at time t = [ [ evaluated_value, [ evaluated_key, [ ] ] ], stack ]
the expression at time t = entry key: value

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

Call Entry Return

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 = entry key: value

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

Call Entry End

if the following are true:

expression state at time t = "call_function_begin"
parent stack at time t = [ ]
the expression at time t = entry key: value

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

Assign Dict (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 (Python dictionary elements)
expression state at time t = "not_expr"

then the expression at time (t + 1) = Python dictionary elements

Assign Dict (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 dictionary elements)
expression state at time t = "not_expr"

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

Assign Dict (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 dictionary elements)
expression state at time t = "not_expr"

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

Assign Dict (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 dictionary elements)
expression state at time t = "not_expr"

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

Assign Dict (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 dictionary elements)
expression state at time t = "not_expr"

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

Assign Dict (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 dictionary elements)
expression state at time t = "not_expr"

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

Assign Dict (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 (Python dictionary elements)
expression state at time t = "not_expr"

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

Assign Dict (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 (Python dictionary elements)
expression state at time t = "not_expr"

then parent stack at time (t + 1) = [ ]

Assign Dict (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 (Python dictionary elements)
expression state at time t = "not_expr"

then arguments stack at time (t + 1) = [ ]

10 11 12