Solution
ID: 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/solution
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 Solution by
Codex 0 2026-10-31
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 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. New to topics? Read the docs here!