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:

    The manifestation of poetry in external life is formal perfection. True sentiment grows within, and art must represent internal phenomena externally.
    Franz Grillparzer (1791–1872)

    No man, not even a doctor, ever gives any other definition of what a nurse should be than this—”devoted and obedient.” This definition would do just as well for a porter. It might even do for a horse. It would not do for a policeman.
    Florence Nightingale (1820–1910)