Исчисление уточнения - Refinement calculus

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

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

использованная литература

  1. ^ Батлер, Майкл. "Учебное пособие по исчислению уточнения". Получено 22 апреля 2020.

внешние ссылки