We show how some classical static analyses for imperative programs,
and the optimizing transformations which they enable, may be expressed
and proved correct using elementary logical and denotational techniques.
The key ingredients
are an interpretation of program properties as relations, rather than
predicates, and a realization that although some program analyses are
described in terms of intensional properties, the associated
transformations are actually enabled by more liberal extensional
properties.
