Counter Machine Reference Model - Formal Definition

Formal Definition

The Counter machine reference model consists of a finite set of registers r1 ... rn, each of which can hold a non-negative integer, r0 (always zero), and a finite list of instructions I1 ... Im. Each of the instructions in this list is one of the following:

  • INC(j) — increment the value of register rj by 1; go to the successor instruction (e.g. instruction that is numerically next-in-sequence).
  • DEC(j) — If the contents of r is not 0 (not empty) then decrement the value of register rj by 1, else the contents of r=0; go to the successor instruction.
  • JZ (j, z) — If the contents of register rj equals Zero then Jump to instruction Iz else go to the successor instruction.
  • HALT — halts the computation.

Formal Semantic:

Instruction Effect on register Effect on Instruction Counter (IC)
INC ( j ) + 1 → j + 1 → IC
DEC ( j ) IF > 0 THEN - 1 → j ELSE 0 → j + 1 → IC
JZ ( j, z ) IF =0 THEN Iz → IC ELSE + 1 ) → IC

Read more about this topic:  Counter Machine Reference Model

Famous quotes containing the words formal and/or definition:

    Two clergymen disputing whether ordination would be valid without the imposition of both hands, the more formal one said, “Do you think the Holy Dove could fly down with only one wing?”
    Horace Walpole (1717–1797)

    The definition of good prose is proper words in their proper places; of good verse, the most proper words in their proper places. The propriety is in either case relative. The words in prose ought to express the intended meaning, and no more; if they attract attention to themselves, it is, in general, a fault.
    Samuel Taylor Coleridge (1772–1834)