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 =
x = c
- c is constant
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 =
x = c
- c is constant
then expression state at time (t + 1) = "not_expr"
- the line at time t = i
- the tab at time t = j
- statement at line i, tab j =
x = c
- c is constant
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
- c is a variable
then Variables Map at time (t + 1) = result of storing (value at c in map (Variables Map 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 =
x = c
- c is a variable
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 =
x = c
- c is a variable
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 =
x = c
- c is a variable
then expression state at time (t + 1) = "not_expr"
- the line at time t = i
- the tab at time t = j
- statement at line i, tab j =
x = c
- c 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 = c
- c 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 = assign statement with target x and expression (function call with name: name and arguments: args)
- expression state at time t = "not_expr"
then the expression 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 = assign statement with target x and expression (function call with name: name and arguments: args)
- 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 = assign statement with target x and expression (function call with name: name and arguments: args)
- 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 = assign statement with target x and expression (function call with name: name and arguments: args)
- 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 = assign statement with target x and expression (function call with name: name and arguments: args)
- expression state at time t = "not_expr"
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 (function call with name: name and arguments: args)
- expression state at time t = "not_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 = "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 = assign statement with target x and expression (function call with name: name and arguments: args)
- 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 = assign statement with target x and expression (function call with name: name and arguments: args)
- 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 = assign statement with target x and expression (function call with name: name and arguments: args)
- 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 = assign statement with target x and expression (function call with name: name and arguments: args)
- expression state at time t = "not_expr"
then Python Object Store at time (t + 1) = Python Object Store at time t
- expression state at time t = "begin_expr"
- the expression at time t = c
- c is constant
- parent stack at time t = [ x, y ]
then expression state at time (t + 1) = "return"
- expression state at time t = "begin_expr"
- the expression at time t = c
- c is constant
- parent stack at time t = [ ]
then expression state at time (t + 1) = "end_expr"
- expression state at time t = "begin_expr"
- the expression at time t = c
- c is constant
then Return Value at time (t + 1) = c
- expression state at time t = "begin_expr"
- the expression at time t = c
- c is constant
then Value Stack at time (t + 1) = Value Stack at time t
- expression state at time t = "begin_expr"
- the expression at time t = c
- c is constant
then arguments stack at time (t + 1) = arguments stack at time t
- expression state at time t = "begin_expr"
- the expression at time t = c
- c is constant
then parent stack at time (t + 1) = parent stack at time t
- expression state at time t = "begin_expr"
- the expression at time t = x
- x is a variable
- parent stack at time t = [ y, z ]
then expression state at time (t + 1) = "return"
- expression state at time t = "begin_expr"
- the expression at time t = v
- v is a variable
- parent stack at time t = [ ]
then expression state at time (t + 1) = "end_expr"
- expression state at time t = "begin_expr"
- the expression at time t = v
- v is a variable
then Return Value at time (t + 1) = value at x in map (Variables Map at time t)
- expression state at time t = "begin_expr"
- the expression at time t = v
- v is a variable
then Value Stack at time (t + 1) = Value Stack at time t
- expression state at time t = "begin_expr"
- the expression at time t = v
- v is a variable
then arguments stack at time (t + 1) = arguments stack at time t
- expression state at time t = "begin_expr"
- the expression at time t = v
- v is a variable
then parent stack at time (t + 1) = parent stack at time t
- expression state at time t = "begin_expr"
- the expression at time t = function call with name: name and arguments: args
then Value Stack at time (t + 1) = [ [ ], Value Stack at time t ]
- expression state at time t = "begin_expr"
- the expression at time t = function call with name: name and arguments: args
then parent stack at time (t + 1) = [ function call with name: name and arguments: args, parent stack at time t ]
- expression state at time t = "begin_expr"
- the expression at time t = function call with name: name and arguments: args
then arguments stack at time (t + 1) = [ args, arguments stack at time t ]
- expression state at time t = "begin_expr"
- the expression at time t = function call with name: name and arguments: args
then expression state at time (t + 1) = "iterate_args"
- expression state at time t = "iterate_args"
- arguments stack at time t = [ [ x, y ], z ]
then the expression at time (t + 1) = x
- expression state at time t = "iterate_args"
- arguments stack at time t = [ [ x, y ], z ]
then arguments stack at time (t + 1) = [ y, z ]
- expression state at time t = "iterate_args"
- arguments stack at time t = [ [ x, y ], z ]
then expression state at time (t + 1) = "begin_expr"
- expression state at time t = "iterate_args"
- arguments stack at time t = [ [ x, y ], z ]
then parent stack at time (t + 1) = parent stack at time t
- expression state at time t = "iterate_args"
- arguments stack at time t = [ [ ], z ]
- parent stack at time t = [ x, y ]
then the expression at time (t + 1) = x
- expression state at time t = "iterate_args"
- arguments stack at time t = [ [ ], z ]
- parent stack at time t = [ x, y ]
then expression state at time (t + 1) = "call_function_begin"
- expression state at time t = "iterate_args"
- arguments stack at time t = [ [ ], z ]
- parent stack at time t = [ x, y ]
then parent stack at time (t + 1) = y
- expression state at time t = "iterate_args"
- arguments stack at time t = [ [ ], z ]
- parent stack at time t = [ x, y ]
then arguments stack at time (t + 1) = z
- expression state at time t = "call_function_begin"
- Value Stack at time t = [ [ a, [ b, [ ] ] ], stack ]
- the expression at time t = function call with name: "__add__" and arguments: args
then Return Value at time (t + 1) = b + a
- expression state at time t = "call_function_begin"
- parent stack at time t = [ x, y ]
- the expression at time t = function call with name: "__add__" and arguments: args
then expression state at time (t + 1) = "return"
- expression state at time t = "call_function_begin"
- parent stack at time t = [ ]
- the expression at time t = function call with name: "__add__" and arguments: args
then expression state at time (t + 1) = "end_expr"
- expression state at time t = "call_function_begin"
- the expression at time t = function call with name: "__add__" and arguments: args
then Python Object Store at time (t + 1) = Python Object Store at time t
- expression state at time t = "call_function_begin"
- Value Stack at time t = [ [ a, [ b, [ ] ] ], stack ]
- the expression at time t = function call with name: "__mul__" and arguments: args
then Return Value at time (t + 1) = b ⋅ a
- expression state at time t = "call_function_begin"
- parent stack at time t = [ x, y ]
- the expression at time t = function call with name: "__mul__" and arguments: args
then expression state at time (t + 1) = "return"
- expression state at time t = "call_function_begin"
- parent stack at time t = [ ]
- the expression at time t = function call with name: "__mul__" and arguments: args
then expression state at time (t + 1) = "end_expr"
- expression state at time t = "call_function_begin"
- the expression at time t = function call with name: "__mul__" and arguments: args
then Python Object Store at time (t + 1) = Python Object Store at time t
- expression state at time t = "call_function_begin"
- Value Stack at time t = [ [ a, [ b, [ ] ] ], stack ]
- the expression at time t = function call with name: "__eq__" and arguments: args
then Return Value at time (t + 1) = b = a
- expression state at time t = "call_function_begin"
- parent stack at time t = [ x, y ]
- the expression at time t = function call with name: "__eq__" and arguments: args
then expression state at time (t + 1) = "return"
- expression state at time t = "call_function_begin"
- parent stack at time t = [ ]
- the expression at time t = function call with name: "__eq__" and arguments: args
then expression state at time (t + 1) = "end_expr"
- expression state at time t = "call_function_begin"
- the expression at time t = function call with name: "__eq__" and arguments: args
then Python Object Store at time (t + 1) = Python Object Store at time t
- expression state at time t = "call_function_begin"
- Value Stack at time t = [ [ a, [ b, [ ] ] ], stack ]
- the expression at time t = function call with name: "__gt__" and arguments: args
then Return Value at time (t + 1) = b > a
- expression state at time t = "call_function_begin"
- parent stack at time t = [ x, y ]
- the expression at time t = function call with name: "__gt__" and arguments: args
then expression state at time (t + 1) = "return"
- expression state at time t = "call_function_begin"
- parent stack at time t = [ ]
- the expression at time t = function call with name: "__gt__" and arguments: args
then expression state at time (t + 1) = "end_expr"
- expression state at time t = "call_function_begin"
- the expression at time t = function call with name: "__gt__" and arguments: args
then Python Object Store at time (t + 1) = Python Object Store at time t
- expression state at time t = "call_function_begin"
- Value Stack at time t = [ [ a, [ b, [ ] ] ], stack ]
- the expression at time t = function call with name: "__lt__" and arguments: args
then Return Value at time (t + 1) = b < a
- expression state at time t = "call_function_begin"
- parent stack at time t = [ x, y ]
- the expression at time t = function call with name: "__lt__" and arguments: args
then expression state at time (t + 1) = "return"
- expression state at time t = "call_function_begin"
- parent stack at time t = [ ]
- the expression at time t = function call with name: "__lt__" and arguments: args
then expression state at time (t + 1) = "end_expr"
- expression state at time t = "call_function_begin"
- the expression at time t = function call with name: "__lt__" and arguments: args
then Python Object Store at time (t + 1) = Python Object Store at time t
- expression state at time t = "call_function_begin"
- Value Stack at time t = [ values, stack ]
- the expression at time t = function call with name: name and arguments: args
then Argument Values at time (t + 1) = reverse of values
- expression state at time t = "call_function_begin"
- Value Stack at time t = [ values, stack ]
- the expression at time t = function call with name: name and arguments: args
then Value Stack at time (t + 1) = stack
- expression state at time t = "call_function_begin"
- Value Stack at time t = [ values, stack ]
- the expression at time t = function call with name: name and arguments: args
then expression state at time (t + 1) = "call_build_args"
- expression state at time t = "call_function_begin"
- 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 Parameters List at time (t + 1) = params
- expression state at time t = "call_function_begin"
- the expression at time t = function call with name: name and arguments: args
then Python Object Store at time (t + 1) = Python Object Store at time t