Can the semantics of a program be represented as a single formula? We show that one formula is insufficient to handle assertions, refinement or slicing, while two formulae are sufficient: A (S) , defining non-termination, and B (S), defining behaviour. Any two formulae A and B will define a corresponding program. Refinement is defined as implication between these formulae.