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.
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))
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)
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
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"
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"
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 ]
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 ]
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 ]
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"
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
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
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
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"
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"
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
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"
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
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
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
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
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) = [ ]
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) = [ ]
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) = [ ]
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 Python Object Store at time (t + 1) = Python Object Store at time t
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 = "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)
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 = "end_expr"
then the line at time (t + 1) = i + 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 = "end_expr"
then the tab at time (t + 1) = the tab at time t
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 = "end_expr"
then stack at time (t + 1) = stack at time t
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 = "end_expr"
then Python Object Store at time (t + 1) = Python Object Store at time t
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 dictionary entries
then Return Value at time (t + 1) = value at a in map entries
if the following are true:
- expression state at time t = "call_function_begin"
- Value Stack at time t = [ [ value, [ key, [ Python reference idx, [ ] ] ] ], stack ]
- the expression at time t = function call with name: "__setitem__" and arguments: [ obj, rest ]
- the element at index idx of stack (Python Object Store at time t) = Python dictionary entries
then Python Object Store at time (t + 1) = result of storing (Python dictionary (result of storing value at key: key in map: entries)) at index idx of stack (Python Object Store at time t)
if the following are true:
- expression state at time t = "call_function_begin"
- Value Stack at time t = [ [ value, [ key, [ Python reference idx, [ ] ] ] ], stack ]
- the expression at time t = function call with name: "__setitem__" and arguments: [ obj, rest ]
- the element at index idx of stack (Python Object Store at time t) = Python dictionary entries
then Value Stack at time (t + 1) = stack
if the following are true:
- expression state at time t = "call_function_begin"
- Value Stack at time t = [ [ value, [ key, [ Python reference idx, [ ] ] ] ], stack ]
- the expression at time t = function call with name: "__setitem__" and arguments: [ obj, rest ]
- the element at index idx of stack (Python Object Store at time t) = Python list elements
then Python Object Store at time (t + 1) = result of storing (Python list (result of storing value at index key of stack elements)) at index idx of stack (Python Object Store at time t)
if the following are true:
- expression state at time t = "call_function_begin"
- Value Stack at time t = [ [ value, [ key, [ Python reference idx, [ ] ] ] ], stack ]
- the expression at time t = function call with name: "__setitem__" and arguments: [ obj, rest ]
- the element at index idx of stack (Python Object Store at time t) = Python list elements
then Value Stack at time (t + 1) = stack
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: "__setitem__" and arguments: args
- expression state at time t = "not_expr"
then Python Object Store at time (t + 1) = Python Object Store at time t
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: "__setitem__" and arguments: args
then expression state at time (t + 1) = "return"
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: "__setitem__" and arguments: args
then expression state at time (t + 1) = "end_expr"
if the following are true:
- the line at time t = i
- the tab at time t = j
- statement at line i, tab j = a class named name with bases: bases
then Class Map at time (t + 1) = result of storing [ entry "bases": bases, [ entry "methods": [ ], [ entry "line": i, [ ] ] ] ] at key: name in map: (Class Map at time t)
if the following are true:
- the line at time t = i
- the tab at time t = j
- statement at line i, tab j = a class named name with bases: bases
then Control Map at time (t + 1) = result of storing (pair ("class", name)) at key: j in map: (Control Map at time t)
if the following are true:
- the line at time t = i
- the tab at time t = j
- statement at line i, tab j = a class named name with bases: bases
then the line at time (t + 1) = i + 1
if the following are true:
- the line at time t = i
- the tab at time t = j
- statement at line i, tab j = a class named name with bases: bases
then the tab at time (t + 1) = j + 1
if the following are true:
- the line at time t = i
- the tab at time t = j
- statement at line i, tab j = a class named name with bases: bases
then Variables Map at time (t + 1) = Variables Map at time t
if the following are true:
- the line at time t = i
- the tab at time t = j
- statement at line i, tab j = a class named name with bases: bases
then stack at time (t + 1) = stack at time t
if the following are true:
- the line at time t = i
- the tab at time t = j
- statement at line i, tab j = a class named name with bases: bases
then "if" map at time (t + 1) = "if" map at time t
if the following are true:
- the line at time t = i
- the tab at time t = j
- statement at line i, tab j = a class named name with bases: bases
then 'while stack' at time (t + 1) = 'while stack' at time t
if the following are true:
- the line at time t = i
- the tab at time t = j
- statement at line i, tab j = a class named name with bases: bases
then Python Object Store at time (t + 1) = Python Object Store at time t
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 ("class", class_name)
then the line at time (t + 1) = the line at time t
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 ("class", class_name)
then the tab at time (t + 1) = j - 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 ("class", class_name)
then expression state at time t = "not_expr"
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 ("class", class_name)
then Control Map at time (t + 1) = Control Map at time t
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 ("class", class_name)
then Variables Map at time (t + 1) = Variables Map at time t
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 ("class", class_name)
then stack at time (t + 1) = stack at time t
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 ("class", class_name)
then "if" map at time (t + 1) = "if" map at time t
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 ("class", class_name)
then expression state at time (t + 1) = expression state at time t
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 ("class", class_name)
then Python Object Store at time (t + 1) = Python Object Store at time t
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 ("class", class_name)
then 'while stack' at time (t + 1) = 'while stack' at time t
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 ("class", class_name)
then Class Map at time (t + 1) = Class Map at time t
if the following are true:
- the line at time t = i
- the tab at time t = j
- statement at line i, tab j = a method named method_name with parameters params
then the line at time (t + 1) = i + 1
if the following are true:
- the line at time t = i
- the tab at time t = j
- statement at line i, tab j = a method named method_name with parameters params
then the tab at time (t + 1) = j
if the following are true:
- the line at time t = i
- the tab at time t = j
- statement at line i, tab j = a method named method_name with parameters params
then Variables Map at time (t + 1) = Variables Map at time t
if the following are true:
- the line at time t = i
- the tab at time t = j
- statement at line i, tab j = a method named method_name with parameters params
then stack at time (t + 1) = stack at time t
if the following are true:
- the line at time t = i
- the tab at time t = j
- statement at line i, tab j = a method named method_name with parameters params
then "if" map at time (t + 1) = "if" map at time t
if the following are true:
- the line at time t = i
- the tab at time t = j
- statement at line i, tab j = a method named method_name with parameters params
then 'while stack' at time (t + 1) = 'while stack' at time t
if the following are true:
- the line at time t = i
- the tab at time t = j
- statement at line i, tab j = a method named method_name with parameters params
then Python Object Store at time (t + 1) = Python Object Store at time t
if the following are true:
- the line at time t = i
- the tab at time t = j
- statement at line i, tab j = a method named method_name with parameters params
then Control Map at time (t + 1) = Control Map at time t
if the following are true:
- the line at time t = i
- the tab at time t = j
- statement at line i, tab j = a method named method_name with parameters params
- value at class_name in map (Class Map at time t) = class_map
- value at "methods" in map class_map = methods_map
then Class Map at time (t + 1) = result of storing (result of storing (result of storing [ entry "params": params, [ entry "line": i, [ ] ] ] at key: method_name in map: methods_map) at key: "methods" in map: class_map) at key: class_name in map: (Class Map at time t)
if the following are true:
- expression state at time t = "call_build_args"
- Parameters List at time t = [ ]
- 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 ]
- line number of method method_name of class class_name in (Class Map at time t) = line
then the line at time (t + 1) = line + 1
if the following are true:
- expression state at time t = "call_build_args"
- Parameters List at time t = [ ]
- 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 ]
- line number of method method_name of class class_name in (Class Map at time t) = line
then the tab at time (t + 1) = 2
if the following are true:
- expression state at time t = "call_build_args"
- Parameters List at time t = [ ]
- 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 ]
- line number of method method_name of class class_name in (Class Map at time t) = line
then Control Map at time (t + 1) = [ entry 0: (pair ("class", class_name)), [ entry 1: (pair ("method", method_name)), [ ] ] ]
if the following are true:
- the line at time t = i
- the tab at time t = j
- statement at line i, tab j = obj.mn(args)
- expression state at time t = "end_expr"
then the line at time (t + 1) = i + 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.mn(args)
- expression state at time t = "end_expr"
then expression state at time (t + 1) = "not_expr"
if the following are true:
- the line at time t = i
- the tab at time t = j
- statement at line i, tab j = obj.mn(args)
- expression state at time t = "end_expr"
then the tab at time (t + 1) = the tab at time t
if the following are true:
- the line at time t = i
- the tab at time t = j
- statement at line i, tab j = obj.mn(args)
- expression state at time t = "end_expr"
then Variables Map at time (t + 1) = Variables Map at time t
if the following are true:
- the line at time t = i
- the tab at time t = j
- statement at line i, tab j = obj.mn(args)
- expression state at time t = "end_expr"
then stack at time (t + 1) = stack at time t
if the following are true:
- the line at time t = i
- the tab at time t = j
- statement at line i, tab j = obj.mn(args)
- expression state at time t = "end_expr"
then Python Object Store at time (t + 1) = Python Object Store at time t
if the following are true:
- the line at time t = i
- the tab at time t = j
- statement at line i, tab j = obj.mn(args)
- expression state at time t = "end_expr"
then Control Map at time (t + 1) = Control Map at time t
if the following are true:
- the line at time t = i
- the tab at time t = j
- statement at line i, tab j = obj.mn(args)
- expression state at time t = "end_expr"
then Class Map at time (t + 1) = Class Map at time t
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_name.method_name(args))
- 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)
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_name.method_name(args))
- expression state at time t = "end_expr"
then the line at time (t + 1) = i + 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_name.method_name(args))
- expression state at time t = "end_expr"
then the tab at time (t + 1) = the tab at time t
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_name.method_name(args))
- expression state at time t = "end_expr"
then stack at time (t + 1) = stack at time t
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_name.method_name(args))
- expression state at time t = "end_expr"
then Python Object Store at time (t + 1) = Python Object Store at time t
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_name.method_name(args))
- expression state at time t = "end_expr"
then Control Map at time (t + 1) = Control Map at time t
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: name and arguments: args)
- expression state at time t = "not_expr"
then the expression at time (t + 1) = Python constructor with name: name and arguments: args
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: name and arguments: args)
- expression state at time t = "not_expr"
then expression state at time (t + 1) = "begin_expr"
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: name and arguments: args)
- expression state at time t = "not_expr"
then the line at time (t + 1) = i
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: name and arguments: args)
- expression state at time t = "not_expr"
then the tab at time (t + 1) = j
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: name and arguments: args)
- expression state at time t = "not_expr"
then Variables Map at time (t + 1) = Variables Map at time t
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: name and arguments: args)
- expression state at time t = "not_expr"
then stack at time (t + 1) = stack at time t
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: name and arguments: args)
- expression state at time t = "not_expr"
then Python Object Store at time (t + 1) = Python Object Store at time t
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: name and arguments: args)
- expression state at time t = "not_expr"
then Control Map at time (t + 1) = Control Map at time t
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: name and arguments: args)
- expression state at time t = "not_expr"
then Value Stack at time (t + 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 constructor with name: name and arguments: args)
- expression state at time t = "not_expr"
then parent stack at time (t + 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 constructor with name: name and arguments: args)
- expression state at time t = "not_expr"
then arguments stack at time (t + 1) = [ ]
if the following are true:
- expression state at time t = "begin_expr"
- the expression at time t = Python constructor with name: class_name and arguments: args
then Value Stack at time (t + 1) = [ [ ], Value Stack at time t ]
if the following are true:
- expression state at time t = "begin_expr"
- the expression at time t = Python constructor with name: class_name and arguments: args
then parent stack at time (t + 1) = [ Python constructor with name: class_name and arguments: args, parent stack at time t ]
if the following are true:
- expression state at time t = "begin_expr"
- the expression at time t = Python constructor with name: class_name and arguments: args
then arguments stack at time (t + 1) = [ args, arguments stack at time t ]
if the following are true:
- expression state at time t = "begin_expr"
- the expression at time t = Python constructor with name: class_name and arguments: args
then expression state at time (t + 1) = "iterate_args"
if the following are true:
- expression state at time t = "call_function_begin"
- the expression at time t = Python constructor with name: class_name and arguments: args
then Python Object Store at time (t + 1) = Python Object Store at time t
if the following are true:
- expression state at time t = "call_function_begin"
- Value Stack at time t = [ evaluated, stack ]
- the expression at time t = Python constructor with name: class_name and arguments: args
then expression state at time (t + 1) = "call_build_args"