Properties of an execution of a computer program--particularly for concurrent and distributed systems--have long been formulated by giving safety properties ("bad things don't happen") and liveness properties ("good things do happen").

A program is totally correct with respect to a precondition and postcondition if