Go backward to Valuation Functions Go up to Top Go forward to Simplification

Program Denotation

• How to understand a program?
• A possibility is to compute its denotation with a particular input argument.

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

• Various results for various inputs.

  Natural number or _|_ (non-termination)

Z:=1;

if A=0 then diverge;

Z:=3.

V P (two)

Denotation