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 (Python list elements)
- 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 (Python list elements)
- 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 = obj_name.method_name(args)
- expression state at time t = "not_expr"
then the expression at time (t + 1) = obj_name.method_name(args)
- 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"
- 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
- 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
- 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) = [ ]
- 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) = [ ]
- 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) = [ ]
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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)
- 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"
- 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
- 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
- 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) = [ ]
- 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) = [ ]
- 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) = [ ]
- 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
- 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
- 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
- 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
- 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
- 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
- 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 ]
- 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 ]
- 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 ]
- 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"
- 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
- 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)
- 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"
- 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
- 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
- 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
- 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
- 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"
- 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
- 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
- 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 ]
- 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
- 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
- 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
- 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
- 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"
- 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"
- 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
- 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
- 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"
- 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"
- 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
- 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)
- 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
- 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"
- 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"
- 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
- 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
- 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
- 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"
- 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"
- 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
- 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"
- 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
- 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
- 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) = [ ]
- 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) = [ ]
- 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) = [ ]
- 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
- 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
- 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 ]
- 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 ]
- 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 ]
- expression state at time t = "begin_expr"
- the expression at time t = Python dictionary entries
then expression state at time (t + 1) = "iterate_args"
- 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))
- 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)
- 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
- 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"
- 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"
- 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 ]
- 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 ]
- 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 ]
- expression state at time t = "begin_expr"
- the expression at time t = entry key: value
then expression state at time (t + 1) = "iterate_args"
- 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
- 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
- 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
- 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"
- 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"
- 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
- 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"
- 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
- 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
- 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
- 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
- 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) = [ ]
- 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) = [ ]
- 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) = [ ]