Уточненное исчисление

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

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

Эта статья о формальных методах является заглушкой . Вы можете помочь Википедии, расширив ее.

• в
• т
• е