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.

Prepare For Function Call (4)

if the following are true:

then Value Stack at time (t + 1) = v_rest


Prepare For Function Call (5)

if the following are true:

then Expression Stack at time (t + 1) = Expression Stack at time t


Prepare For Function Call (6)

if the following are true:

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


Prepare For Function Call (7)

if the following are true:

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


Prepare For Function Call (8)

if the following are true:

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


Prepare For Function Call (9)

if the following are true:

then Context Stack at time (t + 1) = Context Stack at time t


Prepare For Function Call (10)

if the following are true:

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


Prepare For Function Call (11)

if the following are true:

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


Build Function 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)


Build Function Variables (2)

if the following are true:

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


Build Function Variables (3)

if the following are true:

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


Build Function Variables (4)

if the following are true:

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


Unchanged On Func Params (1)

if Parameters List at time t = [ var, frest ], then Expression Stack at time (t + 1) = Expression Stack at time t


Unchanged On Func Params (2)

if Parameters List at time t = [ var, frest ], then Variables Map at time (t + 1) = Variables Map at time t


Unchanged On Func Params (3)

if Parameters List at time t = [ var, frest ], then Control Map at time (t + 1) = Control Map at time t


Unchanged On Func Params (4)

if Parameters List at time t = [ var, frest ], then Context Stack at time (t + 1) = Context Stack at time t


Unchanged On Func Params (5)

if Parameters List at time t = [ var, frest ], then the line at time (t + 1) = the line at time t


Unchanged On Func Params (6)

if Parameters List at time t = [ var, frest ], then the tab at time (t + 1) = the tab at time t


Unchanged On Func Params (7)

if Parameters List at time t = [ var, frest ], then Value Stack at time (t + 1) = Value Stack at time t


Jump To Function (1)

if Parameters List at time t = [ ], then Variables Map at time (t + 1) = Function Variables Map at time t


Jump To Function (2)

if Parameters List at time t = [ ], then the tab at time (t + 1) = 1


Jump To Function (3)

if Parameters List at time t = [ ], then Context Stack at time (t + 1) = [ program context with variables: (Variables Map at time t) and expression state: (expression state with expression stack: (Expression 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), Context Stack at time t ]


Jump To Function (4)

if Parameters List at time t = [ ], then Parameters List at time (t + 1) = None


Jump To Function (5)

if Parameters List at time t = [ ], then Expression Stack at time (t + 1) = [ ]


Jump To Function (6)

if Parameters List at time t = [ ], then Python Object Store at time (t + 1) = Python Object Store at time t


Jump To Function Line (1)

if the following are true:

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


Jump To Function Line (2)

if the following are true:

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


Push Call Return Value (1)

if the following are true:

then Value Stack at time (t + 1) = [ [ r, next_level ], other_levels ]


Push Call Return Value (2)

if the following are true:

then Expression Stack at time (t + 1) = [ ys, rest ]


Push Call Return Value (3)

if the following are true:

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


Push Call Return Value (4)

if the following are true:

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


Push Call Return Value (5)

if the following are true:

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


Push Call Return Value (6)

if the following are true:

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


Push Call Return Value (7)

if the following are true:

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


Push Call Return Value (8)

if the following are true:

then Context Stack at time (t + 1) = Context Stack at time t


Push Call Return Value (9)

if the following are true:

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


Push Call Return Value (10)

if the following are true:

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


Reset Expression Stack

if Expression Stack at time t = [ [ ], [ ] ], then Expression Stack at time (t + 1) = [ ]


Start Assignment Expression (1)

if the following are true:

then Expression Stack at time (t + 1) = [ [ expr, [ ] ], [ ] ]


Start Assignment Expression (2)

if the following are true:

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


Start Assignment Expression (3)

if the following are true:

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


Start Assignment Expression (4)

if the following are true:

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


Start Assignment Expression (5)

if the following are true:

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


Start Assignment Expression (6)

if the following are true:

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


Start Assignment Expression (7)

if the following are true:

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


Start Assignment Expression (8)

if the following are true:

then Context Stack at time (t + 1) = Context Stack at time t


Assign Variable End (1)

if the following are true:

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


Assign Variable End (2)

if the following are true:

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


Assign Variable End (3)

if the following are true:

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


Assign Variable End (4)

if the following are true:

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


Assign Variable End (5)

if the following are true:

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


Assign Variable End (6)

if the following are true:

then Context Stack at time (t + 1) = Context Stack at time t


Unchanged On Assign

if the following are true:

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


Start If Test (1)

if the following are true:

then Expression Stack at time (t + 1) = [ [ expr, [ ] ], [ ] ]


Start If Test (2)

if the following are true:

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


Start If Test (3)

if the following are true:

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


Start If Test (4)

if the following are true:

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


Start If Test (5)

if the following are true:

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


Start If Test (6)

if the following are true:

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


Start If Test (7)

if the following are true:

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


Start If Test (8)

if the following are true:

then Context Stack at time (t + 1) = Context Stack at time t


If Test Is True (1)

if the following are true:

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


If Test Is True (2)

if the following are true:

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


If Test Is 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)


If Test Is False (1)

if the following are true:

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


If Test Is False (2)

if the following are true:

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


If Test Is 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)


Variables Unchanged On If End (1)

if the following are true:

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


Variables Unchanged On If End (2)

if the following are true:

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


Variables Unchanged On If End (3)

if the following are true:

then Context Stack at time (t + 1) = Context Stack at time t


Variables Unchanged On If End (4)

if the following are true:

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


Unchanged On If

if the following are true:

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


ElIf Start Unchanged (1)

if the following are true:

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


ElIf Start Unchanged (2)

if the following are true:

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


ElIf Start Unchanged (3)

if the following are true:

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


ElIf Start Unchanged (4)

if the following are true:

then Context Stack at time (t + 1) = Context Stack at time t


Start ElIf Test (1)

if the following are true:

then Expression Stack at time (t + 1) = [ [ expr, [ ] ], [ ] ]


Start ElIf Test (2)

if the following are true:

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


Start ElIf Test (3)

if the following are true:

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


Start ElIf Test (4)

if the following are true:

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


Start ElIf Test (5)

if the following are true:

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


Start ElIf Test (6)

if the following are true:

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


Start ElIf Test (7)

if the following are true:

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


Start ElIf Test (8)

if the following are true:

then Context Stack at time (t + 1) = Context Stack at time t


Skip Elif Block (1)

if the following are true:

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


Skip Elif Block (2)

if the following are true:

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


Skip Elif Block (3)

if the following are true:

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


Skip Elif Block (4)

if the following are true:

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


Skip Elif Block (5)

if the following are true:

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


Skip Elif Block (6)

if the following are true:

then Context Stack at time (t + 1) = Context Stack at time t


Unchanged When Elif Ended (1)

if the following are true:

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


Unchanged When Elif Ended (2)

if the following are true:

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


Unchanged When Elif Ended (3)

if the following are true:

then Context Stack at time (t + 1) = Context Stack at time t


Elif Test Is True (1)

if the following are true:

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


Elif Test Is True (2)

if the following are true:

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


Elif Test Is 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)


Elif Test Is False (1)

if the following are true:

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


Elif Test Is False (2)

if the following are true:

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


Elif Test Is False (3)

if the following are true:

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


Elif unchanged

if the following are true:

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


Pages: 15 16 17 ... 20