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.
- Parameters List at time t = [ var, frest ]
- Argument Values at time t = [ value, vrest ]
then Parameters List at time (t + 1) = frest
- Parameters List at time t = [ var, frest ]
- Argument Values at time t = [ value, vrest ]
then Argument Values at time (t + 1) = vrest
- Parameters List at time t = [ var, frest ]
- Argument Values at time t = [ value, vrest ]
then Python Object Store at time (t + 1) = Python Object Store at time t
- Parameters List at time t = [ ]
- Expression Stack at time t = [ [ ], [ [ function call with name: name and arguments: args, ys ], rest ] ]
- there is a function named name with parameters params at line line
then the line at time (t + 1) = line + 1
- Parameters List at time t = [ ]
- Expression Stack at time t = [ [ ], [ [ function call with name: name and arguments: args, ys ], rest ] ]
- there is a function named name with parameters params at line line
then Control Map at time (t + 1) = [ entry 0: (pair ("function", name)), [ ] ]
- Return Value at time t = [ r, [ ] ]
- Expression Stack at time t = [ [ ], [ [ function call with name: 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 ]
- Return Value at time t = [ r, [ ] ]
- Expression Stack at time t = [ [ ], [ [ function call with name: name and arguments: 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 = [ [ ], [ [ function call with name: name and arguments: 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 = [ [ ], [ [ function call with name: name and arguments: 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 = [ [ ], [ [ function call with name: 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
- Return Value at time t = [ r, [ ] ]
- Expression Stack at time t = [ [ ], [ [ function call with name: 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
- Return Value at time t = [ r, [ ] ]
- Expression Stack at time t = [ [ ], [ [ function call with name: 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
- Return Value at time t = [ r, [ ] ]
- Expression Stack at time t = [ [ ], [ [ function call with name: 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
- Return Value at time t = [ r, [ ] ]
- Expression Stack at time t = [ [ ], [ [ function call with name: 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
- Return Value at time t = [ r, [ ] ]
- Expression Stack at time t = [ [ ], [ [ function call with name: 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
- the line at time t = i
- the tab at time t = j
- statement at line i, tab j =
target = expr
- Expression Stack at time t = [ ]
then Expression Stack at time (t + 1) = [ [ expr, [ ] ], [ ] ]
- the line at time t = i
- the tab at time t = j
- statement at line i, tab j =
target = expr
- 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 =
target = expr
- 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 =
target = expr
- 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 =
target = expr
- 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 =
target = expr
- 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 =
target = expr
- 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 =
target = expr
- 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 =
target = expr
- Expression Stack at time t = [ [ ], [ ] ]
- Value Stack at time t = [ [ value, [ ] ], [ ] ]
then Variables Map at time (t + 1) = result of storing value at key: target in map: (Variables Map at time t)
- the line at time t = i
- the tab at time t = j
- statement at line i, tab j =
target = expr
- Expression Stack at time t = [ [ ], [ ] ]
- Value Stack at time t = [ [ value, [ ] ], [ ] ]
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 =
target = expr
- Expression Stack at time t = [ [ ], [ ] ]
- Value Stack at time t = [ [ value, [ ] ], [ ] ]
then the tab at time (t + 1) = the tab at time t
- the line at time t = i
- the tab at time t = j
- statement at line i, tab j =
target = expr
- Expression Stack at time t = [ [ ], [ ] ]
- Value Stack at time t = [ [ value, [ ] ], [ ] ]
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 =
target = expr
- 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
- the line at time t = i
- the tab at time t = j
- statement at line i, tab j =
target = expr
- Expression Stack at time t = [ [ ], [ ] ]
- Value Stack at time t = [ [ value, [ ] ], [ ] ]
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 =
target = expr
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 =
if expr:
- Expression Stack at time t = [ ]
then Expression Stack at time (t + 1) = [ [ expr, [ ] ], [ ] ]
- the line at time t = i
- the tab at time t = j
- statement at line i, tab j =
if expr:
- 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 =
if expr:
- 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 =
if expr:
- 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 =
if expr:
- 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 =
if expr:
- 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 =
if expr:
- 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 =
if expr:
- 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 =
if expr:
- Expression Stack at time t = [ [ ], [ ] ]
- Value Stack at time t = [ [ True, [ ] ], [ ] ]
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 =
if expr:
- Expression Stack at time t = [ [ ], [ ] ]
- Value Stack at time t = [ [ True, [ ] ], [ ] ]
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 =
if expr:
- Expression Stack at time t = [ [ ], [ ] ]
- Value Stack at time t = [ [ True, [ ] ], [ ] ]
then Control Map at time (t + 1) = result of storing (pair ("if", True)) 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 =
if expr:
- Expression Stack at time t = [ [ ], [ ] ]
- Value Stack at time t = [ [ False, [ ] ], [ ] ]
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 =
if expr:
- Expression Stack at time t = [ [ ], [ ] ]
- Value Stack at time t = [ [ False, [ ] ], [ ] ]
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 =
if expr:
- Expression Stack at time t = [ [ ], [ ] ]
- Value Stack at time t = [ [ False, [ ] ], [ ] ]
then Control Map at time (t + 1) = result of storing (pair ("if", False)) 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 =
if expr:
- 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 =
if expr:
- 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 =
if expr:
- 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 =
if expr:
- 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 =
if test:
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 =
elif test:
- 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 =
elif test:
- 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 =
elif test:
- 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 =
elif test:
- 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 =
elif test:
- value at j in map (Control Map at time t) = pair ("if", False)
- Expression Stack at time t = [ ]
then Expression Stack at time (t + 1) = [ [ expr, [ ] ], [ ] ]
- the line at time t = i
- the tab at time t = j
- statement at line i, tab j =
elif test:
- value at j in map (Control Map at time t) = pair ("if", False)
- 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 =
elif test:
- value at j in map (Control Map at time t) = pair ("if", False)
- 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 =
elif test:
- value at j in map (Control Map at time t) = pair ("if", False)
- 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 =
elif test:
- value at j in map (Control Map at time t) = pair ("if", False)
- 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 =
elif test:
- value at j in map (Control Map at time t) = pair ("if", False)
- 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 =
elif test:
- value at j in map (Control Map at time t) = pair ("if", False)
- 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 =
elif test:
- value at j in map (Control Map at time t) = pair ("if", False)
- 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 =
elif test:
- value at j in map (Control Map at time t) = pair ("if", True)
- Expression Stack at time t = [ ]
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 =
elif test:
- value at j in map (Control Map at time t) = pair ("if", True)
- 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 =
elif test:
- value at j in map (Control Map at time t) = pair ("if", True)
- 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 =
elif test:
- value at j in map (Control Map at time t) = pair ("if", True)
- 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 =
elif test:
- value at j in map (Control Map at time t) = pair ("if", True)
- 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 =
elif test:
- value at j in map (Control Map at time t) = pair ("if", True)
- 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 =
elif test:
- 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 =
elif test:
- 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 =
elif test:
- 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 =
elif expr:
- Expression Stack at time t = [ [ ], [ ] ]
- Value Stack at time t = [ [ True, [ ] ], [ ] ]
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 =
elif expr:
- Expression Stack at time t = [ [ ], [ ] ]
- Value Stack at time t = [ [ True, [ ] ], [ ] ]
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 =
elif expr:
- Expression Stack at time t = [ [ ], [ ] ]
- Value Stack at time t = [ [ True, [ ] ], [ ] ]
then Control Map at time (t + 1) = result of storing (pair ("if", True)) 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 =
elif expr:
- Expression Stack at time t = [ [ ], [ ] ]
- Value Stack at time t = [ [ False, [ ] ], [ ] ]
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 =
elif expr:
- Expression Stack at time t = [ [ ], [ ] ]
- Value Stack at time t = [ [ False, [ ] ], [ ] ]
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 =
elif expr:
- Expression Stack at time t = [ [ ], [ ] ]
- Value Stack at time t = [ [ False, [ ] ], [ ] ]
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 =
elif test:
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 =
else:
- value at j in map (Control Map at time t) = pair ("if", False)
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 =
else:
- value at j in map (Control Map at time t) = pair ("if", False)
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 =
else:
- value at j in map (Control Map at time t) = pair ("if", True)
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 =
else:
- value at j in map (Control Map at time t) = pair ("if", True)
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 =
else:
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 =
else:
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 =
else:
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 =
else:
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 =
else:
then Class Map at time (t + 1) = Class Map at time t