Function a STORE instruction with src: src address: addr and immediate: imm

the store instruction copies the value in src to address (value at addr + imm)

Format:

a STORE instruction with src: src address: addr and immediate: imm

Input:

Output:

Conditional properties that reference this function:

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

  (link)

Comments

Please log in to add comments