Утонченность исчисление является формализованным подходом к ступенчатому уточнению для построения программ. Требуемое поведение конечной исполняемой программы определяется как абстрактная и, возможно, неисполняемая «программа», которая затем уточняется серией сохраняющих корректность преобразований в эффективно исполняемую программу. [1]
Среди сторонников этого подхода - Ральф-Йохан Бэк , который положил начало этому подходу в своей докторской диссертации 1978 г. О правильности шагов уточнения при разработке программ , и Кэрролл Морган , особенно в его книге « Программирование на основе спецификаций» (Прентис Холл, 2-е издание, 1994 г., ISBN 0-13 -123274-6 ). В последнем случае, мотивация была связать Abrial «ы спецификации обозначение Z , с помощью строгого соотношения поведения , сохраняющей программы уточнения , к исполняемому программированию обозначений на основе Дейкстров » языке с из охранявших команд . Сохранение поведенияв данном случае означает, что любая тройка Хоара, удовлетворяемая программой, также должна удовлетворяться любым ее уточнением, что приводит непосредственно к операторам спецификации как предварительным и постусловиям, стоящим сами по себе для любой программы, которую можно разумно разместить между ними .
Рекомендации
- ^ Батлер, Майкл. "Учебное пособие по исчислению уточнения" . Проверено 22 апреля 2020 . CS1 maint: обескураженный параметр ( ссылка )