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:
- 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 Context Stack at time (t + 1) = Context Stack at time t
if the following are true:
- 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 the line at time (t + 1) = the line at time t
if the following are true:
- 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 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 Stack at time t = [ [ ], [ ] ]
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 Stack at time t = [ [ ], [ ] ]
then Expression 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 = obj.mn(args)
- Expression Stack at time t = [ [ ], [ ] ]
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 Stack at time t = [ [ ], [ ] ]
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 Stack at time t = [ [ ], [ ] ]
then Context Stack at time (t + 1) = Context 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 Stack at time t = [ [ ], [ ] ]
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 Stack at time t = [ [ ], [ ] ]
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 (obj_name.method_name(args))
- Expression Stack at time t = [ [ ], [ ] ]
- Value Stack at time t = [ [ value, [ ] ], [ ] ]
then Variables Map at time (t + 1) = result of storing value 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 Stack at time t = [ [ ], [ ] ]
- Value Stack at time t = [ [ value, [ ] ], [ ] ]
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 Stack at time t = [ [ ], [ ] ]
- Value Stack at time t = [ [ value, [ ] ], [ ] ]
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 Stack at time t = [ [ ], [ ] ]
- Value Stack at time t = [ [ value, [ ] ], [ ] ]
then Context Stack at time (t + 1) = Context 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 Stack at time t = [ [ ], [ ] ]
- Value Stack at time t = [ [ value, [ ] ], [ ] ]
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 Stack at time t = [ [ ], [ ] ]
- Value Stack at time t = [ [ value, [ ] ], [ ] ]
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 Stack at time t = [ ]
then Expression Stack 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 Stack at time t = [ ]
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 Stack at time t = [ ]
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 Stack at time t = [ ]
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 Stack at time t = [ ]
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 Stack at time t = [ ]
then Context Stack at time (t + 1) = Context 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 Stack at time t = [ ]
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 Stack at time t = [ ]
then Control Map at time (t + 1) = Control Map at time t
if Expression Stack at time t = [ [ Python constructor with name: class_name and arguments: args, ys ], rest ], then Value Stack at time (t + 1) = [ [ ], Value Stack at time t ]
if Expression Stack at time t = [ [ Python constructor with name: class_name and arguments: args, ys ], rest ], then Expression Stack at time (t + 1) = [ args, [ [ Python constructor with name: class_name and arguments: args, ys ], rest ] ]
if Expression Stack at time t = [ [ Python constructor with name: class_name and arguments: args, ys ], rest ], then Parameters List at time (t + 1) = None
if Expression Stack at time t = [ [ Python constructor with name: class_name and arguments: args, ys ], rest ], then the line at time (t + 1) = the line at time t
if Expression Stack at time t = [ [ Python constructor with name: class_name and arguments: args, ys ], rest ], then the tab at time (t + 1) = the tab at time t
if Expression Stack at time t = [ [ Python constructor with name: class_name and arguments: args, ys ], rest ], then Variables Map at time (t + 1) = Variables Map at time t
if Expression Stack at time t = [ [ Python constructor with name: class_name and arguments: args, ys ], rest ], then Control Map at time (t + 1) = Control Map at time t
if Expression Stack at time t = [ [ Python constructor with name: class_name and arguments: args, ys ], rest ], then Python Object Store at time (t + 1) = Python Object Store at time t
if Expression Stack at time t = [ [ Python constructor with name: class_name and arguments: args, ys ], rest ], then Context Stack at time (t + 1) = Context Stack at time t
if the following are true:
- Expression Stack at time t = [ [ ], [ [ Python constructor with name: class_name and arguments: args, ys ], rest ] ]
- Value Stack at time t = [ evaluated, stack ]
- method parameters where the Class Map is (Class Map at time t), class name is class_name, and method name is "__init__" = params
- Parameters List at time t = None
then Value Stack at time (t + 1) = stack
if the following are true:
- Expression Stack at time t = [ [ ], [ [ Python constructor with name: class_name and arguments: args, ys ], rest ] ]
- Value Stack at time t = [ evaluated, stack ]
- method parameters where the Class Map is (Class Map at time t), class name is class_name, and method name is "__init__" = params
- Parameters List at time t = None
then Parameters List at time (t + 1) = params
if the following are true:
- Expression Stack at time t = [ [ ], [ [ Python constructor with name: class_name and arguments: args, ys ], rest ] ]
- Value Stack at time t = [ evaluated, stack ]
- method parameters where the Class Map is (Class Map at time t), class name is class_name, and method name is "__init__" = params
- Parameters List at time t = None
then Function Variables Map at time (t + 1) = [ ]
if the following are true:
- Expression Stack at time t = [ [ ], [ [ Python constructor with name: class_name and arguments: args, ys ], rest ] ]
- Value Stack at time t = [ evaluated, stack ]
- method parameters where the Class Map is (Class Map at time t), class name is class_name, and method name is "__init__" = params
- Parameters List at time t = None
then Argument Values at time (t + 1) = reverse of evaluated
if the following are true:
- Expression Stack at time t = [ [ ], [ [ Python constructor with name: class_name and arguments: args, ys ], rest ] ]
- Value Stack at time t = [ evaluated, stack ]
- method parameters where the Class Map is (Class Map at time t), class name is class_name, and method name is "__init__" = params
- Parameters List at time t = None
then Expression Stack at time (t + 1) = Expression Stack at time t
if the following are true:
- Expression Stack at time t = [ [ ], [ [ Python constructor with name: class_name and arguments: args, ys ], rest ] ]
- Value Stack at time t = [ evaluated, stack ]
- method parameters where the Class Map is (Class Map at time t), class name is class_name, and method name is "__init__" = params
- Parameters List at time t = None
then Variables Map at time (t + 1) = Variables Map at time t
if the following are true:
- Expression Stack at time t = [ [ ], [ [ Python constructor with name: class_name and arguments: args, ys ], rest ] ]
- Value Stack at time t = [ evaluated, stack ]
- method parameters where the Class Map is (Class Map at time t), class name is class_name, and method name is "__init__" = params
- Parameters List at time t = None
then Control Map at time (t + 1) = Control Map at time t
if the following are true:
- Expression Stack at time t = [ [ ], [ [ Python constructor with name: class_name and arguments: args, ys ], rest ] ]
- Value Stack at time t = [ evaluated, stack ]
- method parameters where the Class Map is (Class Map at time t), class name is class_name, and method name is "__init__" = params
- Parameters List at time t = None
then Python Object Store at time (t + 1) = Python Object Store at time t
if the following are true:
- Expression Stack at time t = [ [ ], [ [ Python constructor with name: class_name and arguments: args, ys ], rest ] ]
- Value Stack at time t = [ evaluated, stack ]
- method parameters where the Class Map is (Class Map at time t), class name is class_name, and method name is "__init__" = params
- Parameters List at time t = None
then Context Stack at time (t + 1) = Context Stack at time t
if the following are true:
- Expression Stack at time t = [ [ ], [ [ Python constructor with name: class_name and arguments: args, ys ], rest ] ]
- Value Stack at time t = [ evaluated, stack ]
- method parameters where the Class Map is (Class Map at time t), class name is class_name, and method name is "__init__" = params
- Parameters List at time t = None
then the line at time (t + 1) = the line at time t
if the following are true:
- Expression Stack at time t = [ [ ], [ [ Python constructor with name: class_name and arguments: args, ys ], rest ] ]
- Value Stack at time t = [ evaluated, stack ]
- method parameters where the Class Map is (Class Map at time t), class name is class_name, and method name is "__init__" = params
- Parameters List at time t = None
then the tab at time (t + 1) = the tab at time t
if the following are true:
- Expression Stack at time t = [ [ ], [ [ Python constructor with name: class_name and arguments: args, ys ], rest ] ]
- 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 Stack at time t = [ [ ], [ [ Python constructor with name: class_name and arguments: args, ys ], rest ] ]
- 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 Stack at time t = [ [ ], [ [ Python constructor with name: class_name and arguments: args, ys ], rest ] ]
- 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 Stack at time t = [ [ ], [ [ Python constructor with name: class_name and arguments: args, ys ], rest ] ]
- 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:
- Parameters List at time t = [ ]
- Expression Stack at time t = [ [ ], [ [ Python constructor with name: class_name and arguments: args, ys ], rest ] ]
- 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:
- Parameters List at time t = [ ]
- Expression Stack at time t = [ [ ], [ [ Python constructor with name: class_name and arguments: args, ys ], rest ] ]
- 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:
- Parameters List at time t = [ ]
- Expression Stack at time t = [ [ ], [ [ Python constructor with name: class_name and arguments: args, ys ], rest ] ]
- 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:
- Return Value at time t = [ r, [ ] ]
- Expression Stack at time t = [ [ ], [ [ Python constructor with name: clss_name and arguments: args, ys ], rest ] ]
- Value Stack at time t = [ next_level, other_levels ]
then Value Stack at time (t + 1) = [ [ r, next_level ], other_levels ]
if the following are true:
- Return Value at time t = [ r, [ ] ]
- Expression Stack at time t = [ [ ], [ [ Python constructor with name: clss_name and arguments: args, ys ], rest ] ]
- Value Stack at time t = [ next_level, other_levels ]
then Expression Stack at time (t + 1) = [ ys, rest ]
if the following are true:
- Return Value at time t = [ r, [ ] ]
- Expression Stack at time t = [ [ ], [ [ Python constructor with name: clss_name and arguments: args, ys ], rest ] ]
- Value Stack at time t = [ next_level, other_levels ]
then Return Value at time (t + 1) = [ ]
if the following are true:
- Return Value at time t = [ r, [ ] ]
- Expression Stack at time t = [ [ ], [ [ Python constructor with name: clss_name and arguments: args, ys ], rest ] ]
- Value Stack at time t = [ next_level, other_levels ]
then Parameters List at time (t + 1) = None
if the following are true:
- Return Value at time t = [ r, [ ] ]
- Expression Stack at time t = [ [ ], [ [ Python constructor with name: clss_name and arguments: args, ys ], rest ] ]
- Value Stack at time t = [ next_level, other_levels ]
then Variables Map at time (t + 1) = Variables Map at time t
if the following are true:
- Return Value at time t = [ r, [ ] ]
- Expression Stack at time t = [ [ ], [ [ Python constructor with name: clss_name and arguments: args, ys ], rest ] ]
- Value Stack at time t = [ next_level, other_levels ]
then Control Map at time (t + 1) = Control Map at time t
if the following are true:
- Return Value at time t = [ r, [ ] ]
- Expression Stack at time t = [ [ ], [ [ Python constructor with name: clss_name and arguments: args, ys ], rest ] ]
- Value Stack at time t = [ next_level, other_levels ]
then Python Object Store at time (t + 1) = Python Object Store at time t
if the following are true:
- Return Value at time t = [ r, [ ] ]
- Expression Stack at time t = [ [ ], [ [ Python constructor with name: clss_name and arguments: args, ys ], rest ] ]
- Value Stack at time t = [ next_level, other_levels ]
then Context Stack at time (t + 1) = Context Stack at time t
if the following are true:
- Return Value at time t = [ r, [ ] ]
- Expression Stack at time t = [ [ ], [ [ Python constructor with name: clss_name and arguments: args, ys ], rest ] ]
- Value Stack at time t = [ next_level, other_levels ]
then the line at time (t + 1) = the line at time t
if the following are true:
- Return Value at time t = [ r, [ ] ]
- Expression Stack at time t = [ [ ], [ [ Python constructor with name: clss_name and arguments: args, ys ], rest ] ]
- Value Stack at time t = [ next_level, other_levels ]
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 constructor with name: class_name and arguments: args)
- Expression Stack at time t = [ [ ], [ ] ]
- Value Stack at time t = [ [ value, [ ] ], [ ] ]
then Variables Map at time (t + 1) = result of storing value 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 constructor with name: class_name and arguments: args)
- Expression Stack at time t = [ [ ], [ ] ]
- Value Stack at time t = [ [ value, [ ] ], [ ] ]
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 constructor with name: class_name and arguments: args)
- Expression Stack at time t = [ [ ], [ ] ]
- Value Stack at time t = [ [ value, [ ] ], [ ] ]
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 constructor with name: class_name and arguments: args)
- Expression Stack at time t = [ [ ], [ ] ]
- Value Stack at time t = [ [ value, [ ] ], [ ] ]
then Context Stack at time (t + 1) = Context 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: class_name and arguments: args)
- Expression Stack at time t = [ [ ], [ ] ]
- Value Stack at time t = [ [ value, [ ] ], [ ] ]
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: class_name and arguments: args)
- Expression Stack at time t = [ [ ], [ ] ]
- Value Stack at time t = [ [ value, [ ] ], [ ] ]
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 (obj.attr)
- Expression Stack at time t = [ ]
then Expression Stack at time (t + 1) = [ [ obj.attr, [ ] ], [ ] ]
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.attr)
- Expression Stack at time t = [ ]
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 (obj.attr)
- Expression Stack at time t = [ ]
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 (obj.attr)
- Expression Stack at time t = [ ]
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 (obj.attr)
- Expression Stack at time t = [ ]
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 (obj.attr)
- Expression Stack at time t = [ ]
then Context Stack at time (t + 1) = Context 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.attr)
- Expression Stack at time t = [ ]
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.attr)
- Expression Stack at time t = [ ]
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 (obj.attr)
- Expression Stack at time t = [ [ ], [ ] ]
- Value Stack at time t = [ [ value, [ ] ], [ ] ]
then Variables Map at time (t + 1) = result of storing value 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.attr)
- Expression Stack at time t = [ [ ], [ ] ]
- Value Stack at time t = [ [ value, [ ] ], [ ] ]
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.attr)
- Expression Stack at time t = [ [ ], [ ] ]
- Value Stack at time t = [ [ value, [ ] ], [ ] ]
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.attr)
- Expression Stack at time t = [ [ ], [ ] ]
- Value Stack at time t = [ [ value, [ ] ], [ ] ]
then Context Stack at time (t + 1) = Context 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.attr)
- Expression Stack at time t = [ [ ], [ ] ]
- Value Stack at time t = [ [ value, [ ] ], [ ] ]
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.attr)
- Expression Stack at time t = [ [ ], [ ] ]
- Value Stack at time t = [ [ value, [ ] ], [ ] ]
then Control Map at time (t + 1) = Control Map at time t
if Expression Stack at time t = [ [ obj.attr, ys ], rest ], then Value Stack at time (t + 1) = [ [ ], Value Stack at time t ]
if Expression Stack at time t = [ [ obj.attr, ys ], rest ], then Expression Stack at time (t + 1) = [ [ obj, [ ] ], [ [ obj.attr, ys ], rest ] ]
if Expression Stack at time t = [ [ obj.attr, ys ], rest ], then Parameters List at time (t + 1) = None
if Expression Stack at time t = [ [ obj.attr, ys ], rest ], then the line at time (t + 1) = the line at time t
if Expression Stack at time t = [ [ obj.attr, ys ], rest ], then the tab at time (t + 1) = the tab at time t
if Expression Stack at time t = [ [ obj.attr, ys ], rest ], then Variables Map at time (t + 1) = Variables Map at time t
if Expression Stack at time t = [ [ obj.attr, ys ], rest ], then Control Map at time (t + 1) = Control Map at time t
if Expression Stack at time t = [ [ obj.attr, ys ], rest ], then Python Object Store at time (t + 1) = Python Object Store at time t
if Expression Stack at time t = [ [ obj.attr, ys ], rest ], then Context Stack at time (t + 1) = Context Stack at time t
if the following are true:
- Expression Stack at time t = [ [ ], [ [ obj.attr, ys ], rest ] ]
- Value Stack at time t = [ [ Python reference index, [ ] ], [ next_level, other_levels ] ]
- the element at index index of stack (Python Object Store at time t) = Python object: attributes
then Value Stack at time (t + 1) = [ [ value at attr in map attributes, next_level ], other_levels ]
if Expression Stack at time t = [ [ ], [ [ obj.attr, ys ], rest ] ], then Expression Stack at time (t + 1) = [ ys, rest ]
if Expression Stack at time t = [ [ ], [ [ obj.attr, ys ], rest ] ], then the line at time (t + 1) = the line at time t
if Expression Stack at time t = [ [ ], [ [ obj.attr, ys ], rest ] ], then the tab at time (t + 1) = the tab at time t
if Expression Stack at time t = [ [ ], [ [ obj.attr, ys ], rest ] ], then Variables Map at time (t + 1) = Variables Map at time t
if Expression Stack at time t = [ [ ], [ [ obj.attr, ys ], rest ] ], then Control Map at time (t + 1) = Control Map at time t
if Expression Stack at time t = [ [ ], [ [ obj.attr, ys ], rest ] ], then Python Object Store at time (t + 1) = Python Object Store at time t
if Expression Stack at time t = [ [ ], [ [ obj.attr, ys ], rest ] ], then Context Stack at time (t + 1) = Context 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.key = value
- Expression Stack at time t = [ ]
then Expression Stack at time (t + 1) = [ [ obj.key = value, [ ] ], [ ] ]
if the following are true:
- the line at time t = i
- the tab at time t = j
- statement at line i, tab j = obj.key = value
- Expression Stack at time t = [ ]
then Value Stack at time (t + 1) = [ [ ], [ ] ]