Conditional Properties

• 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
• not (other = d)

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

• the instruction at computer c and index i = a STORE instruction with src: src address: addr and immediate: imm
• the PC at computer c and time t = i

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

• the instruction at computer c and index i = a STORE instruction with src: src address: addr and immediate: imm
• the PC at computer c and time t = i
• not (other = (byte at ID: c, cell #addr at time t) + imm)

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

• the instruction at computer c and index i = a LOAD instruction with dst: dst addr: addr and imm: 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 #((byte at ID: c, cell #addr at time t) + imm) at time t

• the instruction at computer c and index i = a LOAD instruction with dst: dst addr: addr and imm: 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

• the instruction at computer c and index i = a BEQ instruction that compares l and r with immediate imm
• the PC at computer c and time t = i

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

• the instruction at computer c and index i = a BEQ instruction that compares left and right with immediate imm
• the PC at computer c and time t = i
• byte at ID: c, cell #left at time t = byte at ID: c, cell #right at time t

then the PC at computer c and time (t + 1) = (i + 1) + imm

• the instruction at computer c and index i = a BEQ instruction that compares left and right with immediate imm
• the PC at computer c and time t = i
• not (byte at ID: c, cell #left at time t = byte at ID: c, cell #right at time t)

then the PC at computer c and time (t + 1) = i + 1

• the instruction at computer c and index i = a jump instruction with to: jump_to
• the PC at computer c and time t = i

then the PC at computer c and time (t + 1) = jump_to

• the instruction at computer c and index i = a jump instruction with to: jump_to
• the PC at computer c and time t = i

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

• the instruction at computer c and index i = jump register instruction with addr: addr
• the PC at computer c and time t = i

then the PC at computer c and time (t + 1) = byte at ID: c, cell #addr at time t

• the instruction at computer c and index i = jump register instruction with addr: addr
• the PC at computer c and time t = i

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

• the instruction at computer c and index i = JAL instruction with jump to: jump_to
• the PC at computer c and time t = i

then the PC at computer c and time (t + 1) = jump_to

• the instruction at computer c and index i = JAL instruction with jump to: jump_to
• the PC at computer c and time t = i
• not (x = 2)

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

• the instruction at computer c and index i = JAL instruction with jump to: jump_to
• the PC at computer c and time t = i

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

• the instruction at computer c and index x = an ADDI instruction with src: d imm: imm and dst: s
• the PC at computer c and time t = x

then the PC at computer c and time (t + 1) = x + 1

• the instruction at computer c and index x = an add instruction with dst: s src1: d and src2: imm
• the PC at computer c and time t = x

then the PC at computer c and time (t + 1) = x + 1

• the instruction at computer c and index x = subtract immediate instruction with dst: s src: d and immediate: imm
• the PC at computer c and time t = x

then the PC at computer c and time (t + 1) = x + 1

• the instruction at computer c and index x = a STORE instruction with src: s address: d and immediate: imm
• the PC at computer c and time t = x

then the PC at computer c and time (t + 1) = x + 1

• the instruction at computer c and index x = a LOAD instruction with dst: s addr: d and imm: imm
• the PC at computer c and time t = x

then the PC at computer c and time (t + 1) = x + 1

• byte at ID: c, cell #27 at time t = 1
• number of characters read at t < byte at ID: c, cell #26 at time t

then display text at x: (cursor x at time t), y: (cursor y at time t), and time: (t + 1) = byte at ID: c, cell #(10 + (number of characters read at t)) at time t

• byte at ID: c, cell #27 at time t = 1
• number of characters read at t < byte at ID: c, cell #26 at time t

then number of characters read at (t + 1) = (number of characters read at t) + 1

• byte at ID: c, cell #27 at time t = 1
• number of characters read at t = byte at ID: c, cell #26 at time t

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

• byte at ID: c, cell #27 at time t = 1
• number of characters read at t = byte at ID: c, cell #26 at time t

then number of characters read at (t + 1) = 0

• byte at ID: c, cell #27 at time t = 1
• number of characters read at t = byte at ID: c, cell #26 at time t

then cursor x at time (t + 1) = cursor x at time t

• byte at ID: c, cell #27 at time t = 1
• number of characters read at t = byte at ID: c, cell #26 at time t

then cursor y at time (t + 1) = cursor y at time t

• byte at ID: c, cell #27 at time t = 1
• cursor x at time t < 39

then cursor x at time (t + 1) = (cursor x at time t) + 1

• byte at ID: c, cell #27 at time t = 1
• cursor x at time t < 39

then cursor y at time (t + 1) = cursor y at time t

• byte at ID: c, cell #27 at time t = 1
• cursor x at time t = 39

then cursor x at time (t + 1) = 0

• byte at ID: c, cell #27 at time t = 1
• cursor x at time t = 39
• cursor y at time t < 11

then cursor y at time (t + 1) = (cursor y at time t) + 1

• byte at ID: c, cell #27 at time t = 1
• cursor x at time t = 39
• cursor y at time t = 11

then display text at x: x, y: y, and time: (t + 1) = display text at x: x, y: (y + 1), and time: t

• byte at ID: c, cell #27 at time t = 1
• byte at ID: c, cell #(10 + (number of characters read at t)) at time t = 13

then cursor x at time (t + 1) = 0

• byte at ID: c, cell #27 at time t = 1
• byte at ID: c, cell #(10 + (number of characters read at t)) at time t = 13
• cursor y at time t < 11

then cursor y at time (t + 1) = (cursor y at time t) + 1

• byte at ID: c, cell #27 at time t = 1
• byte at ID: c, cell #(10 + (number of characters read at t)) at time t = 13
• cursor y at time t = 11

then cursor y at time (t + 1) = cursor y at time t

• byte at ID: c, cell #27 at time t = 1
• byte at ID: c, cell #(10 + (number of characters read at t)) at time t = 13
• cursor y at time t = 11

then display text at x: x, y: y, and time: (t + 1) = display text at x: x, y: (y + 1), and time: t

• byte at ID: c, cell #49 at time t = 1
• byte at ID: c, cell #48 at time t = 1
• disk bytes read at time t < byte at ID: c, cell #46 at time t

then disk byte at index: ((value of cell 47 at time t) + (disk bytes read at time t)) time: (t + 1) = value of cell (30 + (disk bytes read at time t)) at time t

• byte at ID: c, cell #49 at time t = 1
• byte at ID: c, cell #48 at time t = 1
• not (index = (byte at ID: c, cell #47 at time t) + (disk bytes read at time t))

then disk byte at index: index time: (t + 1) = disk byte at index: index time: t

• byte at ID: c, cell #49 at time t = 1
• disk bytes read at time t < byte at ID: c, cell #46 at time t

then disk bytes read at time (t + 1) = (disk bytes read at time t) + 1

• byte at ID: c, cell #49 at time t = 1
• disk bytes read at time t = byte at ID: c, cell #46 at time t

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

• byte at ID: c, cell #49 at time t = 1
• disk bytes read at time t = byte at ID: c, cell #46 at time t

then disk bytes read at time (t + 1) = 0

• byte at ID: c, cell #49 at time t = 1
• disk bytes read at time t = byte at ID: c, cell #46 at time t

then disk byte at index: index time: (t + 1) = disk byte at index: index time: t

• byte at ID: c, cell #49 at time t = 1
• byte at ID: c, cell #48 at time t = 0
• disk bytes read at time t < byte at ID: c, cell #46 at time t

then byte at ID: c, cell #(30 + (disk bytes read at time t)) at time (t + 1) = disk byte at index: ((byte at ID: c, cell #47 at time t) + (disk bytes read at time t)) time: t

• byte at ID: c, cell #49 at time t = 1
• disk bytes read at time t = byte at ID: c, cell #46 at time t
• byte at ID: c, cell #48 at time t = 0

then interrupt at computer: c index: 1 time: (t + 1) = 1

• byte at ID: c, cell #49 at time t = 1
• byte at ID: c, cell #48 at time t = 0

then disk byte at index: index time: (t + 1) = disk byte at index: index time: t

• byte at ID: x, cell #68 at time t = 1
• byte at ID: x, cell #67 at time t = y_decimal
• y in decimal = y_decimal
• network bytes read from computer: x at time t < byte at ID: x, cell #66 at time t

then byte at ID: y, cell #(50 + (network bytes read from computer: x at time t)) at time (t + 1) = byte at ID: x, cell #(50 + (network bytes read from computer: x at time t)) at time t

• byte at ID: x, cell #68 at time t = 1
• byte at ID: x, cell #67 at time t = y_decimal
• y in decimal = y_decimal
• network bytes read from computer: x at time t < byte at ID: x, cell #66 at time t

then network bytes read from computer: x at time (t + 1) = (network bytes read from computer: x at time t) + 1

• byte at ID: x, cell #68 at time t = 1
• byte at ID: x, cell #67 at time t = y_decimal
• y in decimal = y_decimal
• network bytes read from computer: x at time t = byte at ID: x, cell #66 at time t

then interrupt at computer: y index: 2 time: (t + 1) = 1

• byte at ID: x, cell #68 at time t = 1
• byte at ID: x, cell #67 at time t = y_decimal
• y in decimal = y_decimal
• network bytes read from computer: x at time t = byte at ID: x, cell #66 at time t

then byte at ID: x, cell #68 at time (t + 1) = 0

• byte at ID: x, cell #68 at time t = 1
• byte at ID: x, cell #67 at time t = y_decimal
• y in decimal = y_decimal
• network bytes read from computer: x at time t = byte at ID: x, cell #66 at time t

then network bytes read from computer: x at time (t + 1) = 0

• byte at ID: x, cell #68 at time t = 1
• byte at ID: x, cell #67 at time t = y_decimal
• y in decimal = y_decimal
• network bytes read from computer: x at time t = byte at ID: x, cell #66 at time t

then byte at ID: y, cell #66 at time (t + 1) = byte at ID: x, cell #66 at time t

• the line at time t = i
• the tab at time t = j
• statement at line i, tab j = Python list elements
• expression state at time t = "not_expr"

then the expression 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 = Python list elements
• expression state at time t = "not_expr"

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

• the line at time t = i
• the tab at time t = j
• statement at line i, tab j = Python list elements
• expression state at time t = "not_expr"

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 list elements
• expression state at time t = "not_expr"

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 list elements
• expression state at time t = "not_expr"

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 list elements
• expression state at time t = "not_expr"

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

• the line at time t = i
• the tab at time t = j
• statement at line i, tab j = Python list elements
• expression state at time t = "not_expr"

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

• the line at time t = i
• the tab at time t = j
• statement at line i, tab j = Python list elements
• expression state at time t = "not_expr"

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 list elements
• expression state at time t = "not_expr"

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

• expression state at time t = "begin_expr"
• the expression at time t = Python list elements

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

• expression state at time t = "begin_expr"
• the expression at time t = Python list elements

then parent stack at time (t + 1) = [ Python list elements, parent stack at time t ]

• expression state at time t = "begin_expr"
• the expression at time t = Python list elements

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

• expression state at time t = "begin_expr"
• the expression at time t = Python list elements

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

• expression state at time t = "call_function_begin"
• Value Stack at time t = [ values, stack ]
• the expression at time t = Python list elements

then Return Value at time (t + 1) = Python reference (length of stack (Python Object Store at time t))

• expression state at time t = "call_function_begin"
• Value Stack at time t = [ values, stack ]
• the expression at time t = Python list elements

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

• expression state at time t = "call_function_begin"
• Value Stack at time t = [ values, stack ]
• the expression at time t = Python list elements

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

• expression state at time t = "call_function_begin"
• parent stack at time t = [ x, y ]
• the expression at time t = Python list elements

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

• expression state at time t = "call_function_begin"
• parent stack at time t = [ ]
• the expression at time t = Python list elements

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

• 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 stack at time (t + 1) = 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 "if" map at time (t + 1) = "if" 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 'while stack' at time (t + 1) = 'while 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 state at time t = "not_expr"

then the expression 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 state at time t = "not_expr"

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

• 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 state at time t = "not_expr"

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 state at time t = "not_expr"

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 state at time t = "not_expr"

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 state at time t = "not_expr"

then stack at time (t + 1) = 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 state at time t = "not_expr"

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 state at time t = "not_expr"

then parent 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 state at time t = "not_expr"

then arguments 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 state at time t = "not_expr"

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 state at time t = "not_expr"

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 x and expression (Python list elements)
• expression state at time t = "end_expr"

then Variables Map at time (t + 1) = result of storing (Return Value at time t) at key: x in map: (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 state at time t = "end_expr"

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 = assign statement with target x and expression (Python list elements)
• expression state at time t = "end_expr"

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 = assign statement with target x and expression (Python list elements)
• expression state at time t = "end_expr"

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