Generic commands--a tool for partial correctness formalisms

A semantic framework for logical formalisms based on partial correctness assertions of the form P{S}Q is given. P{S}Q asserts that if P holds before execution of S then Q holds after. Generic commands are introduced. The generic command {P=≥Q} is in a sense the least specified command with precondition P and postcondition Q. Proof rules and a noneffective semantics are given for generic commands. A proof rule for recursive procedures is given using generic commands.