Some Remarks on the Simple Concrete Model of Computer
Andrzej Trybulec, Yatsuka Nakamura · 2004
We prove some results on SCM needed for the proof of the correctness of Euclid’s algorithm. We introduce the following concepts: starting finite partial state (Start-At(l)), then assigns to the instruction counter an instruction location (and consists only of this assignment), programmed finite partial state, that consists of the instructions (to be more precise, a finite partial state with the domain consisting of instruction locations). We define for a total state s what it means that s starts at l (the value of the instruction counter in the state s is l) and s halts at l (the halt instruction is assigned to l in the state s). Similar notions are defined for finite partial states.