Go backward to A Language with Assignment Go up to Top Go forward to Program Denotation

Valuation Functions

• P: Program -> Nat -> Nat_{_|_}

  Program maps input number to an answer number; non-termination is possible (codomain includes _|_).

• C: Command -> Store_{_|_} -> Store_{_|_}

  Command maps store into a new store; predecessor command may not have terminated (domain includes _|_) and command may not terminate (codomain includes _|_).

• E: Expression -> Store -> Nat

  Expression maps store into natural number.

• B: Bool-exp -> Store -> Tr

  Boolean expression maps store into truth value.

• N: Numeral -> Nat

  Numeral yields a natural value.