Понятие корректности программы, введенное в разд. 2.3, состоит из трех условий
(2.7–2.9). Главным из них является условие (2.7) соответствия программы и спецификации, согласно которому постусловие оператора S должно быть доказано из LS(S). Однако в практике построения программ из математического решения задачи, как правило, реализуется вывод в обратную сторону: программа выводится из спецификации. Нашей целью является определения условий, при которых такой вывод был бы возможен, с построением соответствующих правил доказательства корректности программы. Необходимым условием является однозначность спецификации.