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.
- 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 ]
- 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)
- 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
- 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
- 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
- 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, [ ] ], [ ] ]
- 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
- 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
- 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
- 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
- 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) = [ [ ], [ ] ]
- 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
- 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
- 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), [ ] ], [ ] ]
- 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
- 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
- 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) = [ [ ], [ ] ]
- 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
- 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
- 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
- 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
- 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
- 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), [ ] ], [ ] ]
- 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
- 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
- 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) = [ [ ], [ ] ]
- 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
- 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
- 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
- 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
- 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)
- 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 ]
obj.append(x)
, ys ], rest ] ], then Expression Stack at time (t + 1) = [ ys, rest ]obj.append(x)
, ys ], rest ] ], then the line at time (t + 1) = the line at time tobj.append(x)
, ys ], rest ] ], then the tab at time (t + 1) = the tab at time tobj.append(x)
, ys ], rest ] ], then Variables Map at time (t + 1) = Variables Map at time tobj.append(x)
, ys ], rest ] ], then Control Map at time (t + 1) = Control Map at time tobj.append(x)
, ys ], rest ] ], then Context Stack at time (t + 1) = Context Stack at time t- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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 ]
- 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
- 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 ]
- 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)
- 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 ]
- 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
- 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 ]
- 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, [ ] ], [ ] ]
- 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
- 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
- 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) = [ [ ], [ ] ]
- 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
- 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