Уточняющее исчисление

Уточняющее исчисление — это формализованный подход к поэтапному уточнению при построении программы. Требуемое поведение окончательной исполняемой программы определяется как абстрактная и, возможно, неисполняемая «программа», которая затем уточняется с помощью ряда преобразований, сохраняющих корректность, в эффективно исполняемую программу.

В число сторонников входят Ральф-Йохан Бэк , который разработал этот подход в своей докторской диссертации 1978 года « О правильности этапов уточнения при разработке программ» , и Кэрролл Морган , особенно с его книгой «Программирование на основе спецификаций» (Prentice Hall, 2-е издание, 1994 г., ISBN   0-13-123274-6 ). В последнем случае мотивацией было связать Абриала нотацию спецификации Z через строгое отношение уточнения программы , сохраняющей поведение , с нотацией исполняемого программирования, основанной на Дейкстры языке защищенных команд . Сохранение поведения в данном случае означает, что любая тройка Хоара , которой удовлетворяет программа, также должна удовлетворяться при любом ее уточнении, что приводит непосредственно к утверждениям спецификации как пред- и постусловиям, которые сами по себе являются самостоятельными для любой программы, которая могла бы быть обоснованно реализована. помещен между ними.