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.

Decrement When Continuing (5)

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

Decrement When Continuing (6)

if "continue" state at t = "continuing", then Context Stack at time (t + 1) = Context Stack at time t

Decrement When Continuing (7)

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

Unchanged On Call Constant (1)

if the following are true:

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

Unchanged On Call Constant (2)

if the following are true:

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

Unchanged On Call Constant (3)

if the following are true:

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

Unchanged On Call Constant (4)

if the following are true:

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

Unchanged On Call Constant (5)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = c
c is constant

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

Push Constant Statement To Stack (1)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = c
c is constant
Expression Stack at time t = [ ]

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

Push Constant Statement To Stack (2)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = c
c is constant
Expression Stack at time t = [ ]

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

Push Constant Statement To Stack (3)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = c
c is constant
Expression Stack at time t = [ ]

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

Push Constant Statement To Stack (4)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = c
c is constant
Expression Stack at time t = [ ]

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

Unchanged On Variable (1)

if the following are true:

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

Unchanged On Variable (2)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = x
x is a variable

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

Unchanged On Variable (3)

if the following are true:

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

Unchanged On Variable (4)

if the following are true:

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

Unchanged On Variable (5)

if the following are true:

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

Push Variable Statement To Stack (1)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = x
c is a variable
Expression Stack at time t = [ ]

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

Push Variable Statement To Stack (2)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = x
c is a variable
Expression Stack at time t = [ ]

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

Push Variable Statement To Stack (3)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = x
c is a variable
Expression Stack at time t = [ ]

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

Push Variable Statement To Stack (4)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = x
c is a variable
Expression Stack at time t = [ ]

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

Class Defs On Call

if the following are true:

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

Push Call To Stack (1)

if the following are true:

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 Stack at time t = [ ]

then Expression Stack at time (t + 1) = [ [ function call with name: name and arguments: args, [ ] ], [ ] ]

Push Call To Stack (2)

if the following are true:

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 Stack at time t = [ ]

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

Push Call To Stack (3)

if the following are true:

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 Stack at time t = [ ]

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

Push Call To Stack (4)

if the following are true:

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 Stack at time t = [ ]

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

Push Call To Stack (5)

if the following are true:

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 Stack at time t = [ ]

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

Push Call To Stack (6)

if the following are true:

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 Stack at time t = [ ]

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

Push Call To Stack (7)

if the following are true:

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 Stack at time t = [ ]

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

Push Call To Stack (8)

if the following are true:

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 Stack at time t = [ ]

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

Push Constant To Stack (1)

if the following are true:

Expression Stack at time t = [ [ x, ys ], rest ]
Value Stack at time t = [ values, v_rest ]
x is constant

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

Push Constant To Stack (2)

if the following are true:

Expression Stack at time t = [ [ x, ys ], rest ]
Value Stack at time t = [ values, v_rest ]
x is constant

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

Push Constant To Stack (3)

if the following are true:

Expression Stack at time t = [ [ x, ys ], rest ]
Value Stack at time t = [ values, v_rest ]
x is constant

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

Push Constant To Stack (4)

if the following are true:

Expression Stack at time t = [ [ x, ys ], rest ]
Value Stack at time t = [ values, v_rest ]
x is constant

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

Push Constant To Stack (5)

if the following are true:

Expression Stack at time t = [ [ x, ys ], rest ]
Value Stack at time t = [ values, v_rest ]
x is constant

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

Push Constant To Stack (6)

if the following are true:

Expression Stack at time t = [ [ x, ys ], rest ]
Value Stack at time t = [ values, v_rest ]
x is constant

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

Push Constant To Stack (7)

if the following are true:

Expression Stack at time t = [ [ x, ys ], rest ]
Value Stack at time t = [ values, v_rest ]
x is constant

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

Push Constant To Stack (8)

if the following are true:

Expression Stack at time t = [ [ x, ys ], rest ]
Value Stack at time t = [ values, v_rest ]
x is constant

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

Push Constant To Stack (9)

if the following are true:

Expression Stack at time t = [ [ x, ys ], rest ]
Value Stack at time t = [ values, v_rest ]
x is constant

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

Push Variable Value To Stack (1)

if the following are true:

Expression Stack at time t = [ [ x, ys ], rest ]
Value Stack at time t = [ values, v_rest ]
x is a variable

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

Push Variable Value To Stack (2)

if the following are true:

Expression Stack at time t = [ [ x, ys ], rest ]
Value Stack at time t = [ values, v_rest ]
x is a variable

then Value Stack at time (t + 1) = [ [ value at x in map (Variables Map at time t), values ], v_rest ]

Push Variable Value To Stack (3)

if the following are true:

Expression Stack at time t = [ [ x, ys ], rest ]
Value Stack at time t = [ values, v_rest ]
x is a variable

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

Push Variable Value To Stack (4)

if the following are true:

Expression Stack at time t = [ [ x, ys ], rest ]
Value Stack at time t = [ values, v_rest ]
x is a variable

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

Push Variable Value To Stack (5)

if the following are true:

Expression Stack at time t = [ [ x, ys ], rest ]
Value Stack at time t = [ values, v_rest ]
x is a variable

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

Push Variable Value To Stack (6)

if the following are true:

Expression Stack at time t = [ [ x, ys ], rest ]
Value Stack at time t = [ values, v_rest ]
x is a variable

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

Push Variable Value To Stack (7)

if the following are true:

Expression Stack at time t = [ [ x, ys ], rest ]
Value Stack at time t = [ values, v_rest ]
x is a variable

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

Push Variable Value To Stack (8)

if the following are true:

Expression Stack at time t = [ [ x, ys ], rest ]
Value Stack at time t = [ values, v_rest ]
x is a variable

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

Push Variable Value To Stack (9)

if the following are true:

Expression Stack at time t = [ [ x, ys ], rest ]
Value Stack at time t = [ values, v_rest ]
x is a variable

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

Push Arguments To Stack (1)

if Expression Stack at time t = [ [ function call with name: name and arguments: args, ys ], rest ], then Expression Stack at time (t + 1) = [ args, [ [ function call with name: name and arguments: args, ys ], rest ] ]

Push Arguments To Stack (2)

if Expression Stack at time t = [ [ function call with name: name and arguments: args, ys ], rest ], then Value Stack at time (t + 1) = [ [ ], Value Stack at time t ]

Push Arguments To Stack (3)

if Expression Stack at time t = [ [ function call with name: name and arguments: args, ys ], rest ], then Parameters List at time (t + 1) = None

Push Arguments To Stack (4)

if Expression Stack at time t = [ [ function call with name: name and arguments: args, ys ], rest ], then the line at time (t + 1) = the line at time t

Push Arguments To Stack (5)

if Expression Stack at time t = [ [ function call with name: name and arguments: args, ys ], rest ], then the tab at time (t + 1) = the tab at time t

Push Arguments To Stack (6)

if Expression Stack at time t = [ [ function call with name: name and arguments: args, ys ], rest ], then Variables Map at time (t + 1) = Variables Map at time t

Push Arguments To Stack (7)

if Expression Stack at time t = [ [ function call with name: name and arguments: args, ys ], rest ], then Control Map at time (t + 1) = Control Map at time t

Push Arguments To Stack (8)

if Expression Stack at time t = [ [ function call with name: name and arguments: args, ys ], rest ], then Python Object Store at time (t + 1) = Python Object Store at time t

Push Arguments To Stack (9)

if Expression Stack at time t = [ [ function call with name: name and arguments: args, ys ], rest ], then Context Stack at time (t + 1) = Context Stack at time t

Perform Addition

if the following are true:

Expression Stack at time t = [ [ ], [ [ function call with name: "__add__" and arguments: args, ys ], rest ] ]
Value Stack at time t = [ [ a, [ b, [ ] ] ], [ next_level, other_levels ] ]

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

On Stack Addition (1)

if Expression Stack at time t = [ [ ], [ [ function call with name: "__add__" and arguments: args, ys ], rest ] ], then Expression Stack at time (t + 1) = [ ys, rest ]

On Stack Addition (2)

if Expression Stack at time t = [ [ ], [ [ function call with name: "__add__" and arguments: args, ys ], rest ] ], then the line at time (t + 1) = the line at time t

On Stack Addition (3)

if Expression Stack at time t = [ [ ], [ [ function call with name: "__add__" and arguments: args, ys ], rest ] ], then the tab at time (t + 1) = the tab at time t

On Stack Addition (4)

if Expression Stack at time t = [ [ ], [ [ function call with name: "__add__" and arguments: args, ys ], rest ] ], then Variables Map at time (t + 1) = Variables Map at time t

On Stack Addition (5)

if Expression Stack at time t = [ [ ], [ [ function call with name: "__add__" and arguments: args, ys ], rest ] ], then Control Map at time (t + 1) = Control Map at time t

On Stack Addition (6)

if Expression Stack at time t = [ [ ], [ [ function call with name: "__add__" and arguments: args, ys ], rest ] ], then Python Object Store at time (t + 1) = Python Object Store at time t

On Stack Addition (7)

if Expression Stack at time t = [ [ ], [ [ function call with name: "__add__" and arguments: args, ys ], rest ] ], then Context Stack at time (t + 1) = Context Stack at time t

Perform Multiply

if the following are true:

Expression Stack at time t = [ [ ], [ [ function call with name: "__mul__" and arguments: args, ys ], rest ] ]
Value Stack at time t = [ [ a, [ b, [ ] ] ], [ next_level, other_levels ] ]

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

On Stack Multiply (1)

if Expression Stack at time t = [ [ ], [ [ function call with name: "__mul__" and arguments: args, ys ], rest ] ], then Expression Stack at time (t + 1) = [ ys, rest ]

On Stack Multiply (2)

if Expression Stack at time t = [ [ ], [ [ function call with name: "__mul__" and arguments: args, ys ], rest ] ], then the line at time (t + 1) = the line at time t

On Stack Multiply (3)

if Expression Stack at time t = [ [ ], [ [ function call with name: "__mul__" and arguments: args, ys ], rest ] ], then the tab at time (t + 1) = the tab at time t

On Stack Multiply (4)

if Expression Stack at time t = [ [ ], [ [ function call with name: "__mul__" and arguments: args, ys ], rest ] ], then Variables Map at time (t + 1) = Variables Map at time t

On Stack Multiply (5)

if Expression Stack at time t = [ [ ], [ [ function call with name: "__mul__" and arguments: args, ys ], rest ] ], then Control Map at time (t + 1) = Control Map at time t

On Stack Multiply (6)

if Expression Stack at time t = [ [ ], [ [ function call with name: "__mul__" and arguments: args, ys ], rest ] ], then Python Object Store at time (t + 1) = Python Object Store at time t

On Stack Multiply (7)

if Expression Stack at time t = [ [ ], [ [ function call with name: "__mul__" and arguments: args, ys ], rest ] ], then Context Stack at time (t + 1) = Context Stack at time t

Perform Stack Equality Call

if the following are true:

Expression Stack at time t = [ [ ], [ [ function call with name: "__eq__" and arguments: args, ys ], rest ] ]
Value Stack at time t = [ [ a, [ b, [ ] ] ], [ next_level, other_levels ] ]

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

On Stack Equal (1)

if Expression Stack at time t = [ [ ], [ [ function call with name: "__eq__" and arguments: args, ys ], rest ] ], then Expression Stack at time (t + 1) = [ ys, rest ]

On Stack Equal (2)

if Expression Stack at time t = [ [ ], [ [ function call with name: "__eq__" and arguments: args, ys ], rest ] ], then the line at time (t + 1) = the line at time t

On Stack Equal (3)

if Expression Stack at time t = [ [ ], [ [ function call with name: "__eq__" and arguments: args, ys ], rest ] ], then the tab at time (t + 1) = the tab at time t

On Stack Equal (4)

if Expression Stack at time t = [ [ ], [ [ function call with name: "__eq__" and arguments: args, ys ], rest ] ], then Variables Map at time (t + 1) = Variables Map at time t

On Stack Equal (5)

if Expression Stack at time t = [ [ ], [ [ function call with name: "__eq__" and arguments: args, ys ], rest ] ], then Control Map at time (t + 1) = Control Map at time t

On Stack Equal (6)

if Expression Stack at time t = [ [ ], [ [ function call with name: "__eq__" and arguments: args, ys ], rest ] ], then Python Object Store at time (t + 1) = Python Object Store at time t

On Stack Equal (7)

if Expression Stack at time t = [ [ ], [ [ function call with name: "__eq__" and arguments: args, ys ], rest ] ], then Context Stack at time (t + 1) = Context Stack at time t

Perform Stack Less Than

if the following are true:

Expression Stack at time t = [ [ ], [ [ function call with name: "__lt__" and arguments: args, ys ], rest ] ]
Value Stack at time t = [ [ a, [ b, [ ] ] ], [ next_level, other_levels ] ]

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

On Stack Less Than (1)

if Expression Stack at time t = [ [ ], [ [ function call with name: "__lt__" and arguments: args, ys ], rest ] ], then Expression Stack at time (t + 1) = [ ys, rest ]

On Stack Less Than (2)

if Expression Stack at time t = [ [ ], [ [ function call with name: "__lt__" and arguments: args, ys ], rest ] ], then the line at time (t + 1) = the line at time t

On Stack Less Than (3)

if Expression Stack at time t = [ [ ], [ [ function call with name: "__lt__" and arguments: args, ys ], rest ] ], then the tab at time (t + 1) = the tab at time t

On Stack Less Than (4)

if Expression Stack at time t = [ [ ], [ [ function call with name: "__lt__" and arguments: args, ys ], rest ] ], then Variables Map at time (t + 1) = Variables Map at time t

On Stack Less Than (5)

if Expression Stack at time t = [ [ ], [ [ function call with name: "__lt__" and arguments: args, ys ], rest ] ], then Control Map at time (t + 1) = Control Map at time t

On Stack Less Than (6)

if Expression Stack at time t = [ [ ], [ [ function call with name: "__lt__" and arguments: args, ys ], rest ] ], then Python Object Store at time (t + 1) = Python Object Store at time t

On Stack Less Than (7)

if Expression Stack at time t = [ [ ], [ [ function call with name: "__lt__" and arguments: args, ys ], rest ] ], then Context Stack at time (t + 1) = Context Stack at time t

Perform Stack Greater Than

if the following are true:

Expression Stack at time t = [ [ ], [ [ function call with name: "__gt__" and arguments: args, ys ], rest ] ]
Value Stack at time t = [ [ a, [ b, [ ] ] ], [ next_level, other_levels ] ]

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

On Stack Greater Than (1)

if Expression Stack at time t = [ [ ], [ [ function call with name: "__gt__" and arguments: args, ys ], rest ] ], then Expression Stack at time (t + 1) = [ ys, rest ]

On Stack Greater Than (2)

if Expression Stack at time t = [ [ ], [ [ function call with name: "__gt__" and arguments: args, ys ], rest ] ], then the line at time (t + 1) = the line at time t

On Stack Greater Than (3)

if Expression Stack at time t = [ [ ], [ [ function call with name: "__gt__" and arguments: args, ys ], rest ] ], then the tab at time (t + 1) = the tab at time t

On Stack Greater Than (4)

if Expression Stack at time t = [ [ ], [ [ function call with name: "__gt__" and arguments: args, ys ], rest ] ], then Variables Map at time (t + 1) = Variables Map at time t

On Stack Greater Than (5)

if Expression Stack at time t = [ [ ], [ [ function call with name: "__gt__" and arguments: args, ys ], rest ] ], then Control Map at time (t + 1) = Control Map at time t

On Stack Greater Than (6)

if Expression Stack at time t = [ [ ], [ [ function call with name: "__gt__" and arguments: args, ys ], rest ] ], then Python Object Store at time (t + 1) = Python Object Store at time t

On Stack Greater Than (7)

if Expression Stack at time t = [ [ ], [ [ function call with name: "__gt__" and arguments: args, ys ], rest ] ], then Context Stack at time (t + 1) = Context Stack at time t

Prepare For Function Call (1)

if the following are true:

Expression Stack at time t = [ [ ], [ [ function call with name: name and arguments: args, ys ], rest ] ]
Value Stack at time t = [ values, v_rest ]
there is a function named name with parameters params at line line
Parameters List at time t = None

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

Prepare For Function Call (2)

if the following are true:

Expression Stack at time t = [ [ ], [ [ function call with name: name and arguments: args, ys ], rest ] ]
Value Stack at time t = [ values, v_rest ]
there is a function named name with parameters params at line line
Parameters List at time t = None

then Argument Values at time (t + 1) = reverse of values

Prepare For Function Call (3)

if the following are true:

Expression Stack at time t = [ [ ], [ [ function call with name: name and arguments: args, ys ], rest ] ]
Value Stack at time t = [ values, v_rest ]
there is a function named name with parameters params at line line
Parameters List at time t = None

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

Pages: 14 15 16 ... 20