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.

Variable Unchanged (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

Assign If 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

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

Assign If 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

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

Assign If 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

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

Assign If 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

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

Assign 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 = x = c
c is constant

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:

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

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

Assign 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 = x = c
c is constant

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

Assign 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 = x = c
c is constant

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

Assign 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 = x = c
c is constant

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

Assign Constant (6)

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
c is constant

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

Assign 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 = c
c is a variable

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

Assign 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 = c
c is a variable

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

Assign 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 = c
c is a variable

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

Assign 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 = c
c is a variable

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

Assign 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 = c
c is a variable

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

Assign Variable (6)

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
c is a variable

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

Assign Call (1)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = assign statement with target x and expression (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

Assign Call (2)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = assign statement with target x and expression (function call with name: name and arguments: args)
expression state at time t = "not_expr"

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

Assign Call (3)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = assign statement with target x and expression (function call with name: name and arguments: args)
expression state at time t = "not_expr"

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

Assign Call (4)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = assign statement with target x and expression (function call with name: name and arguments: args)
expression state at time t = "not_expr"

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

Assign Call (5)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = assign statement with target x and expression (function call with name: name and arguments: args)
expression state at time t = "not_expr"

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

Assign Call (6)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = assign statement with target x and expression (function call with name: name and arguments: args)
expression state at time t = "not_expr"

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

Assign Call (7)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = assign statement with target x and expression (function call with name: name and arguments: args)
expression state at time t = "not_expr"

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

Assign Call (8)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = assign statement with target x and expression (function call with name: name and arguments: args)
expression state at time t = "not_expr"

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

Assign Call (9)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = assign statement with target x and expression (function call with name: name and arguments: args)
expression state at time t = "not_expr"

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

Assign Call (10)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = assign statement with target x and expression (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

Assign Call (11)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = assign statement with target x and expression (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

Insn Count Begin Expression (1)

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

Insn Count Begin Expression (2)

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

Insn Count Begin Expression (3)

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

Insn Count Begin Expression (4)

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

Insn Count Begin Expression (5)

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

Insn Count Begin Expression (6)

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

Insn Count Begin Expression (7)

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

Insn Count Begin Expression (8)

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

Evaluate Constant Argument State

if the following are true:

expression state at time t = "begin_expr"
the expression at time t = c
c is constant
parent stack at time t = [ x, y ]

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

Evaluate Constant State

if the following are true:

expression state at time t = "begin_expr"
the expression at time t = c
c is constant
parent stack at time t = [ ]

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

Evaluate Constant (1)

if the following are true:

expression state at time t = "begin_expr"
the expression at time t = c
c is constant

then Return Value at time (t + 1) = c

Evaluate Constant (2)

if the following are true:

expression state at time t = "begin_expr"
the expression at time t = c
c is constant

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

Evaluate Constant (3)

if the following are true:

expression state at time t = "begin_expr"
the expression at time t = c
c is constant

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

Evaluate Constant (4)

if the following are true:

expression state at time t = "begin_expr"
the expression at time t = c
c is constant

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

Evaluate Variable Argument State

if the following are true:

expression state at time t = "begin_expr"
the expression at time t = x
x is a variable
parent stack at time t = [ y, z ]

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

Evaluate Variable State

if the following are true:

expression state at time t = "begin_expr"
the expression at time t = v
v is a variable
parent stack at time t = [ ]

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

Evaluate Variable (1)

if the following are true:

expression state at time t = "begin_expr"
the expression at time t = v
v is a variable

then Return Value at time (t + 1) = value at x in map (Variables Map at time t)

Evaluate Variable (2)

if the following are true:

expression state at time t = "begin_expr"
the expression at time t = v
v is a variable

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

Evaluate Variable (3)

if the following are true:

expression state at time t = "begin_expr"
the expression at time t = v
v is a variable

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

Evaluate Variable (4)

if the following are true:

expression state at time t = "begin_expr"
the expression at time t = v
v is a variable

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

Begin Expr Call (1)

if the following are true:

expression state at time t = "begin_expr"
the expression at time t = function call with name: name and arguments: args

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

Begin Expr Call (2)

if the following are true:

expression state at time t = "begin_expr"
the expression at time t = function call with name: name and arguments: args

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

Begin Expr Call (3)

if the following are true:

expression state at time t = "begin_expr"
the expression at time t = function call with name: name and arguments: args

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

Begin Expr Call (4)

if the following are true:

expression state at time t = "begin_expr"
the expression at time t = function call with name: name and arguments: args

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

Iterate Insn (1)

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

Iterate Insn (2)

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

Iterate Insn (3)

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

Iterate Insn (4)

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

Iterate Insn (5)

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

Iterate Insn (6)

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

Iterate Insn (7)

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

Iterate Insn (8)

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

Do Iterage Args (1)

if the following are true:

expression state at time t = "iterate_args"
arguments stack at time t = [ [ x, y ], z ]

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

Do Iterage Args (2)

if the following are true:

expression state at time t = "iterate_args"
arguments stack at time t = [ [ x, y ], z ]

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

Do Iterage Args (3)

if the following are true:

expression state at time t = "iterate_args"
arguments stack at time t = [ [ x, y ], z ]

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

Do Iterage Args (4)

if the following are true:

expression state at time t = "iterate_args"
arguments stack at time t = [ [ x, y ], z ]

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

Iterate Args Empty (1)

if the following are true:

expression state at time t = "iterate_args"
arguments stack at time t = [ [ ], z ]
parent stack at time t = [ x, y ]

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

Iterate Args Empty (2)

if the following are true:

expression state at time t = "iterate_args"
arguments stack at time t = [ [ ], z ]
parent stack at time t = [ x, y ]

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

Iterate Args Empty (3)

if the following are true:

expression state at time t = "iterate_args"
arguments stack at time t = [ [ ], z ]
parent stack at time t = [ x, y ]

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

Iterate Args Empty (4)

if the following are true:

expression state at time t = "iterate_args"
arguments stack at time t = [ [ ], z ]
parent stack at time t = [ x, y ]

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

Assign Parent (1)

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

Assign Parent (2)

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

Assign Parent (3)

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

Assign Parent (4)

if expression state at time t = "call_function_begin", then Function Variables Map at time (t + 1) = [ ]

Assign Parent (5)

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

Assign Parent (6)

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

Assign Parent (7)

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

Assign Parent (8)

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

Assign Parent (9)

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

Assign Parent (10)

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

Call Func Add

if the following are true:

expression state at time t = "call_function_begin"
Value Stack at time t = [ [ a, [ b, [ ] ] ], stack ]
the expression at time t = function call with name: "__add__" and arguments: args

then Return Value at time (t + 1) = b + a

Call Add Return

if the following are true:

expression state at time t = "call_function_begin"
parent stack at time t = [ x, y ]
the expression at time t = function call with name: "__add__" and arguments: args

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

Call Add End

if the following are true:

expression state at time t = "call_function_begin"
parent stack at time t = [ ]
the expression at time t = function call with name: "__add__" and arguments: args

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

Call Add Object Store

if the following are true:

expression state at time t = "call_function_begin"
the expression at time t = function call with name: "__add__" and arguments: args

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

Call Func Multiply

if the following are true:

expression state at time t = "call_function_begin"
Value Stack at time t = [ [ a, [ b, [ ] ] ], stack ]
the expression at time t = function call with name: "__mul__" and arguments: args

then Return Value at time (t + 1) = b ⋅ a

Call Multiply Return

if the following are true:

expression state at time t = "call_function_begin"
parent stack at time t = [ x, y ]
the expression at time t = function call with name: "__mul__" and arguments: args

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

Call Multiply End

if the following are true:

expression state at time t = "call_function_begin"
parent stack at time t = [ ]
the expression at time t = function call with name: "__mul__" and arguments: args

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

Call Multiply Object Store

if the following are true:

expression state at time t = "call_function_begin"
the expression at time t = function call with name: "__mul__" and arguments: args

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

Call Function Equal

if the following are true:

expression state at time t = "call_function_begin"
Value Stack at time t = [ [ a, [ b, [ ] ] ], stack ]
the expression at time t = function call with name: "__eq__" and arguments: args

then Return Value at time (t + 1) = b = a

Call Equal Expr

if the following are true:

expression state at time t = "call_function_begin"
parent stack at time t = [ x, y ]
the expression at time t = function call with name: "__eq__" and arguments: args

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

Call Equal Expression Done

if the following are true:

expression state at time t = "call_function_begin"
parent stack at time t = [ ]
the expression at time t = function call with name: "__eq__" and arguments: args

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

Call Equal Object Store

if the following are true:

expression state at time t = "call_function_begin"
the expression at time t = function call with name: "__eq__" and arguments: args

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

Call Function Greater

if the following are true:

expression state at time t = "call_function_begin"
Value Stack at time t = [ [ a, [ b, [ ] ] ], stack ]
the expression at time t = function call with name: "__gt__" and arguments: args

then Return Value at time (t + 1) = b > a

Call Greater Expr

if the following are true:

expression state at time t = "call_function_begin"
parent stack at time t = [ x, y ]
the expression at time t = function call with name: "__gt__" and arguments: args

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

Call Greater Expression Done

if the following are true:

expression state at time t = "call_function_begin"
parent stack at time t = [ ]
the expression at time t = function call with name: "__gt__" and arguments: args

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

Call Greater Object Store

if the following are true:

expression state at time t = "call_function_begin"
the expression at time t = function call with name: "__gt__" and arguments: args

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

Call Function Less

if the following are true:

expression state at time t = "call_function_begin"
Value Stack at time t = [ [ a, [ b, [ ] ] ], stack ]
the expression at time t = function call with name: "__lt__" and arguments: args

then Return Value at time (t + 1) = b < a

Call Less Expr

if the following are true:

expression state at time t = "call_function_begin"
parent stack at time t = [ x, y ]
the expression at time t = function call with name: "__lt__" and arguments: args

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

Call Less Expression Done

if the following are true:

expression state at time t = "call_function_begin"
parent stack at time t = [ ]
the expression at time t = function call with name: "__lt__" and arguments: args

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

Call Less Object Store

if the following are true:

expression state at time t = "call_function_begin"
the expression at time t = function call with name: "__lt__" and arguments: args

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

Do Children Values (1)

if the following are true:

expression state at time t = "call_function_begin"
Value Stack at time t = [ values, stack ]
the expression at time t = function call with name: name and arguments: args

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

Do Children Values (2)

if the following are true:

expression state at time t = "call_function_begin"
Value Stack at time t = [ values, stack ]
the expression at time t = function call with name: name and arguments: args

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

Pages: 6 7 8 ... 20