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 k = s
- k > j
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 k = s
- k < j
- value at (j - 1) in map (Control Map at time t) = pair ("while", while_line)
then the line at time (t + 1) = while_line
- the line at time t = i
- the tab at time t = j
- statement at line i, tab k = s
- k < j
- value at (j - 1) in map (Control Map at time t) = pair ("while", while_line)
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 k = s
- k < j
- value at (j - 1) in map (Control Map at time t) = pair ("while", while_line)
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 k = s
- k < j
- value at (j - 1) in map (Control Map at time t) = pair ("while", while_line)
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 k = s
- k < j
- value at (j - 1) in map (Control Map at time t) = pair ("while", while_line)
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 k = s
- k < j
- value at (j - 1) in map (Control Map at time t) = pair ("while", while_line)
then expression state at time (t + 1) = expression state at time t
- the line at time t = i
- the tab at time t = j
- statement at line i, tab k = s
- k < j
- value at (j - 1) in map (Control Map at time t) = pair ("while", while_line)
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 k = s
- k < j
- value at (j - 1) in map (Control Map at time t) = pair ("while", while_line)
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 k = s
- k < j
- value at (j - 1) in map (Control Map at time t) = pair ("while", while_line)
then Control Map at time (t + 1) = Control Map at time t
- the line at time t = i
- the tab at time t = j
- number of lines = i - 1
- value at (j - 1) in map (Control Map at time t) = pair ("while", while_line)
then the line at time (t + 1) = while_line
- the line at time t = i
- the tab at time t = j
- number of lines = i - 1
- value at (j - 1) in map (Control Map at time t) = pair ("while", while_line)
then the tab at time (t + 1) = j - 1
- the line at time t = i
- the tab at time t = j
- number of lines = i - 1
- value at (j - 1) in map (Control Map at time t) = pair ("while", while_line)
then Variables Map at time (t + 1) = Variables Map at time t
- the line at time t = i
- the tab at time t = j
- number of lines = i - 1
- value at (j - 1) in map (Control Map at time t) = pair ("while", while_line)
then stack at time (t + 1) = stack at time t
- the line at time t = i
- the tab at time t = j
- number of lines = i - 1
- value at (j - 1) in map (Control Map at time t) = pair ("while", while_line)
then expression state at time (t + 1) = expression state at time t
- the line at time t = i
- the tab at time t = j
- number of lines = i - 1
- value at (j - 1) in map (Control Map at time t) = pair ("while", while_line)
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
- number of lines = i - 1
- value at (j - 1) in map (Control Map at time t) = pair ("while", while_line)
then Class Map at time (t + 1) = Class Map at time t
- the line at time t = i
- the tab at time t = j
- number of lines = i - 1
- value at (j - 1) in map (Control Map at time t) = pair ("while", while_line)
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 k = s
- k < j
then expression state at time (t + 1) = "not_expr"
- the line at time t = i
- the tab at time t = j
- number of lines = i - 1
- value at (j - 1) in map (Control Map at time t) = pair ("if", if_value)
then the line at time (t + 1) = i
- the line at time t = i
- the tab at time t = j
- number of lines = i - 1
- value at (j - 1) in map (Control Map at time t) = pair ("if", if_value)
then the tab at time (t + 1) = j - 1
- the line at time t = i
- the tab at time t = j
- number of lines = i - 1
- value at (j - 1) in map (Control Map at time t) = pair ("if", if_value)
then expression state at time (t + 1) = "not_expr"
- the line at time t = i
- the tab at time t = j
- number of lines = i - 1
- value at (j - 1) in map (Control Map at time t) = pair ("if", if_value)
then Variables Map at time (t + 1) = Variables Map at time t
- the line at time t = i
- the tab at time t = j
- number of lines = i - 1
- value at (j - 1) in map (Control Map at time t) = pair ("if", if_value)
then stack at time (t + 1) = stack at time t
- the line at time t = i
- the tab at time t = j
- number of lines = i - 1
- value at (j - 1) in map (Control Map at time t) = pair ("if", if_value)
then Class Map at time (t + 1) = Class Map at time t
- the line at time t = i
- the tab at time t = j
- number of lines = i - 1
- value at (j - 1) in map (Control Map at time t) = pair ("if", if_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
- "break" state at t = "breaking"
- value at (j - 1) in map (Control Map at time t) = control_value
- control_value describes a loop = True
then the line at time (t + 1) = i + 1
- the line at time t = i
- the tab at time t = j
- "break" state at t = "breaking"
- value at (j - 1) in map (Control Map at time t) = control_value
- control_value describes a loop = True
then "break" state at (t + 1) = "not_breaking"
- the line at time t = i
- the tab at time t = j
- "break" state at t = "breaking"
- value at (j - 1) in map (Control Map at time t) = control_value
- control_value describes a loop = False
then the line at time (t + 1) = i
- the line at time t = i
- the tab at time t = j
- "break" state at t = "breaking"
- value at (j - 1) in map (Control Map at time t) = control_value
- control_value describes a loop = False
then "break" state at (t + 1) = "breaking"
- the line at time t = i
- the tab at time t = j
- "continue" state at t = "continuing"
- value at (j - 1) in map (Control Map at time t) = control_value
- control_value describes a loop = True
then the line at time (t + 1) = while_line
- the line at time t = i
- the tab at time t = j
- "continue" state at t = "continuing"
- value at (j - 1) in map (Control Map at time t) = control_value
- control_value describes a loop = True
then "continue" state at (t + 1) = "not_continuing"
- the line at time t = i
- the tab at time t = j
- "continue" state at t = "continuing"
- value at (j - 1) in map (Control Map at time t) = control_value
- control_value describes a loop = False
then the line at time (t + 1) = i
- the line at time t = i
- the tab at time t = j
- "continue" state at t = "continuing"
- value at (j - 1) in map (Control Map at time t) = control_value
- control_value describes a loop = False
then "continue" state at (t + 1) = "continuing"
- 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 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 = 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 = 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 = 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 = 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 = 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 = 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 = 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 = 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
- 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 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 = 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 = function call with name: name and arguments: args
- expression state at time t = "end_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 = 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 = 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 = 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 = function call with name: name and arguments: args
- expression state at time t = "end_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 = c
- c is constant
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 = c
- c is constant
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 = 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 = c
- expression state at time t = "not_expr"
- c is constant
then the expression at time (t + 1) = c
- the line at time t = i
- the tab at time t = j
- statement at line i, tab j = c
- expression state at time t = "not_expr"
- c is constant
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 = c
- expression state at time t = "not_expr"
- c is constant
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
- expression state at time t = "not_expr"
- c is constant
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 = c
- expression state at time t = "not_expr"
- c is constant
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
- expression state at time t = "not_expr"
- c is constant
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 = c
- expression state at time t = "not_expr"
- c is constant
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 = x
- expression state at time t = "not_expr"
- x is a variable
then the expression at time (t + 1) = x
- the line at time t = i
- the tab at time t = j
- statement at line i, tab j = x
- expression state at time t = "not_expr"
- x is a variable
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 = x
- expression state at time t = "not_expr"
- x is a variable
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
- expression state at time t = "not_expr"
- x is a variable
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
- expression state at time t = "not_expr"
- x is a variable
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
- expression state at time t = "not_expr"
- x is a variable
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 = x
- expression state at time t = "not_expr"
- x is a variable
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 = x
- expression state at time t = "not_expr"
- 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 = function call with name: name and arguments: args
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
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 = function call with name: name and arguments: args
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
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 = c
- c is constant
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 = 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 = c
- c is constant
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 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 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
- 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
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 =
x = c
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 =
x = c
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
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 = c
- c is constant
then Variables Map at time (t + 1) = result of storing c 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 constant
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 constant
then the tab at time (t + 1) = j