Conditional Properties
In each statement, if the test expression is true, then the conclusion expression is also assumed to be true. Conditional properties are used to prove theorems.
- the line at time t = i
- the tab at time t = j
- statement at line i, tab j = c
- c is constant
- 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 = c
- c is constant
- 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 = c
- c is constant
- 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 = x
- x is a variable
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 = x
- x is a variable
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 = x
- x is a variable
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 = x
- x is a variable
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 = x
- x is a variable
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 = x
- c is a variable
- Expression Stack at time t = [ ]
then Expression Stack at time (t + 1) = [ [ x, [ ] ], [ ] ]
- the line at time t = i
- the tab at time t = j
- statement at line i, tab j = x
- c is a variable
- 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 = x
- c is a variable
- 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 = x
- c is a variable
- 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 = function call with name: name and arguments: args
then Class Map at time (t + 1) = Class Map at time t
- the line at time t = i
- the tab at time t = j
- statement at line i, tab j = function call with name: name and arguments: args
- Expression Stack at time t = [ ]
then Expression Stack at time (t + 1) = [ [ function call with name: name and arguments: args, [ ] ], [ ] ]
- the line at time t = i
- the tab at time t = j
- statement at line i, tab j = function call with name: name and arguments: args
- 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 = function call with name: name and arguments: args
- 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 = function call with name: name and arguments: args
- 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 = function call with name: name and arguments: args
- 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 = function call with name: name and arguments: args
- Expression Stack at time t = [ ]
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 = function call 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
- the line at time t = i
- the tab at time t = j
- statement at line i, tab j = function call with name: name and arguments: args
- Expression Stack at time t = [ ]
then Context Stack at time (t + 1) = Context Stack at time t
- Expression Stack at time t = [ [ x, ys ], rest ]
- Value Stack at time t = [ values, v_rest ]
- x is constant
then Expression Stack at time (t + 1) = [ ys, rest ]
- Expression Stack at time t = [ [ x, ys ], rest ]
- Value Stack at time t = [ values, v_rest ]
- x is constant
then Value Stack at time (t + 1) = [ [ x, values ], v_rest ]
- Expression Stack at time t = [ [ x, ys ], rest ]
- Value Stack at time t = [ values, v_rest ]
- x is constant
then Parameters List at time (t + 1) = None
- Expression Stack at time t = [ [ x, ys ], rest ]
- Value Stack at time t = [ values, v_rest ]
- x is constant
then the line at time (t + 1) = the line at time t
- Expression Stack at time t = [ [ x, ys ], rest ]
- Value Stack at time t = [ values, v_rest ]
- x is constant
then the tab at time (t + 1) = the tab at time t
- Expression Stack at time t = [ [ x, ys ], rest ]
- Value Stack at time t = [ values, v_rest ]
- x is constant
then Variables Map at time (t + 1) = Variables Map at time t
- Expression Stack at time t = [ [ x, ys ], rest ]
- Value Stack at time t = [ values, v_rest ]
- x is constant
then Control Map at time (t + 1) = Control Map at time t
- Expression Stack at time t = [ [ x, ys ], rest ]
- Value Stack at time t = [ values, v_rest ]
- x is constant
then Python Object Store at time (t + 1) = Python Object Store at time t
- Expression Stack at time t = [ [ x, ys ], rest ]
- Value Stack at time t = [ values, v_rest ]
- x is constant
then Context Stack at time (t + 1) = Context Stack at time t
- Expression Stack at time t = [ [ x, ys ], rest ]
- Value Stack at time t = [ values, v_rest ]
- x is a variable
then Expression Stack at time (t + 1) = [ ys, rest ]
- Expression Stack at time t = [ [ x, ys ], rest ]
- Value Stack at time t = [ values, v_rest ]
- x is a variable
then Value Stack at time (t + 1) = [ [ value at x in map (Variables Map at time t), values ], v_rest ]
- Expression Stack at time t = [ [ x, ys ], rest ]
- Value Stack at time t = [ values, v_rest ]
- x is a variable
then Parameters List at time (t + 1) = None
- Expression Stack at time t = [ [ x, ys ], rest ]
- Value Stack at time t = [ values, v_rest ]
- x is a variable
then the line at time (t + 1) = the line at time t
- Expression Stack at time t = [ [ x, ys ], rest ]
- Value Stack at time t = [ values, v_rest ]
- x is a variable
then the tab at time (t + 1) = the tab at time t
- Expression Stack at time t = [ [ x, ys ], rest ]
- Value Stack at time t = [ values, v_rest ]
- x is a variable
then Variables Map at time (t + 1) = Variables Map at time t
- Expression Stack at time t = [ [ x, ys ], rest ]
- Value Stack at time t = [ values, v_rest ]
- x is a variable
then Control Map at time (t + 1) = Control Map at time t
- Expression Stack at time t = [ [ x, ys ], rest ]
- Value Stack at time t = [ values, v_rest ]
- x is a variable
then Python Object Store at time (t + 1) = Python Object Store at time t
- Expression Stack at time t = [ [ x, ys ], rest ]
- Value Stack at time t = [ values, v_rest ]
- x is a variable
then Context Stack at time (t + 1) = Context Stack at time t
- Expression Stack at time t = [ [ ], [ [ function call with name: "__add__" and arguments: args, ys ], rest ] ]
- Value Stack at time t = [ [ a, [ b, [ ] ] ], [ next_level, other_levels ] ]
then Value Stack at time (t + 1) = [ [ b + a, next_level ], other_levels ]
- Expression Stack at time t = [ [ ], [ [ function call with name: "__mul__" and arguments: args, ys ], rest ] ]
- Value Stack at time t = [ [ a, [ b, [ ] ] ], [ next_level, other_levels ] ]
then Value Stack at time (t + 1) = [ [ b ⋅ a, next_level ], other_levels ]
- Expression Stack at time t = [ [ ], [ [ function call with name: "__eq__" and arguments: args, ys ], rest ] ]
- Value Stack at time t = [ [ a, [ b, [ ] ] ], [ next_level, other_levels ] ]
then Value Stack at time (t + 1) = [ [ b = a, next_level ], other_levels ]
- Expression Stack at time t = [ [ ], [ [ function call with name: "__lt__" and arguments: args, ys ], rest ] ]
- Value Stack at time t = [ [ a, [ b, [ ] ] ], [ next_level, other_levels ] ]
then Value Stack at time (t + 1) = [ [ b < a, next_level ], other_levels ]
- Expression Stack at time t = [ [ ], [ [ function call with name: "__gt__" and arguments: args, ys ], rest ] ]
- Value Stack at time t = [ [ a, [ b, [ ] ] ], [ next_level, other_levels ] ]
then Value Stack at time (t + 1) = [ [ b > a, next_level ], other_levels ]
- Expression Stack at time t = [ [ ], [ [ function call with name: name and arguments: args, ys ], rest ] ]
- Value Stack at time t = [ values, v_rest ]
- there is a function named name with parameters params at line line
- Parameters List at time t = None
then Parameters List at time (t + 1) = params
- Expression Stack at time t = [ [ ], [ [ function call with name: name and arguments: args, ys ], rest ] ]
- Value Stack at time t = [ values, v_rest ]
- there is a function named name with parameters params at line line
- Parameters List at time t = None
then Argument Values at time (t + 1) = reverse of values
- Expression Stack at time t = [ [ ], [ [ function call with name: name and arguments: args, ys ], rest ] ]
- Value Stack at time t = [ values, v_rest ]
- there is a function named name with parameters params at line line
- Parameters List at time t = None
then Function Variables Map at time (t + 1) = [ ]
- Expression Stack at time t = [ [ ], [ [ function call with name: name and arguments: args, ys ], rest ] ]
- Value Stack at time t = [ values, v_rest ]
- there is a function named name with parameters params at line line
- Parameters List at time t = None
then Value Stack at time (t + 1) = v_rest
- Expression Stack at time t = [ [ ], [ [ function call with name: name and arguments: args, ys ], rest ] ]
- Value Stack at time t = [ values, v_rest ]
- there is a function named name with parameters params at line line
- Parameters List at time t = None
then Expression Stack at time (t + 1) = Expression Stack at time t
- Expression Stack at time t = [ [ ], [ [ function call with name: name and arguments: args, ys ], rest ] ]
- Value Stack at time t = [ values, v_rest ]
- there is a function named name with parameters params at line line
- Parameters List at time t = None
then Variables Map at time (t + 1) = Variables Map at time t
- Expression Stack at time t = [ [ ], [ [ function call with name: name and arguments: args, ys ], rest ] ]
- Value Stack at time t = [ values, v_rest ]
- there is a function named name with parameters params at line line
- Parameters List at time t = None
then Control Map at time (t + 1) = Control Map at time t
- Expression Stack at time t = [ [ ], [ [ function call with name: name and arguments: args, ys ], rest ] ]
- Value Stack at time t = [ values, v_rest ]
- there is a function named name with parameters params at line line
- Parameters List at time t = None
then Python Object Store at time (t + 1) = Python Object Store at time t
- Expression Stack at time t = [ [ ], [ [ function call with name: name and arguments: args, ys ], rest ] ]
- Value Stack at time t = [ values, v_rest ]
- there is a function named name with parameters params at line line
- Parameters List at time t = None
then Context Stack at time (t + 1) = Context Stack at time t
- Expression Stack at time t = [ [ ], [ [ function call with name: name and arguments: args, ys ], rest ] ]
- Value Stack at time t = [ values, v_rest ]
- there is a function named name with parameters params at line line
- Parameters List at time t = None
then the line at time (t + 1) = the line at time t
- Expression Stack at time t = [ [ ], [ [ function call with name: name and arguments: args, ys ], rest ] ]
- Value Stack at time t = [ values, v_rest ]
- there is a function named name with parameters params at line line
- Parameters List at time t = None
then the tab at time (t + 1) = the tab at time t
- Parameters List at time t = [ var, frest ]
- Argument Values at time t = [ value, vrest ]
then Function Variables Map at time (t + 1) = result of storing value at key: var in map: (Function Variables Map at time t)