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.
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
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
if expression state at time t = "end_expr", then expression state at time (t + 1) = "not_expr"
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
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
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
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
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)
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
- not (other = d)
then byte at ID: c, cell #other at time (t + 1) = byte at ID: c, cell #other at time t
if the following are true:
- 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
if the following are true:
- 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
if the following are true:
- 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
if the following are true:
- 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
if the following are true:
- 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
if the following are true:
- 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
if the following are true:
- 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
if the following are true:
- 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
if the following are true:
- 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
if the following are true:
- 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
if the following are true:
- 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
if the following are true:
- 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
if the following are true:
- 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
if the following are true:
- 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
if the following are true:
- 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
if the following are true:
- 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
if the following are true:
- 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
if the following are true:
- 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
if the following are true:
- 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
if interrupt at computer: c index: 0 time: t = 1, then the PC at computer c and time (t + 1) = 1
if interrupt at computer: c index: x time: t = 1, then interrupt at computer: c index: x time: (t + 1) = 0
if interrupt at computer: c index: x time: t = 1, then byte at ID: c, cell #idx at time (t + 1) = byte at ID: c, cell #idx at time t
if the following are true:
- 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
if the following are true:
- 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
if the following are true:
- 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
if the following are true:
- 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
if the following are true:
- 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
if the following are true:
- 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
if byte at ID: c, cell #27 at time t = 0, then number of characters read at (t + 1) = number of characters read at t
if byte at ID: c, cell #27 at time t = 0, then cursor x at time (t + 1) = cursor x at time t
if byte at ID: c, cell #27 at time t = 0, then cursor y at time (t + 1) = cursor y at time t
if the following are true:
- 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
if the following are true:
- 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
if the following are true:
- byte at ID: c, cell #27 at time t = 1
- cursor x at time t = 39
then cursor x at time (t + 1) = 0
if the following are true:
- 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
if cursor y at time t = 11, then cursor y at time (t + 1) = cursor y at time t
if the following are true:
- 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
if the following are true:
- 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
if the following are true:
- 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
if the following are true:
- 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
if the following are true:
- 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
if interrupt at computer: c index: 1 time: t = 1, then the PC at computer c and time (t + 1) = 2
if the following are true:
- 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
if the following are true:
- 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
if the following are true:
- 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
if the following are true:
- 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
if the following are true:
- 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
if the following are true:
- 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
if byte at ID: c, cell #49 at time t = 0, then disk bytes read at time (t + 1) = disk bytes read at time t
if byte at ID: c, cell #49 at time t = 0, then disk byte at index: index time: (t + 1) = disk byte at index: index time: t
if the following are true:
- 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
if the following are true:
- 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
if the following are true:
- 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
if the following are true:
- 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
if the following are true:
- 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
if the following are true:
- 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
if the following are true:
- 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
if the following are true:
- 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
if the following are true:
- 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
if interrupt at computer: x index: 2 time: t = 1, then the PC at computer x and time (t + 1) = 3
if byte at ID: x, cell #68 at time t = 0, then network bytes read from computer: x at time (t + 1) = network bytes read from computer: x at time t
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
- expression state at time t = "not_expr"
then the expression at time (t + 1) = Python list elements
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
- expression state at time t = "not_expr"
then expression state at time (t + 1) = "begin_expr"
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
- expression state at time t = "not_expr"
then the line at time (t + 1) = i
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
- expression state at time t = "not_expr"
then the tab at time (t + 1) = j
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
- expression state at time t = "not_expr"
then Value Stack at time (t + 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
- expression state at time t = "not_expr"
then parent stack at time (t + 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
- expression state at time t = "not_expr"
then arguments stack at time (t + 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
- expression state at time t = "not_expr"
then Python Object Store at time (t + 1) = Python Object Store at time t
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
- expression state at time t = "not_expr"
then Control Map at time (t + 1) = Control Map at time t
if the following are true:
- 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 ]
if the following are true:
- 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 ]
if the following are true:
- 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 ]
if the following are true:
- expression state at time t = "begin_expr"
- the expression at time t = Python list elements
then expression state at time (t + 1) = "iterate_args"
if the following are true:
- 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))
if the following are true:
- 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)
if the following are true:
- 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
if the following are true:
- 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"
if the following are true:
- 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"
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
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 stack at time (t + 1) = stack at time t
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 "if" map at time (t + 1) = "if" map at time t
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 'while stack' at time (t + 1) = 'while stack' at time t
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
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 state at time t = "not_expr"
then the expression at time (t + 1) = Python list elements
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 state at time t = "not_expr"
then expression state at time (t + 1) = "begin_expr"
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 state at time t = "not_expr"
then the line at time (t + 1) = i
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 state at time t = "not_expr"
then the tab at time (t + 1) = j
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 state at time t = "not_expr"
then Variables Map at time (t + 1) = Variables Map at time t
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 state at time t = "not_expr"
then stack at time (t + 1) = stack at time t
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 state at time t = "not_expr"
then Value Stack at time (t + 1) = [ ]