Ebben a fejezetben olyan tételeket bizonyítunk be, amelyeket gyakran alkalmazunk feladatok finomítása során, vagy amelyek megkönnyítik annak bizonyítását, hogy egy program megfelel egy adott specifikációs feltételnek. Ezeket a tételeket levezetési szabályoknak nevezzük. A leggyakrabban invariánsok, elkerülhetetlenséget kifejező, ill. fixpontfeltételek finomítására van szükség.