Function Byte of Memory At ID and Time

The Byte of Memory at Time function outputs the value stored in memory cell #i at time t

Format:

byte at ID: id, cell #i at time t

Input:

Output:

Details:

Each memory slot in the computer stores 1 byte. A byte is 8 bits. A bit can represent 2 values (0 and 1), which means that a byte can represent 256 possible values. As the computer executes instructions, the values in memory can change. For example, the value at location 3 might be 0 at time 0 but change to 8 at time 1.

Properties that reference this function:

Conditional properties that reference this function:

• 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

  (link)

• 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

  (link)

• 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

  (link)

• 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

  (link)

• 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)

  (link)

• 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

  (link)

• 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

  (link)

• 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

  (link)

• 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

  (link)

• 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

  (link)

• 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

  (link)

• 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

  (link)

• 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

  (link)

• 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

  (link)

• 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

  (link)

• 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

  (link)

• 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

  (link)

• 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

  (link)

• 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

  (link)

• 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

  (link)

• 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

  (link)

• 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

  (link)

• 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

  (link)

• 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

  (link)

• 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

  (link)

• 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

  (link)

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

  (link)

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

  (link)

• 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

  (link)

• 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

  (link)

• 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

  (link)

• 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

  (link)

• 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

  (link)

• 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

  (link)

• 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

  (link)

• 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

  (link)

• 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

  (link)

• 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

  (link)

• 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

  (link)

• 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

  (link)

• 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

  (link)

• 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

  (link)

• 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

  (link)

• 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

  (link)

• 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

  (link)

• 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

  (link)

• 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

  (link)

• 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

  (link)

• 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

  (link)

• 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

  (link)

• 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

  (link)

• 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

  (link)

• 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

  (link)

• 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

  (link)

• 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

  (link)

Comments

Please log in to add comments