Past exam of the year 1 of the computer science course of the University of Oxford / 2015 / Digital systems, linear algebra, introduction to formal proof / 6 / a

A zero-address instruction has no explicit operand addresses, so its operands and result location must be implicit in the instruction set architecture. A stack machine supplies these naturally: operations remove their inputs from the top of an operand stack and push the result. A fixed-processor register design is logically possible, so “almost certainly” is appropriately weaker than a proof that only a stack machine could work.

Write the stack from bottom to top, with its top on the right. Let $S$ stand for any unchanged prefix. Suitable effects areThus add pops two operands and pushes one sum, reducing stack occupancy by one. The special const c instruction pushes its immediate constant and increases occupancy by one. Only const needs an explicit value in its encoding.