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.
- 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