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 state at time t = "call_build_args"
- Parameters List at time t = [ var, frest ]
then the line at time (t + 1) = the line at time t
- expression state at time t = "call_build_args"
- Parameters List at time t = [ var, frest ]
then the tab at time (t + 1) = the tab at time t
- expression state at time t = "call_build_args"
- 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)
- expression state at time t = "call_build_args"
- Parameters List at time t = [ var, frest ]
- Argument Values at time t = [ value, vrest ]
then Parameters List at time (t + 1) = frest
- expression state at time t = "call_build_args"
- Parameters List at time t = [ var, frest ]
- Argument Values at time t = [ value, vrest ]
then Argument Values at time (t + 1) = vrest
- expression state at time t = "call_build_args"
- Parameters List at time t = [ var, frest ]
- Argument Values at time t = [ value, vrest ]
then expression state at time (t + 1) = "call_build_args"
- expression state at time t = "call_build_args"
- Parameters List at time t = [ var, frest ]
- Argument Values at time t = [ value, vrest ]
then Variables Map at time (t + 1) = Variables Map at time t
- expression state at time t = "call_build_args"
- Parameters List at time t = [ var, frest ]
- Argument Values at time t = [ value, vrest ]
then stack at time (t + 1) = stack at time t
- expression state at time t = "call_build_args"
- 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
- expression state at time t = "call_build_args"
- Parameters List at time t = [ var, frest ]
- Argument Values at time t = [ value, vrest ]
then Control Map at time (t + 1) = Control Map at time t
- expression state at time t = "call_build_args"
- Parameters List at time t = [ ]
then expression state at time (t + 1) = "not_expr"
- expression state at time t = "call_build_args"
- Parameters List at time t = [ ]
then Python Object Store at time (t + 1) = Python Object Store at time t
- expression state at time t = "call_build_args"
- Parameters List at time t = [ ]
then Variables Map at time (t + 1) = Function Variables Map at time t
- expression state at time t = "call_build_args"
- Parameters List at time t = [ ]
then the tab at time (t + 1) = 1
- expression state at time t = "call_build_args"
- Parameters List at time t = [ ]
then stack at time (t + 1) = [ program context with variables: (Variables Map at time t) and expression state: (expression state with parent stack: (parent stack at time t) arguments: (arguments stack at time t) values: (Value Stack at time t) line: (the line at time t) tab: (the tab at time t)) and control map: (Control Map at time t), stack at time t ]
- expression state at time t = "call_build_args"
- Parameters List at time t = [ ]
- the expression at time t = function call with name: name and arguments: args
- there is a function named name with parameters params at line line
then the line at time (t + 1) = line + 1
- expression state at time t = "call_build_args"
- Parameters List at time t = [ ]
- the expression at time t = function call with name: name and arguments: args
- there is a function named name with parameters params at line line
then Control Map at time (t + 1) = [ entry 0: (pair ("function", name)), [ ] ]
- expression state at time t = "call_returned"
- parent stack at time t = [ ]
then expression state at time (t + 1) = "end_expr"
- expression state at time t = "call_returned"
- parent stack at time t = [ x, y ]
then expression state at time (t + 1) = "return"
- expression state at time t = "return"
- Value Stack at time t = [ v, w ]
- Return Value at time t = r
then Value Stack at time (t + 1) = [ [ r, v ], w ]
- 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 (function call with name: 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)
- 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 (function call with name: name and arguments: args)
- expression state at time t = "end_expr"
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 = assign statement with target x and expression (function call with name: name and arguments: args)
- expression state at time t = "end_expr"
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 = assign statement with target x and expression (function call with name: name and arguments: args)
- expression state at time t = "end_expr"
then stack at time (t + 1) = 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 (function call with name: name and arguments: args)
- expression state at time t = "end_expr"
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 = assign statement with target x and expression (function call with name: name and arguments: args)
- expression state at time t = "end_expr"
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 test:
- expression state at time t = "not_expr"
then the expression at time (t + 1) = test
- the line at time t = i
- the tab at time t = j
- statement at line i, tab j =
if test:
- expression state at time t = "not_expr"
then expression state at time (t + 1) = "begin_expr"
- the line at time t = i
- the tab at time t = j
- statement at line i, tab j =
if test:
- expression state at time t = "not_expr"
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 test:
- expression state at time t = "not_expr"
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 test:
- expression state at time t = "not_expr"
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 test:
- expression state at time t = "not_expr"
then parent stack at time (t + 1) = [ ]
- the line at time t = i
- the tab at time t = j
- statement at line i, tab j =
if test:
- expression state at time t = "not_expr"
then arguments stack at time (t + 1) = [ ]
- the line at time t = i
- the tab at time t = j
- statement at line i, tab j =
if test:
- expression state at time t = "not_expr"
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:
- expression state at time t = "not_expr"
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 test:
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 test:
then stack at time (t + 1) = stack at time t
- the line at time t = i
- the tab at time t = j
- statement at line i, tab j =
if test:
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 =
if test:
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 =
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 =
if test:
- expression state at time t = "end_expr"
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:
- expression state at time t = "end_expr"
- Return Value 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 test:
- expression state at time t = "end_expr"
- Return Value 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 test:
- expression state at time t = "end_expr"
- Return Value 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 test:
- expression state at time t = "end_expr"
- Return Value at time t = True
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 test:
- expression state at time t = "end_expr"
- Return Value 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 test:
- expression state at time t = "end_expr"
- Return Value 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 test:
- expression state at time t = "end_expr"
- Return Value 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 test:
- expression state at time t = "end_expr"
- Return Value at time t = False
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 state at time t = "not_expr"
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 state at time t = "not_expr"
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 state at time t = "not_expr"
then the expression at time (t + 1) = test
- 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 state at time t = "not_expr"
then expression state at time (t + 1) = "begin_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 state at time t = "not_expr"
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 state at time t = "not_expr"
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 state at time t = "not_expr"
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 state at time t = "not_expr"
then parent 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 state at time t = "not_expr"
then arguments 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", True)
- expression state at time t = "not_expr"
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 state at time t = "not_expr"
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:
- expression state at time t = "end_expr"
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 state at time t = "end_expr"
- Return Value 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 test:
- expression state at time t = "end_expr"
- Return Value 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 test:
- expression state at time t = "end_expr"
- Return Value 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 test:
- expression state at time t = "end_expr"
- Return Value at time t = True
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 state at time t = "end_expr"
- Return Value 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 test:
- expression state at time t = "end_expr"
- Return Value 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 test:
- expression state at time t = "end_expr"
- Return Value 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:
- expression state at time t = "end_expr"
- Return Value at time t = False
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:
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:
then stack at time (t + 1) = stack at time t
- the line at time t = i
- the tab at time t = j
- statement at line i, tab j =
elif test:
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 =
elif test:
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 =
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