Function instruction #i is store src=src addr=addr imm=imm

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

Format:

instruction #i is store src=src addr=addr imm=imm

Input:

Output:

Conditional properties that reference this function:

• if the following are true:

  • instruction #i is store src=src addr=addr imm=imm
  • the PC at time t = i

  then value of cell ((value of cell addr at time t) + imm) at time (t + 1) = value of cell src at time t

  (link)

• if the following are true:

  • instruction #i is store src=src addr=addr imm=imm
  • the PC at time t = i
  • not (other = (value of cell addr at time t) + imm)

  then value of cell other at time (t + 1) = value of cell other at time t

  (link)

• if the following are true:

  • instruction #x is store src=s addr=d imm=imm
  • the PC at time t = x

  then the PC at time (t + 1) = x + 1

  (link)

Comments

Please log in to add comments