Function subtract immediate instruction with dst: dst src: src and immediate: imm

the subtract-immediate (subtracti) instruction subracts imm from a value stored in src and stores the result in dst

Format:

subtract immediate instruction with dst: dst src: src and immediate: imm

Input:

Output:

Conditional properties that reference this function:

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

  (link)

Comments

Please log in to add comments