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.

Begin PyList Elements (9)

if Expression Stack at time t = [ [ Python list elements, ys ], rest ], then Context Stack at time (t + 1) = Context Stack at time t

Call PyList (1)

if the following are true:

Expression Stack at time t = [ [ ], [ [ Python list elements, ys ], rest ] ]
Value Stack at time t = [ values, [ next_level, other_levels ] ]

then Value Stack at time (t + 1) = [ [ Python reference (length of stack (Python Object Store at time t)), next_level ], other_levels ]

Call PyList (2)

if the following are true:

Expression Stack at time t = [ [ ], [ [ Python list elements, ys ], rest ] ]
Value Stack at time t = [ values, [ next_level, other_levels ] ]

then Python Object Store at time (t + 1) = result of appending (Python list (reverse of values)) to (Python Object Store at time t)

Effect of Call Func List (1)

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

Effect of Call Func List (2)

if Expression Stack at time t = [ [ ], [ [ Python list elements, ys ], rest ] ], then the line at time (t + 1) = the line at time t

Effect of Call Func List (3)

if Expression Stack at time t = [ [ ], [ [ Python list elements, ys ], rest ] ], then the tab at time (t + 1) = the tab at time t

Effect of Call Func List (4)

if Expression Stack at time t = [ [ ], [ [ Python list elements, ys ], rest ] ], then Variables Map at time (t + 1) = Variables Map at time t

Effect of Call Func List (5)

if Expression Stack at time t = [ [ ], [ [ Python list elements, ys ], rest ] ], then Control Map at time (t + 1) = Control Map at time t

Effect of Call Func List (6)

if Expression Stack at time t = [ [ ], [ [ Python list elements, ys ], rest ] ], then Context Stack at time (t + 1) = Context Stack at time t

PyList 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 = Python list elements

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

PyList 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 = Python list elements

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

PyList 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 = Python list elements

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

Assign PyList To Target (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 (Python list elements)
Expression Stack at time t = [ ]

then Expression Stack at time (t + 1) = [ [ Python list elements, [ ] ], [ ] ]

Assign PyList To Target (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 (Python list elements)
Expression Stack at time t = [ ]

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

Assign PyList To Target (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 (Python list elements)
Expression Stack at time t = [ ]

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

Assign PyList To Target (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 (Python list elements)
Expression Stack at time t = [ ]

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

Assign PyList To Target (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 (Python list elements)
Expression Stack at time t = [ ]

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

Assign PyList To Target (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 (Python list elements)
Expression Stack at time t = [ ]

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

Assign PyList To Target (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 (Python list elements)
Expression Stack at time t = [ ]

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

Assign PyList To Target (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 (Python list elements)
Expression Stack at time t = [ ]

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

Begin Method 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 = obj_name.method_name(args)
Expression Stack at time t = [ ]

then Expression Stack at time (t + 1) = [ [ obj_name.method_name(args), [ ] ], [ ] ]

Begin Method 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 = obj_name.method_name(args)
Expression Stack at time t = [ ]

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

Begin Method 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 = obj_name.method_name(args)
Expression Stack at time t = [ ]

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

Begin Method 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 = obj_name.method_name(args)
Expression Stack at time t = [ ]

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

Begin Method 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 = obj_name.method_name(args)
Expression Stack at time t = [ ]

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

Begin Method 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 = obj_name.method_name(args)
Expression Stack at time t = [ ]

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

Begin Method 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 = obj_name.method_name(args)
Expression Stack at time t = [ ]

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

Begin Method 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 = obj_name.method_name(args)
Expression Stack at time t = [ ]

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

Class defs on method Call

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = obj_name.method_name(args)

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

Begin Assign Method 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 target and expression (obj_name.method_name(args))
Expression Stack at time t = [ ]

then Expression Stack at time (t + 1) = [ [ obj_name.method_name(args), [ ] ], [ ] ]

Begin Assign Method 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 target and expression (obj_name.method_name(args))
Expression Stack at time t = [ ]

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

Begin Assign Method 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 target and expression (obj_name.method_name(args))
Expression Stack at time t = [ ]

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

Begin Assign Method 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 target and expression (obj_name.method_name(args))
Expression Stack at time t = [ ]

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

Begin Assign Method 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 target and expression (obj_name.method_name(args))
Expression Stack at time t = [ ]

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

Begin Assign Method 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 target and expression (obj_name.method_name(args))
Expression Stack at time t = [ ]

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

Begin Assign Method 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 target and expression (obj_name.method_name(args))
Expression Stack at time t = [ ]

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

Begin Assign Method 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 target and expression (obj_name.method_name(args))
Expression Stack at time t = [ ]

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

Evaluate Method Arguments (1)

if Expression Stack at time t = [ [ obj_name.method_name(args), ys ], rest ], then Expression Stack at time (t + 1) = [ args, [ [ obj_name.method_name(args), ys ], rest ] ]

Evaluate Method Arguments (2)

if Expression Stack at time t = [ [ obj_name.method_name(args), ys ], rest ], then Value Stack at time (t + 1) = [ [ ], Value Stack at time t ]

Evaluate Method Arguments (3)

if Expression Stack at time t = [ [ obj_name.method_name(args), ys ], rest ], then Parameters List at time (t + 1) = None

Evaluate Method Arguments (4)

if Expression Stack at time t = [ [ obj_name.method_name(args), ys ], rest ], then the line at time (t + 1) = the line at time t

Evaluate Method Arguments (5)

if Expression Stack at time t = [ [ obj_name.method_name(args), ys ], rest ], then the tab at time (t + 1) = the tab at time t

Evaluate Method Arguments (6)

if Expression Stack at time t = [ [ obj_name.method_name(args), ys ], rest ], then Variables Map at time (t + 1) = Variables Map at time t

Evaluate Method Arguments (7)

if Expression Stack at time t = [ [ obj_name.method_name(args), ys ], rest ], then Control Map at time (t + 1) = Control Map at time t

Evaluate Method Arguments (8)

if Expression Stack at time t = [ [ obj_name.method_name(args), ys ], rest ], then Python Object Store at time (t + 1) = Python Object Store at time t

Evaluate Method Arguments (9)

if Expression Stack at time t = [ [ obj_name.method_name(args), ys ], rest ], then Context Stack at time (t + 1) = Context Stack at time t

Append Value (1)

if the following are true:

Expression Stack at time t = [ [ ], [ [ obj.append(x), ys ], rest ] ]
Value Stack at time t = [ [ value, [ ] ], [ next_level, other_levels ] ]
value at obj in map (Variables Map at time t) = Python reference idx
the element at index idx of stack (Python Object Store at time t) = Python list entries

then Python Object Store at time (t + 1) = result of storing (Python list (result of appending value to entries)) at index idx of stack (Python Object Store at time t)

Append Value (2)

if the following are true:

Expression Stack at time t = [ [ ], [ [ obj.append(x), ys ], rest ] ]
Value Stack at time t = [ [ value, [ ] ], [ next_level, other_levels ] ]
value at obj in map (Variables Map at time t) = Python reference idx
the element at index idx of stack (Python Object Store at time t) = Python list entries

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

When Method Call Is Evaluated (1)

if Expression Stack at time t = [ [ ], [ [ obj.append(x), ys ], rest ] ], then Expression Stack at time (t + 1) = [ ys, rest ]

When Method Call Is Evaluated (2)

if Expression Stack at time t = [ [ ], [ [ obj.append(x), ys ], rest ] ], then the line at time (t + 1) = the line at time t

When Method Call Is Evaluated (3)

if Expression Stack at time t = [ [ ], [ [ obj.append(x), ys ], rest ] ], then the tab at time (t + 1) = the tab at time t

When Method Call Is Evaluated (4)

if Expression Stack at time t = [ [ ], [ [ obj.append(x), ys ], rest ] ], then Variables Map at time (t + 1) = Variables Map at time t

When Method Call Is Evaluated (5)

if Expression Stack at time t = [ [ ], [ [ obj.append(x), ys ], rest ] ], then Control Map at time (t + 1) = Control Map at time t

When Method Call Is Evaluated (6)

if Expression Stack at time t = [ [ ], [ [ obj.append(x), ys ], rest ] ], then Context Stack at time (t + 1) = Context Stack at time t

End Method 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 = obj.name(el)
Expression Stack at time t = [ [ ], [ ] ]

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

End Method 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 = obj.name(el)
Expression Stack at time t = [ [ ], [ ] ]

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

End Method 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 = obj.name(el)
Expression Stack at time t = [ [ ], [ ] ]

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

End Method 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 = obj.name(el)
Expression Stack at time t = [ [ ], [ ] ]

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

End Method 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 = obj.name(el)
Expression Stack at time t = [ [ ], [ ] ]

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

End Method 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 = obj.name(el)
Expression Stack at time t = [ [ ], [ ] ]

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

object store on getitem

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: "__getitem__" and arguments: args
Expression Stack at time t = [ ]

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

Call Get Item

if the following are true:

Expression Stack at time t = [ [ ], [ [ function call with name: "__getitem__" and arguments: args, ys ], rest ] ]
Value Stack at time t = [ [ a, [ Python reference idx, [ ] ] ], [ next_level, other_levels ] ]
the element at index idx of stack (Python Object Store at time t) = Python list entries

then Value Stack at time (t + 1) = [ [ the element at index a of stack entries, next_level ], other_levels ]

When getitem Is Evaluated (1)

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

When getitem Is Evaluated (2)

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

When getitem Is Evaluated (3)

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

When getitem Is Evaluated (4)

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

When getitem Is Evaluated (5)

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

When getitem Is Evaluated (6)

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

Object Store on get length

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: "len" and arguments: args
Expression Stack at time t = [ ]

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

Get PyList Length

if the following are true:

Value Stack at time t = [ [ Python reference idx, [ ] ], [ next_level, other_levels ] ]
Expression Stack at time t = [ [ ], [ [ function call with name: "len" and arguments: args, ys ], rest ] ]
the element at index idx of stack (Python Object Store at time t) = Python list entries

then Value Stack at time (t + 1) = [ [ length of stack entries, next_level ], other_levels ]

When len Is Evaluated (1)

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

When len Is Evaluated (2)

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

When len Is Evaluated (3)

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

When len Is Evaluated (4)

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

When len Is Evaluated (5)

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

When len Is Evaluated (6)

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

Pop from pylist objects (1)

if the following are true:

Value Stack at time t = [ [ a, [ ] ], [ next_level, other_levels ] ]
Expression Stack at time t = [ [ ], [ [ name."pop"(args), ys ], rest ] ]
value at name in map (Variables Map at time t) = Python reference idx
the element at index idx of stack (Python Object Store at time t) = Python list entries

then Python Object Store at time (t + 1) = result of storing (Python list (stack after popping a value from stack entries at index a)) at index idx of stack (Python Object Store at time t)

Pop from pylist objects (2)

if the following are true:

Value Stack at time t = [ [ a, [ ] ], [ next_level, other_levels ] ]
Expression Stack at time t = [ [ ], [ [ name."pop"(args), ys ], rest ] ]
value at name in map (Variables Map at time t) = Python reference idx
the element at index idx of stack (Python Object Store at time t) = Python list entries

then Value Stack at time (t + 1) = [ [ the element at index a of stack entries, next_level ], other_levels ]

Do Python Pop (1)

if Expression Stack at time t = [ [ ], [ [ name."pop"(args), ys ], rest ] ], then Expression Stack at time (t + 1) = [ ys, rest ]

Do Python Pop (2)

if Expression Stack at time t = [ [ ], [ [ name."pop"(args), ys ], rest ] ], then the line at time (t + 1) = the line at time t

Do Python Pop (3)

if Expression Stack at time t = [ [ ], [ [ name."pop"(args), ys ], rest ] ], then the tab at time (t + 1) = the tab at time t

Do Python Pop (4)

if Expression Stack at time t = [ [ ], [ [ name."pop"(args), ys ], rest ] ], then Variables Map at time (t + 1) = Variables Map at time t

Do Python Pop (5)

if Expression Stack at time t = [ [ ], [ [ name."pop"(args), ys ], rest ] ], then Control Map at time (t + 1) = Control Map at time t

Do Python Pop (6)

if Expression Stack at time t = [ [ ], [ [ name."pop"(args), ys ], rest ] ], then Context Stack at time (t + 1) = Context Stack at time t

Object Store on contains

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: "__contains__" and arguments: args
Expression Stack at time t = [ ]

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

Call Parent Contains Item

if the following are true:

Value Stack at time t = [ [ a, [ Python reference idx, [ ] ] ], [ next_level, other_levels ] ]
Expression Stack at time t = [ [ ], [ [ function call with name: "__contains__" and arguments: args, ys ], rest ] ]
the element at index idx of stack (Python Object Store at time t) = Python list entries

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

When Contains Call Is Evaluated (1)

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

When Contains Call Is Evaluated (2)

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

When Contains Call Is Evaluated (3)

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

When Contains Call Is Evaluated (4)

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

When Contains Call Is Evaluated (5)

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

When Contains Call Is Evaluated (6)

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

Begin PyDict (1)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = Python dictionary entries
Expression Stack at time t = [ ]

then Expression Stack at time (t + 1) = [ [ Python dictionary entries, [ ] ], [ ] ]

Begin PyDict (2)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = Python dictionary entries
Expression Stack at time t = [ ]

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

Begin PyDict (3)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = Python dictionary entries
Expression Stack at time t = [ ]

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

Begin PyDict (4)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = Python dictionary entries
Expression Stack at time t = [ ]

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

Begin PyDict (5)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = Python dictionary entries
Expression Stack at time t = [ ]

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

Begin PyDict (6)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = Python dictionary entries
Expression Stack at time t = [ ]

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

Begin PyDict Elements (1)

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

Begin PyDict Elements (2)

if Expression Stack at time t = [ [ Python dictionary entries, ys ], rest ], then Value Stack at time (t + 1) = [ [ ], Value Stack at time t ]

1 2 3