Введение в технологию программирования

         

Постановка задачи. Оценка осуществимости - часть 2


Зачем? Ведь модель и так все делает". Это произвело на них впечатление. Хотя, конечно, стремиться к более точным моделям нужно всегда.

Несколько слов о декомпозиции системы. Я не устаю удивляться, насколько точнее оценка сложности системы, которая является суммой оценок ее компонентов, полученных в результате декомпозиции, чем первоначальная оценка системы в целом. Ведь делают эти оценки одни и те же системные аналитики, наверняка у них уже было примерное представление о системе и ее компонентах, когда они давали первоначальную оценку. И тем не менее, эти же мысли, положенные на бумагу, особенно с помощью каких-то средств формализации, приводят к совершенно другому результату.

Однако, формализация формализации рознь. Тридцать лет назад бытовало мнение, что можно и нужно каждую задачу формально специфицировать с помощью логики предикатов чтобы можно было доказать корректность ее решения[6]. Для каждой программы P нужно задать предусловие A, описывающее состояние среды (в частности, переменных программы) перед исполнением программы, и постусловие S, описывающее состояние после завершения ее исполнения:

A {P} S

Очевидно, что A и S – несопоставимы, поскольку описывают состояние в разные моменты времени. Можно "протянуть" предусловие A через текст программы, изменяя его соответственно каждому проходимому оператору, при этом логическая формула предусловия фантастически быстро растет, например, после условного предложения будет дизъюнкция двух вариантов, описывающих текущие предусловия после веток then и else – мы же не знаем, какая именно ветка будет исполняться. Обозначим результат протягивания через A'. Тогда остается доказать истинность импликации A'

S, и программа корректна! Мы тоже потратили несколько лет, работая в этом направлении, например, Н. Ф. Фоминых в 1976-м году защитил под моим руководством дипломную работу, реализовав "протягиватель" для Алгола 68. Все эти предусловия и постусловия были очень громоздкими – много больше, чем текст программы и затраты на их создание – тоже.




Содержание  Назад  Вперед