Axiomatic semantics definitions with so-called "laws of programming" has been advocated as being a natural method that is easy to use for verification without requiring deep specialized mathematical knowledge (see Hoare et al. [HHJ+87]). The appealing feature of this method is that the semantics of a language is described only by equations (or refinement relationships) relating syntactic objects of the language without explicit mention of semantic entities.

• kiel-khb-5-1.ps