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:
- 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"
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 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 = [ evaluated, stack ]
- the expression at time t = Python constructor with name: class_name and arguments: args
then Argument Values at time (t + 1) = reverse of evaluated
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
- method parameters where the Class Map is (Class Map at time t), class name is class_name, and method name is "__init__" = params
then Parameters List at time (t + 1) = params
if the following are true:
- expression state at time t = "call_build_args"
- the expression at time t = Python constructor with name: class_name and arguments: args
- Function Variables Map at time t = [ ]
- Parameters List at time t = [ self, p_rest ]
then Function Variables Map at time (t + 1) = [ entry self: (Python reference (length of stack (Python Object Store at time t))), [ ] ]
if the following are true:
- expression state at time t = "call_build_args"
- the expression at time t = Python constructor with name: class_name and arguments: args
- Function Variables Map at time t = [ ]
- Parameters List at time t = [ self, p_rest ]
then Python Object Store at time (t + 1) = result of appending (Python object: [ entry "__class_name__": class_name, [ ] ]) to (Python Object Store at time t)
if the following are true:
- expression state at time t = "call_build_args"
- the expression at time t = Python constructor with name: class_name and arguments: args
- Function Variables Map at time t = [ ]
- Parameters List at time t = [ self, p_rest ]
then Parameters List at time (t + 1) = p_rest
if the following are true:
- expression state at time t = "call_build_args"
- the expression at time t = Python constructor with name: class_name and arguments: args
- Function Variables Map at time t = [ ]
- Parameters List at time t = [ self, p_rest ]
then Argument Values at time (t + 1) = Argument Values at time t
if the following are true:
- expression state at time t = "call_build_args"
- the expression at time t = Python constructor with name: class_name and arguments: args
- Function Variables Map at time t = [ ]
- Parameters List at time t = [ self, p_rest ]
then expression state at time (t + 1) = "call_build_args"
if the following are true:
- expression state at time t = "call_build_args"
- the expression at time t = Python constructor with name: class_name and arguments: args
- Function Variables Map at time t = [ ]
- Parameters List at time t = [ self, p_rest ]
then Variables Map at time (t + 1) = Variables Map at time t
if the following are true:
- expression state at time t = "call_build_args"
- the expression at time t = Python constructor with name: class_name and arguments: args
- Function Variables Map at time t = [ ]
- Parameters List at time t = [ self, p_rest ]
then stack at time (t + 1) = stack at time t
if the following are true:
- expression state at time t = "call_build_args"
- the expression at time t = Python constructor with name: class_name and arguments: args
- Function Variables Map at time t = [ ]
- Parameters List at time t = [ self, p_rest ]
then Control Map at time (t + 1) = Control 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 = Python constructor with name: class_name and arguments: args
- line number of method "__init__" 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 = Python constructor with name: class_name and arguments: args
- line number of method "__init__" 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 = Python constructor with name: class_name and arguments: args
- line number of method "__init__" 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", "__init__")), [ ] ] ]
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 Variables Map at time (t + 1) = result of storing (Return Value at time t) at key: x in map: (Variables Map at time t)