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.

Do Children Values (3)

if the following are true:

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


Call Function Begin

if the following are true:

then Parameters List at time (t + 1) = params


call func begin object store

if the following are true:

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


Call Build Args (1)

if expression state at time t = "call_build_args", then parent stack at time (t + 1) = parent stack at time t


Call Build Args (2)

if expression state at time t = "call_build_args", then arguments stack at time (t + 1) = arguments stack at time t


Call Build Args (3)

if expression state at time t = "call_build_args", then Value Stack at time (t + 1) = Value Stack at time t


Call Build Args (4)

if expression state at time t = "call_build_args", then the expression at time (t + 1) = the expression at time t


Call Build Args (5)

if expression state at time t = "call_build_args", then Class Map at time (t + 1) = Class Map at time t


Call Build Args Unchanged on Params (1)

if the following are true:

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


Call Build Args Unchanged on Params (2)

if the following are true:

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


Call Build Args Set Variables (1)

if the following are true:

then Function Variables Map at time (t + 1) = result of storing value at key: var in map: (Function Variables Map at time t)


Call Build Args Set Variables (2)

if the following are true:

then Parameters List at time (t + 1) = frest


Call Build Args Set Variables (3)

if the following are true:

then Argument Values at time (t + 1) = vrest


Call Build Args Set Variables (4)

if the following are true:

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


Call Build Args Set Variables (5)

if the following are true:

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


Call Build Args Set Variables (6)

if the following are true:

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


Call Build Args Set Variables (7)

if the following are true:

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


Call Build Args Set Variables (8)

if the following are true:

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


Call build args state (1)

if the following are true:

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


Call build args state (2)

if the following are true:

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


Call build args state (3)

if the following are true:

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


Call build args state (4)

if the following are true:

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


Call build args state (5)

if the following are true:

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 ]


Call Line (1)

if the following are true:

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


Call Line (2)

if the following are true:

then Control Map at time (t + 1) = [ entry 0: (pair ("function", name)), [ ] ]


Call Returned Unchanged (1)

if expression state at time t = "call_returned", then Variables Map at time (t + 1) = Variables Map at time t


Call Returned Unchanged (2)

if expression state at time t = "call_returned", then the line at time (t + 1) = the line at time t


Call Returned Unchanged (3)

if expression state at time t = "call_returned", then the tab at time (t + 1) = the tab at time t


Call Returned Unchanged (4)

if expression state at time t = "call_returned", then stack at time (t + 1) = stack at time t


Call Returned Unchanged (5)

if expression state at time t = "call_returned", then Return Value at time (t + 1) = Return Value at time t


Call Returned Unchanged (6)

if expression state at time t = "call_returned", then parent stack at time (t + 1) = parent stack at time t


Call Returned Unchanged (7)

if expression state at time t = "call_returned", then arguments stack at time (t + 1) = arguments stack at time t


Call Returned Unchanged (8)

if expression state at time t = "call_returned", then Value Stack at time (t + 1) = Value Stack at time t


Call Returned Unchanged (9)

if expression state at time t = "call_returned", then Python Object Store at time (t + 1) = Python Object Store at time t


Call Returned Unchanged (10)

if expression state at time t = "call_returned", then Control Map at time (t + 1) = Control Map at time t


Call Returned Unchanged (11)

if expression state at time t = "call_returned", then Class Map at time (t + 1) = Class Map at time t


Call Returned End

if the following are true:

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


Call Returned Return

if the following are true:

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


Return (1)

if expression state at time t = "return", then expression state at time (t + 1) = "iterate_args"


Return (2)

if expression state at time t = "return", then the expression at time (t + 1) = the expression at time t


Return (3)

if expression state at time t = "return", then arguments stack at time (t + 1) = arguments stack at time t


Return (4)

if expression state at time t = "return", then parent stack at time (t + 1) = parent stack at time t


Return (5)

if expression state at time t = "return", then Variables Map at time (t + 1) = Variables Map at time t


Return (6)

if expression state at time t = "return", then the line at time (t + 1) = the line at time t


Return (7)

if expression state at time t = "return", then the tab at time (t + 1) = the tab at time t


Return (8)

if expression state at time t = "return", then stack at time (t + 1) = stack at time t


Return (9)

if expression state at time t = "return", then Python Object Store at time (t + 1) = Python Object Store at time t


Return (10)

if expression state at time t = "return", then Control Map at time (t + 1) = Control Map at time t


Return (11)

if expression state at time t = "return", then Class Map at time (t + 1) = Class Map at time t


Append To Value Stack

if the following are true:

then Value Stack at time (t + 1) = [ [ r, v ], w ]


Assign Variable to Call Result (1)

if the following are true:

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)


Assign Variable to Call Result (2)

if the following are true:

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


Assign Variable to Call Result (3)

if the following are true:

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


Assign Variable to Call Result (4)

if the following are true:

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


Assign Variable to Call Result (5)

if the following are true:

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


Assign Variable to Call Result (6)

if the following are true:

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


If Condition Test (1)

if the following are true:

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


If Condition Test (2)

if the following are true:

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


If Condition Test (3)

if the following are true:

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


If Condition Test (4)

if the following are true:

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


If Condition Test (5)

if the following are true:

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


If Condition Test (6)

if the following are true:

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


If Condition Test (7)

if the following are true:

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


If Condition Test (8)

if the following are true:

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


If Condition Test (9)

if the following are true:

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


Unchanged on If (1)

if the following are true:

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


Unchanged on If (2)

if the following are true:

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


Unchanged on If (3)

if the following are true:

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


Unchanged on If (4)

if the following are true:

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


Unchanged on If (5)

if the following are true:

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


If ended object store

if the following are true:

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


Set If Condition True (1)

if the following are true:

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


Set If Condition True (2)

if the following are true:

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


Set If Condition True (3)

if the following are true:

then Control Map at time (t + 1) = result of storing (pair ("if", True)) at key: j in map: (Control Map at time t)


Set If Condition True (4)

if the following are true:

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


If False (1)

if the following are true:

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


If False (2)

if the following are true:

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


If False (3)

if the following are true:

then Control Map at time (t + 1) = result of storing (pair ("if", False)) at key: j in map: (Control Map at time t)


If False (4)

if the following are true:

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


Elif not Expr unchanged (1)

if the following are true:

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


Elif not Expr unchanged (2)

if the following are true:

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


Elif Test (1)

if the following are true:

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


Elif Test (2)

if the following are true:

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


Elif Test (3)

if the following are true:

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


Elif Test (4)

if the following are true:

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


Elif Test (5)

if the following are true:

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


Elif Test (6)

if the following are true:

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


Elif Test (7)

if the following are true:

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


Skip Elif (1)

if the following are true:

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


Skip Elif (2)

if the following are true:

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


Elif end Expr unchanged

if the following are true:

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


Evaluate Elif (1)

if the following are true:

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


Evaluate Elif (2)

if the following are true:

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


Evaluate Elif (3)

if the following are true:

then Control Map at time (t + 1) = result of storing (pair ("if", True)) at key: j in map: (Control Map at time t)


Evaluate Elif (4)

if the following are true:

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


Elif False (1)

if the following are true:

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


Elif False (2)

if the following are true:

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


Elif False (3)

if the following are true:

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


Elif False (4)

if the following are true:

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


Elif Unchanged (1)

if the following are true:

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


Pages: 7 8 9 ... 20