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.

Else Unchanged (1)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = else:

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

Else Unchanged (2)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = else:

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

Else Unchanged (3)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = else:

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

Else Unchanged (4)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = else:

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

Else 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 = else:

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

Else Unchanged (6)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = else:

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

Else Unchanged (7)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = else:

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

Else Unchanged (8)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = else:

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

Decrement Tab (1)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab k = s
k < j
value at (j - 1) in map (Control Map at time t) = pair ("if", if_value)

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

Decrement Tab (2)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab k = s
k < j
value at (j - 1) in map (Control Map at time t) = pair ("if", if_value)

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

Decrement Tab (3)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab k = s
k < j
value at (j - 1) in map (Control Map at time t) = pair ("if", if_value)

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

Decrement Tab (4)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab k = s
k < j
value at (j - 1) in map (Control Map at time t) = pair ("if", if_value)

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

Decrement Tab (5)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab k = s
k < j
value at (j - 1) in map (Control Map at time t) = pair ("if", if_value)

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

Decrement Tab (6)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab k = s
k < j
value at (j - 1) in map (Control Map at time t) = pair ("if", if_value)

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

Decrement Tab (7)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab k = s
k < j
value at (j - 1) in map (Control Map at time t) = pair ("if", if_value)

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

While 1 (1)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = "while" statement with condition (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

While 1 (2)

if the following are true:

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

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

While 1 (3)

if the following are true:

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

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

While 1 (4)

if the following are true:

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

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

While 1 (5)

if the following are true:

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

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

While 1 (6)

if the following are true:

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

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

While 1 (7)

if the following are true:

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

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

While 1 (8)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = "while" statement with condition (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

While 1 (9)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = "while" statement with condition (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

While Unchanged (1)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = "while" statement with condition (function call with name: name and arguments: args)

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

While Unchanged (2)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = "while" statement with condition (function call with name: name and arguments: args)

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

While Unchanged (3)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = "while" statement with condition (function call with name: name and arguments: args)

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

While Unchanged (4)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = "while" statement with condition (function call with name: name and arguments: args)

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

While 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 = "while" statement with condition (function call with name: name and arguments: args)

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

While 2 (1)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = "while" statement with condition (function call with name: name and arguments: args)
expression state at time t = "end_expr"

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

While 2 (2)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = "while" statement with condition (function call with name: name and arguments: args)
expression state at time t = "end_expr"

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

While 2 (3)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = "while" statement with condition (function call with name: name and arguments: args)
expression state at time t = "end_expr"

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

While Go (1)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = "while" statement with condition (function call with name: name and arguments: args)
expression state at time t = "end_expr"
Return Value at time t = True

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

While Go (2)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = "while" statement with condition (function call with name: name and arguments: args)
expression state at time t = "end_expr"
Return Value at time t = True

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

While False (1)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = "while" statement with condition (function call with name: name and arguments: args)
expression state at time t = "end_expr"
Return Value at time t = False

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

While False (2)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = "while" statement with condition (function call with name: name and arguments: args)
expression state at time t = "end_expr"
Return Value at time t = False

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

In Break Statement (1)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = break

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

In Break Statement (2)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = break

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

In Break Statement (3)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = break

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

In Break Statement (4)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = break

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

In Break Statement (5)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = break

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

In Break Statement (6)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = break

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

In Break Statement (7)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = break

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

In Break Statement (8)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = break

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

In Break Statement (9)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = break

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

In Continue Statement (1)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = continue

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

In Continue Statement (2)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = continue

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

In Continue Statement (3)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = continue

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

In Continue Statement (4)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = continue

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

In Continue Statement (5)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = continue

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

In Continue Statement (6)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = continue

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

In Continue Statement (7)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = continue

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

In Continue Statement (8)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = continue

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

In Continue Statement (9)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = continue

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

In Continue Statement (10)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = continue

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

In Continue Statement (11)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = continue

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

Function Definition (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 definition where name: name and parameters: params

then there is a function named name with parameters params at line line

Function Definition (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 definition where name: name and parameters: params

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

Function Definition (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 definition where name: name and parameters: params

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

Function Definition (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 definition where name: name and parameters: params

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

Function Definition (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 definition where name: name and parameters: params

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

Function Definition (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 definition where name: name and parameters: params

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

Function Definition (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 definition where name: name and parameters: params

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

Function Definition (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 definition where name: name and parameters: params

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

Function Definition (9)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = function definition where name: name and parameters: params

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

Function Definition (10)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = function definition where name: name and parameters: params

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

Return 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 = return v

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

Return 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 = return v

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

Return 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 = return v

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

Constant object

if the following are true:

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

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

Variable Object

if the following are true:

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

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

Return Statement State (1)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = return rex
expression state at time t = "not_expr"

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

Return Statement State (2)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = return rex
expression state at time t = "not_expr"

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

Return Statement State (3)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = return rex
expression state at time t = "not_expr"

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

Return Statement State (4)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = return rex
expression state at time t = "not_expr"

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

Return Statement State (5)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = return rex
expression state at time t = "not_expr"

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

Return Statement State (6)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = return rex
expression state at time t = "not_expr"

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

Return Statement State (7)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = return rex
expression state at time t = "not_expr"

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

Return Statement State (8)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = return rex
expression state at time t = "not_expr"

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

Return Statement State (9)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = return rex
expression state at time t = "not_expr"

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

Return Statement State (10)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = return rex
expression state at time t = "not_expr"

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

Return Statement State (11)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = return rex
expression state at time t = "not_expr"

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

Function Call Pop 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 = return rex
stack at time t = [ program context with variables: varis and expression state: (expression state with parent stack: parent_stack arguments: arg_stack values: value_stack line: line tab: tab) and control map: control_map, rest ]
expression state at time t = "end_expr"

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

Function Call Pop 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 = return rex
stack at time t = [ program context with variables: varis and expression state: (expression state with parent stack: parent_stack arguments: arg_stack values: value_stack line: line tab: tab) and control map: control_map, rest ]
expression state at time t = "end_expr"

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

Function Call Pop 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 = return rex
stack at time t = [ program context with variables: varis and expression state: (expression state with parent stack: parent_stack arguments: arg_stack values: value_stack line: line tab: tab) and control map: control_map, rest ]
expression state at time t = "end_expr"

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

Function Call Pop 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 = return rex
stack at time t = [ program context with variables: varis and expression state: (expression state with parent stack: parent_stack arguments: arg_stack values: value_stack line: line tab: tab) and control map: control_map, rest ]
expression state at time t = "end_expr"

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

Function Call Pop 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 = return rex
stack at time t = [ program context with variables: varis and expression state: (expression state with parent stack: parent_stack arguments: arg_stack values: value_stack line: line tab: tab) and control map: control_map, rest ]
expression state at time t = "end_expr"

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

Function Call Pop 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 = return rex
stack at time t = [ program context with variables: varis and expression state: (expression state with parent stack: parent_stack arguments: arg_stack values: value_stack line: line tab: tab) and control map: control_map, rest ]
expression state at time t = "end_expr"

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

Function Call Pop 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 = return rex
stack at time t = [ program context with variables: varis and expression state: (expression state with parent stack: parent_stack arguments: arg_stack values: value_stack line: line tab: tab) and control map: control_map, rest ]
expression state at time t = "end_expr"

then stack at time (t + 1) = rest

Function Call Pop 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 = return rex
stack at time t = [ program context with variables: varis and expression state: (expression state with parent stack: parent_stack arguments: arg_stack values: value_stack line: line tab: tab) and control map: control_map, rest ]
expression state at time t = "end_expr"

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

Function Call Pop Stack (9)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = return rex
stack at time t = [ program context with variables: varis and expression state: (expression state with parent stack: parent_stack arguments: arg_stack values: value_stack line: line tab: tab) and control map: control_map, rest ]
expression state at time t = "end_expr"

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

Function Call Pop Stack (10)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = return rex
stack at time t = [ program context with variables: varis and expression state: (expression state with parent stack: parent_stack arguments: arg_stack values: value_stack line: line tab: tab) and control map: control_map, rest ]
expression state at time t = "end_expr"

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

Returning Property

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = return rex
expression state at time t = "end_expr"

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

Call End Object

if the following are true:

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

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

Not expression

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

Computer ADDI Instruction, Concise

if the following are true:

the instruction at computer c and index i = an ADDI instruction with src: src imm: imm and dst: dst
the PC at computer c and time t = i

then byte at ID: c, cell #dst at time (t + 1) = (byte at ID: c, cell #src at time t) + imm

Computer ADDI Instruction, Others

if the following are true:

the instruction at computer c and index i = an ADDI instruction with src: src imm: imm and dst: dst
the PC at computer c and time t = i
not (other = dst)

then byte at ID: c, cell #other at time (t + 1) = byte at ID: c, cell #other at time t

Computer SUBTRACTI Instruction

if the following are true:

the instruction at computer c and index i = subtract immediate instruction with dst: dst src: src and immediate: imm
the PC at computer c and time t = i

then byte at ID: c, cell #dst at time (t + 1) = (byte at ID: c, cell #src at time t) - imm

Computer SUBTRACTI Instruction, Others

if the following are true:

the instruction at computer c and index i = subtract immediate instruction with dst: dst src: src and immediate: imm
the PC at computer c and time t = i
not (other = dst)

then byte at ID: c, cell #other at time (t + 1) = byte at ID: c, cell #other at time t

Computer ADD Instruction

if the following are true:

the instruction at computer c and index i = an add instruction with dst: d src1: s1 and src2: s2
the PC at computer c and time t = i

then byte at ID: c, cell #d at time (t + 1) = (byte at ID: c, cell #s1 at time t) + (byte at ID: c, cell #s2 at time t)

8 9 10