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.

Skip Line (8)
if the following are true:

then Class Map at time (t + 1) = Class Map at time t


Return to While loop (1)
if the following are true:

then the line at time (t + 1) = while_line


Return to While loop (2)
if the following are true:

then the tab at time (t + 1) = j - 1


Return to While loop (3)
if the following are true:

then Variables Map at time (t + 1) = Variables Map at time t


Return to While loop (4)
if the following are true:

then stack at time (t + 1) = stack at time t


Return to While loop (5)
if the following are true:

then "if" map at time (t + 1) = "if" map at time t


Return to While loop (6)
if the following are true:

then expression state at time (t + 1) = expression state at time t


Return to While loop (7)
if the following are true:

then Python Object Store at time (t + 1) = Python Object Store at time t


Return to While loop (8)
if the following are true:

then Class Map at time (t + 1) = Class Map at time t


Return to While loop (9)
if the following are true:

then Control Map at time (t + 1) = Control Map at time t


Return to While loop At End (1)
if the following are true:

then the line at time (t + 1) = while_line


Return to While loop At End (2)
if the following are true:

then the tab at time (t + 1) = j - 1


Return to While loop At End (3)
if the following are true:

then Variables Map at time (t + 1) = Variables Map at time t


Return to While loop At End (4)
if the following are true:

then stack at time (t + 1) = stack at time t


Return to While loop At End (5)
if the following are true:

then expression state at time (t + 1) = expression state at time t


Return to While loop At End (6)
if the following are true:

then Python Object Store at time (t + 1) = Python Object Store at time t


Return to While loop At End (7)
if the following are true:

then Class Map at time (t + 1) = Class Map at time t


Return to While loop At End (8)
if the following are true:

then Control Map at time (t + 1) = Control Map at time t


When decrementing
if the following are true:

then expression state at time (t + 1) = "not_expr"


Decrement Tab At If End (1)
if the following are true:

then the line at time (t + 1) = i


Decrement Tab At If End (2)
if the following are true:

then the tab at time (t + 1) = j - 1


Decrement Tab At If End (3)
if the following are true:

then expression state at time (t + 1) = "not_expr"


Decrement Tab At If End (4)
if the following are true:

then Variables Map at time (t + 1) = Variables Map at time t


Decrement Tab At If End (5)
if the following are true:

then stack at time (t + 1) = stack at time t


Decrement Tab At If End (6)
if the following are true:

then Class Map at time (t + 1) = Class Map at time t


Decrement Tab At If End (7)
if the following are true:

then Control Map at time (t + 1) = Control Map at time t


End Breaking (1)
if the following are true:

then the line at time (t + 1) = i + 1


End Breaking (2)
if the following are true:

then "break" state at (t + 1) = "not_breaking"


Breaking On Not Loop (1)
if the following are true:

then the line at time (t + 1) = i


Breaking On Not Loop (2)
if the following are true:

then "break" state at (t + 1) = "breaking"


When Breaking (1)
if "break" state at t = "breaking", then the tab at time (t + 1) = (the tab at time t) - 1

When Breaking (2)
if "break" state at t = "breaking", then Python Object Store at time (t + 1) = Python Object Store at time t

When Breaking (3)
if "break" state at t = "breaking", then Class Map at time (t + 1) = Class Map at time t

When Breaking (4)
if "break" state at t = "breaking", then Variables Map at time (t + 1) = Variables Map at time t

When Breaking (5)
if "break" state at t = "breaking", then stack at time (t + 1) = stack at time t

When Breaking (6)
if "break" state at t = "breaking", then Control Map at time (t + 1) = Control Map at time t

End Continuing (1)
if the following are true:

then the line at time (t + 1) = while_line


End Continuing (2)
if the following are true:

then "continue" state at (t + 1) = "not_continuing"


Continuing On Not Loop (1)
if the following are true:

then the line at time (t + 1) = i


Continuing On Not Loop (2)
if the following are true:

then "continue" state at (t + 1) = "continuing"


When Continuing (1)
if "continue" state at t = "continuing", then the tab at time (t + 1) = (the tab at time t) - 1

When Continuing (2)
if "continue" state at t = "continuing", then expression state at time (t + 1) = "not_expr"

When Continuing (3)
if "continue" state at t = "continuing", then Python Object Store at time (t + 1) = Python Object Store at time t

When Continuing (4)
if "continue" state at t = "continuing", then Class Map at time (t + 1) = Class Map at time t

When Continuing (5)
if "continue" state at t = "continuing", then Variables Map at time (t + 1) = Variables Map at time t

When Continuing (6)
if "continue" state at t = "continuing", then stack at time (t + 1) = stack at time t

When Continuing (7)
if "continue" state at t = "continuing", then Control Map at time (t + 1) = Control Map at time t

Call (1)
if the following are true:

then the expression at time (t + 1) = function call with name: name and arguments: args


Call (2)
if the following are true:

then expression state at time (t + 1) = "begin_expr"


Call (3)
if the following are true:

then the line at time (t + 1) = i


Call (4)
if the following are true:

then the tab at time (t + 1) = j


Call (5)
if the following are true:

then Value Stack at time (t + 1) = [ ]


Call (6)
if the following are true:

then parent stack at time (t + 1) = [ ]


Call (7)
if the following are true:

then arguments stack at time (t + 1) = [ ]


Call (8)
if the following are true:

then Control Map at time (t + 1) = Control Map at time t


Call (9)
if the following are true:

then Python Object Store at time (t + 1) = Python Object Store at time t


Call ended (1)
if the following are true:

then the line at time (t + 1) = i + 1


Call ended (2)
if the following are true:

then the tab at time (t + 1) = the tab at time t


Call ended (3)
if the following are true:

then Variables Map at time (t + 1) = Variables Map at time t


Call ended (4)
if the following are true:

then stack at time (t + 1) = stack at time t


Call ended (5)
if the following are true:

then Control Map at time (t + 1) = Control Map at time t


Call ended (6)
if the following are true:

then Python Object Store at time (t + 1) = Python Object Store at time t


Call ended (7)
if the following are true:

then Class Map at time (t + 1) = Class Map at time t


Call Constant Unchanged (1)
if the following are true:

then Class Map at time (t + 1) = Class Map at time t


Call Constant Unchanged (2)
if the following are true:

then Control Map at time (t + 1) = Control Map at time t


Call Constant Unchanged (3)
if the following are true:

then Python Object Store at time (t + 1) = Python Object Store at time t


Call Constant (1)
if the following are true:

then the expression at time (t + 1) = c


Call Constant (2)
if the following are true:

then expression state at time (t + 1) = "begin_expr"


Call Constant (3)
if the following are true:

then the line at time (t + 1) = i


Call Constant (4)
if the following are true:

then the tab at time (t + 1) = j


Call Constant (5)
if the following are true:

then Value Stack at time (t + 1) = [ ]


Call Constant (6)
if the following are true:

then parent stack at time (t + 1) = [ ]


Call Constant (7)
if the following are true:

then arguments stack at time (t + 1) = [ ]


Call Variable (1)
if the following are true:

then the expression at time (t + 1) = x


Call Variable (2)
if the following are true:

then expression state at time (t + 1) = "begin_expr"


Call Variable (3)
if the following are true:

then the line at time (t + 1) = i


Call Variable (4)
if the following are true:

then the tab at time (t + 1) = j


Call Variable (5)
if the following are true:

then Value Stack at time (t + 1) = [ ]


Call Variable (6)
if the following are true:

then parent stack at time (t + 1) = [ ]


Call Variable (7)
if the following are true:

then arguments stack at time (t + 1) = [ ]


Call Variable (8)
if the following are true:

then Control Map at time (t + 1) = Control Map at time t


Call Unchanged (1)
if the following are true:

then Variables Map at time (t + 1) = Variables Map at time t


Call Unchanged (2)
if the following are true:

then stack at time (t + 1) = stack at time t


Call Unchanged (3)
if the following are true:

then Control Map at time (t + 1) = Control Map at time t


Call Unchanged (4)
if the following are true:

then Class Map at time (t + 1) = Class Map at time t


Constant Unchanged (1)
if the following are true:

then Variables Map at time (t + 1) = Variables Map at time t


Constant Unchanged (2)
if the following are true:

then stack at time (t + 1) = stack at time t


Constant Unchanged (3)
if the following are true:

then Control Map at time (t + 1) = Control Map at time t


Variable Unchanged (1)
if the following are true:

then Variables Map at time (t + 1) = Variables Map at time t


Variable Unchanged (2)
if the following are true:

then stack at time (t + 1) = stack at time t


Variable Unchanged (3)
if the following are true:

then Control Map at time (t + 1) = Control Map at time t


Variable Unchanged (4)
if the following are true:

then Class Map at time (t + 1) = Class Map at time t


Variable Unchanged (5)
if the following are true:

then Python Object Store at time (t + 1) = Python Object Store at time t


Assign If Stack (1)
if the following are true:

then "if" map at time (t + 1) = "if" map at time t


Assign If Stack (2)
if the following are true:

then 'while stack' at time (t + 1) = 'while stack' at time t


Assign If Stack (3)
if the following are true:

then Control Map at time (t + 1) = Control Map at time t


Assign If Stack (4)
if the following are true:

then Class Map at time (t + 1) = Class Map at time t


Assign Constant (1)
if the following are true:

then Variables Map at time (t + 1) = result of storing c at key: x in map: (Variables Map at time t)


Assign Constant (2)
if the following are true:

then the line at time (t + 1) = i + 1


Assign Constant (3)
if the following are true:

then the tab at time (t + 1) = j


5 6 7