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.
- Expression Stack at time t = [ [ ], [ [ Python dictionary entries, ys ], rest ] ]
- Value Stack at time t = [ values, [ next_level, other_levels ] ]
then Value Stack at time (t + 1) = [ [ Python reference (length of stack (Python Object Store at time t)), next_level ], other_levels ]
- Expression Stack at time t = [ [ ], [ [ Python dictionary entries, ys ], rest ] ]
- Value Stack at time t = [ values, [ next_level, other_levels ] ]
then Python Object Store at time (t + 1) = result of appending (Python dictionary (reverse of values)) to (Python Object Store at time t)
- Expression Stack at time t = [ [ ], [ [ entry key: value, ys ], rest ] ]
- Value Stack at time t = [ [ evaluated_value, [ evaluated_key, [ ] ] ], [ next_level, other_levels ] ]
then Value Stack at time (t + 1) = [ [ entry evaluated_key: evaluated_value, next_level ], other_levels ]
- 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 Stack at time t = [ ]
then Expression Stack 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 Stack at time t = [ ]
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 Stack at time t = [ ]
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 Stack at time t = [ ]
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 Stack at time t = [ ]
then Context Stack at time (t + 1) = Context 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 Stack at time t = [ ]
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 Stack at time t = [ ]
then Python Object Store at time (t + 1) = Python Object Store at time t
- Expression Stack at time t = [ [ ], [ [ function call with name: "__getitem__" and arguments: args, ys ], rest ] ]
- Value Stack at time t = [ [ a, [ Python reference idx, [ ] ] ], [ next_level, other_levels ] ]
- the element at index idx of stack (Python Object Store at time t) = Python dictionary entries
then Value Stack at time (t + 1) = [ [ value at a in map entries, next_level ], other_levels ]
- Expression Stack at time t = [ [ ], [ [ function call with name: "__setitem__" and arguments: args, ys ], rest ] ]
- Value Stack at time t = [ [ value, [ key, [ Python reference idx, [ ] ] ] ], [ next_level, other_levels ] ]
- 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)
- Expression Stack at time t = [ [ ], [ [ function call with name: "__setitem__" and arguments: args, ys ], rest ] ]
- Value Stack at time t = [ [ value, [ key, [ Python reference idx, [ ] ] ] ], [ next_level, other_levels ] ]
- the element at index idx of stack (Python Object Store at time t) = Python dictionary entries
then Value Stack at time (t + 1) = [ [ None, next_level ], other_levels ]
- Expression Stack at time t = [ [ ], [ [ function call with name: "__setitem__" and arguments: args, ys ], rest ] ]
- Value Stack at time t = [ [ value, [ key, [ Python reference idx, [ ] ] ] ], [ next_level, other_levels ] ]
- 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)
- Expression Stack at time t = [ [ ], [ [ function call with name: "__setitem__" and arguments: args, ys ], rest ] ]
- Value Stack at time t = [ [ value, [ key, [ Python reference idx, [ ] ] ] ], [ next_level, other_levels ] ]
- the element at index idx of stack (Python Object Store at time t) = Python list elements
then Value Stack at time (t + 1) = [ [ None, next_level ], other_levels ]
- 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 Stack at time t = [ ]
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 = 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)
- 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)
- 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
- 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
- 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
- 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 Context Stack at time (t + 1) = Context Stack at time t
- 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
- 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
- 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
- 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
- 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
- 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 Stack at time t = [ ]
- 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
- 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
- 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 Context Stack at time (t + 1) = Context Stack at time t
- 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
- 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 Stack at time (t + 1) = Expression Stack at time t
- 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
- 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
- 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
- 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
- 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
- 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
- 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 Context Stack at time (t + 1) = Context Stack at time t
- 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
- 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
- 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
- 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
- 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)
- Expression Stack at time t = [ [ ], [ [ obj_name.method_name(args), ys ], rest ] ]
- 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
- Parameters List at time t = None
- Value Stack at time t = [ values, v_stack ]
then Parameters List at time (t + 1) = params
- Expression Stack at time t = [ [ ], [ [ obj_name.method_name(args), ys ], rest ] ]
- 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
- Parameters List at time t = None
- Value Stack at time t = [ values, v_stack ]
then Value Stack at time (t + 1) = v_stack
- Expression Stack at time t = [ [ ], [ [ obj_name.method_name(args), ys ], rest ] ]
- 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
- Parameters List at time t = None
- Value Stack at time t = [ values, v_stack ]
then Function Variables Map at time (t + 1) = [ ]
- Expression Stack at time t = [ [ ], [ [ obj_name.method_name(args), ys ], rest ] ]
- 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
- Parameters List at time t = None
- Value Stack at time t = [ values, v_stack ]
then Argument Values at time (t + 1) = [ Python reference index, reverse of values ]
- Expression Stack at time t = [ [ ], [ [ obj_name.method_name(args), ys ], rest ] ]
- 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
- Parameters List at time t = None
- Value Stack at time t = [ values, v_stack ]
then Expression Stack at time (t + 1) = Expression Stack at time t
- Expression Stack at time t = [ [ ], [ [ obj_name.method_name(args), ys ], rest ] ]
- 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
- Parameters List at time t = None
- Value Stack at time t = [ values, v_stack ]
then Variables Map at time (t + 1) = Variables Map at time t
- Expression Stack at time t = [ [ ], [ [ obj_name.method_name(args), ys ], rest ] ]
- 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
- Parameters List at time t = None
- Value Stack at time t = [ values, v_stack ]
then Control Map at time (t + 1) = Control Map at time t
- Expression Stack at time t = [ [ ], [ [ obj_name.method_name(args), ys ], rest ] ]
- 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
- Parameters List at time t = None
- Value Stack at time t = [ values, v_stack ]
then Python Object Store at time (t + 1) = Python Object Store at time t
- Expression Stack at time t = [ [ ], [ [ obj_name.method_name(args), ys ], rest ] ]
- 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
- Parameters List at time t = None
- Value Stack at time t = [ values, v_stack ]
then Context Stack at time (t + 1) = Context Stack at time t
- Expression Stack at time t = [ [ ], [ [ obj_name.method_name(args), ys ], rest ] ]
- 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
- Parameters List at time t = None
- Value Stack at time t = [ values, v_stack ]
then the line at time (t + 1) = the line at time t
- Expression Stack at time t = [ [ ], [ [ obj_name.method_name(args), ys ], rest ] ]
- 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
- Parameters List at time t = None
- Value Stack at time t = [ values, v_stack ]
then the tab at time (t + 1) = the tab at time t
- Parameters List at time t = [ ]
- Expression Stack at time t = [ [ ], [ [ obj_name.method_name(args), ys ], rest ] ]
- 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
- Parameters List at time t = [ ]
- Expression Stack at time t = [ [ ], [ [ obj_name.method_name(args), ys ], rest ] ]
- 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
- Parameters List at time t = [ ]
- Expression Stack at time t = [ [ ], [ [ obj_name.method_name(args), ys ], rest ] ]
- 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)), [ ] ] ]
- Return Value at time t = [ r, [ ] ]
- Expression Stack at time t = [ [ ], [ [ name.method(args), ys ], rest ] ]
- Value Stack at time t = [ next_level, other_levels ]
then Value Stack at time (t + 1) = [ [ r, next_level ], other_levels ]
- Return Value at time t = [ r, [ ] ]
- Expression Stack at time t = [ [ ], [ [ name.method(args), ys ], rest ] ]
- Value Stack at time t = [ next_level, other_levels ]
then Expression Stack at time (t + 1) = [ ys, rest ]
- Return Value at time t = [ r, [ ] ]
- Expression Stack at time t = [ [ ], [ [ name.method(args), ys ], rest ] ]
- Value Stack at time t = [ next_level, other_levels ]
then Return Value at time (t + 1) = [ ]
- Return Value at time t = [ r, [ ] ]
- Expression Stack at time t = [ [ ], [ [ name.method(args), ys ], rest ] ]
- Value Stack at time t = [ next_level, other_levels ]
then Parameters List at time (t + 1) = None
- Return Value at time t = [ r, [ ] ]
- Expression Stack at time t = [ [ ], [ [ name.method(args), ys ], rest ] ]
- Value Stack at time t = [ next_level, other_levels ]
then Variables Map at time (t + 1) = Variables Map at time t
- Return Value at time t = [ r, [ ] ]
- Expression Stack at time t = [ [ ], [ [ name.method(args), ys ], rest ] ]
- Value Stack at time t = [ next_level, other_levels ]
then Control Map at time (t + 1) = Control Map at time t