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 =
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 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 =
else:
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 =
else:
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 =
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
- the line at time t = i
- the tab at time t = j
- statement at line i, tab j =
else:
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 ("if", if_value)
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 k = s
- k < j
- 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
- statement at line i, tab k = s
- k < j
- 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
- statement at line i, tab k = s
- k < j
- 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
- statement at line i, tab k = s
- k < j
- value at (j - 1) in map (Control Map at time t) = pair ("if", if_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 k = s
- k < j
- 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
- statement at line i, tab k = s
- k < j
- 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
- statement at line i, tab j = "while" statement with condition (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 = "while" statement with condition (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 = "while" statement with condition (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 = "while" statement with condition (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 = "while" statement with condition (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 = "while" statement with condition (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 = "while" statement with condition (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 = "while" statement with condition (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 = "while" statement with condition (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 = "while" statement with condition (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 = "while" statement with condition (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 = "while" statement with condition (function call with name: name and arguments: args)
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 = "while" statement with condition (function call with name: name and arguments: args)
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 = "while" statement with condition (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 = "while" statement with condition (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 = "while" statement with condition (function call with name: name and arguments: args)
- expression state at time t = "end_expr"
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 = "while" statement with condition (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 = "while" statement with condition (function call with name: name and arguments: args)
- 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 = "while" statement with condition (function call with name: name and arguments: args)
- expression state at time t = "end_expr"
- Return Value at time t = True
then Control Map at time (t + 1) = result of storing (pair ("while", i)) 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 = "while" statement with condition (function call with name: name and arguments: args)
- 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 = "while" statement with condition (function call with name: name and arguments: args)
- 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 =
break
then "break" state at (t + 1) = "breaking"
- the line at time t = i
- the tab at time t = j
- statement at line i, tab j =
break
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 =
break
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 =
break
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 =
break
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 =
break
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 =
break
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 =
break
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 =
break
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 =
continue
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 =
continue
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 =
continue
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 =
continue
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 =
continue
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 =
continue
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 =
continue
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 =
continue
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 =
continue
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 =
continue
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 =
continue
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 definition where name: name and parameters: params
then there is a function named name with parameters params at line line
- the line at time t = i
- the tab at time t = j
- statement at line i, tab j = function definition where name: name and parameters: params
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 definition where name: name and parameters: params
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 definition where name: name and parameters: params
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 definition where name: name and parameters: params
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 definition where name: name and parameters: params
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 = function definition where name: name and parameters: params
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 = function definition where name: name and parameters: params
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 definition where name: name and parameters: params
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 definition where name: name and parameters: params
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 =
return v
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 =
return v
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 =
return v
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 =
return 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 =
return 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 =
return rex
- expression state at time t = "not_expr"
then the expression at time (t + 1) = rex
- the line at time t = i
- the tab at time t = j
- statement at line i, tab j =
return rex
- 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 =
return rex
- 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 =
return rex
- 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 =
return rex
- 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 =
return rex
- 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 =
return rex
- 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 =
return rex
- 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 =
return rex
- 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 =
return rex
- 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 =
return rex
- 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 =
return rex
- stack at time t = [ program context with variables: varis and expression state: (expression state with parent stack: parent_stack arguments: arg_stack values: value_stack line: line tab: tab) and control map: control_map, rest ]
- expression state at time t = "end_expr"
then Variables Map at time (t + 1) = varis
- the line at time t = i
- the tab at time t = j
- statement at line i, tab j =
return rex
- stack at time t = [ program context with variables: varis and expression state: (expression state with parent stack: parent_stack arguments: arg_stack values: value_stack line: line tab: tab) and control map: control_map, rest ]
- expression state at time t = "end_expr"
then the line at time (t + 1) = line
- the line at time t = i
- the tab at time t = j
- statement at line i, tab j =
return rex
- stack at time t = [ program context with variables: varis and expression state: (expression state with parent stack: parent_stack arguments: arg_stack values: value_stack line: line tab: tab) and control map: control_map, rest ]
- expression state at time t = "end_expr"
then the tab at time (t + 1) = tab
- the line at time t = i
- the tab at time t = j
- statement at line i, tab j =
return rex
- stack at time t = [ program context with variables: varis and expression state: (expression state with parent stack: parent_stack arguments: arg_stack values: value_stack line: line tab: tab) and control map: control_map, rest ]
- expression state at time t = "end_expr"
then expression state at time (t + 1) = "call_returned"
- the line at time t = i
- the tab at time t = j
- statement at line i, tab j =
return rex
- stack at time t = [ program context with variables: varis and expression state: (expression state with parent stack: parent_stack arguments: arg_stack values: value_stack line: line tab: tab) and control map: control_map, rest ]
- expression state at time t = "end_expr"
then parent stack at time (t + 1) = parent_stack
- the line at time t = i
- the tab at time t = j
- statement at line i, tab j =
return rex
- stack at time t = [ program context with variables: varis and expression state: (expression state with parent stack: parent_stack arguments: arg_stack values: value_stack line: line tab: tab) and control map: control_map, rest ]
- expression state at time t = "end_expr"
then Control Map at time (t + 1) = control_map
- the line at time t = i
- the tab at time t = j
- statement at line i, tab j =
return rex
- stack at time t = [ program context with variables: varis and expression state: (expression state with parent stack: parent_stack arguments: arg_stack values: value_stack line: line tab: tab) and control map: control_map, rest ]
- expression state at time t = "end_expr"
then stack at time (t + 1) = rest
- the line at time t = i
- the tab at time t = j
- statement at line i, tab j =
return rex
- stack at time t = [ program context with variables: varis and expression state: (expression state with parent stack: parent_stack arguments: arg_stack values: value_stack line: line tab: tab) and control map: control_map, rest ]
- expression state at time t = "end_expr"
then Value Stack at time (t + 1) = value_stack
- the line at time t = i
- the tab at time t = j
- statement at line i, tab j =
return rex
- stack at time t = [ program context with variables: varis and expression state: (expression state with parent stack: parent_stack arguments: arg_stack values: value_stack line: line tab: tab) and control map: control_map, rest ]
- expression state at time t = "end_expr"
then arguments stack at time (t + 1) = arg_stack
- the line at time t = i
- the tab at time t = j
- statement at line i, tab j =
return rex
- stack at time t = [ program context with variables: varis and expression state: (expression state with parent stack: parent_stack arguments: arg_stack values: value_stack line: line tab: tab) and control map: control_map, rest ]
- expression state at time t = "end_expr"
then Return Value at time (t + 1) = Return Value at time t
- the line at time t = i
- the tab at time t = j
- statement at line i, tab j =
return rex
- 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 = return (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 instruction at computer c and index i = an ADDI instruction with src: src imm: imm and dst: dst
- the PC at computer c and time t = i
then byte at ID: c, cell #dst at time (t + 1) = (byte at ID: c, cell #src at time t) + imm
- the instruction at computer c and index i = an ADDI instruction with src: src imm: imm and dst: dst
- the PC at computer c and time t = i
- not (other = dst)
then byte at ID: c, cell #other at time (t + 1) = byte at ID: c, cell #other at time t
- the instruction at computer c and index i = subtract immediate instruction with dst: dst src: src and immediate: imm
- the PC at computer c and time t = i
then byte at ID: c, cell #dst at time (t + 1) = (byte at ID: c, cell #src at time t) - imm
- the instruction at computer c and index i = subtract immediate instruction with dst: dst src: src and immediate: imm
- the PC at computer c and time t = i
- not (other = dst)
then byte at ID: c, cell #other at time (t + 1) = byte at ID: c, cell #other at time t
- the instruction at computer c and index i = an add instruction with dst: d src1: s1 and src2: s2
- the PC at computer c and time t = i
then byte at ID: c, cell #d at time (t + 1) = (byte at ID: c, cell #s1 at time t) + (byte at ID: c, cell #s2 at time t)