Modelling the algebra of weakest preconditions

In expounding the notions of pre- and postconditions, of termination and nontermination, of correctness and of predicate transformers I found that the same trivalent distinction played a major role in all contexts. Namely: Initialisation properties: An execution of a program always, sometimes or never starts from an initial state. Termination/nontermination properties: If it starts, the execution always, sometimes or never terminates. Clean-/messy termination properties: A terminating execution always, sometimes or never terminates cleanly. Final state properties: All, some or no final states of α from s have a given property