Составители:
Рубрика:
разных стадиях проектирования. При таком подходе при написании
программ акцент делается на их тестируемость, т.е. на создание
программ, которые удобно тестировать, а безошибочность и
корректность программы в значительной степени зависят от
творческих способностей и интуиции разработчика.
В отличие от интуитивного подхода, который мы
охарактеризовали выше, рассматриваемый далее подход трактует
программирование как точную математическую науку. Этот подход
основан на том, что спецификация программ выражается средствами
логики, причем связь программ с их спецификацией осуществляется
путем определения семантики программ также средствами логики
(алгоритмическая логика Хоара
*
). Этот подход открывает путь к
верификации (доказательству правильности) алгоритмов и программ
средствами логики.
В основе верификации программ (алгоритмов) – анализ
действия программ (алгоритмов) над данными. Для каждого
исходного состояния данных X, для которого выполнение
завершается, результирующее состояние данных Y является
определенным. Это значение Y единственно для данного X, поэтому
множество всех упорядоченных пар (X,Y) определяет функцию,
которую будем называть программной функцией.
Мы будем использовать символьные вычисления, чтобы
получить аналитическое выражение программной функции для
исследуемой программы. Программную функцию f для простой
программы P обозначим через [P] и определим выражением
[P]={(X,Y)⎥ Y=f(X)},
где X - состояние поля данных до выполнения P,
Y - состояние поля данных после выполнения P,
{(X,Y) ⎥ Y=f(X)} - множество пар (X,Y), таких, что Y=f(X).
Последовательные (линейные) структуры
Рассмотрим последовательность двух блоков g={(X,Y)} и
h={(Y,Z)}, изображенную на рис.2.1. Программная функция такой
:
*
Дал У., Дейкстра Э., Хоор К. труктурное программирование. – М Мир, 1975. С
X Y Z
Рис.2.1.
g h
112
p
=
Страницы
- « первая
- ‹ предыдущая
- …
- 26
- 27
- 28
- 29
- 30
- …
- следующая ›
- последняя »
