Реальное переосмысление "формальных методов"

Дэвид Лордж Парнас
Перевод: Виктор Кулямин

Оригинал: David Lorge Parnas. Really Rethinking "Formal Methods". Computer (IEEE Computer Society), V. 43, No 1, January 2010

Дэвид Лордж Парнас является почетным профессором университета МакМастера, Канада, и университета Лимерика, Ирландия, а также президентом компании Middle Road Software. Он уже почти 50 лет занимается исследованиями в различных областях, выявляя связи между теорией и практикой в проектировании программного обеспечения. Степень доктора философии по электротехнике получена им в университете Карнеги-Меллон.

Мы должны подвергнуть сомнению предположения, лежащие в основе хорошо известных современных формальных методов разработки программного обеспечения, чтобы понять, почему они не получили широкого распространения, и что в них следует изменить.

Тема нескольких основных статей сентябрьского выпуска Computer в 2009 году звучала как "Переосмысление формальных методов". Такое переосмысление определенно серьезно запоздало.

Уже более 40 лет тому назад покойный Роберт Флойд (Robert Floyd) показал, как можно "определять смысл программ", и продемонстрировал, как можно проверить, что программы делают то, для чего они предназначены [1]. Прошло, по крайней мере, 35 лет с тех пор, как я слышал рассказ Жана-Реймонда Эбриэля (Jean-Raymond Abrial) о его идеях, легших в основу нотации Z и ее многочисленных диалектов. Люди, создавшие венский метод (Vienna Development Method, VDM), начинали работать примерно в то же время. Даже формальные методы второго и третьего поколений уже показывают признаки старения.

С 1967 г. много раз происходили "революции" в аппаратной части и в человеко-машинных интерфейсах. Когда Флойд писал свою работу, компьютер на моем рабочем столе был невообразим. К сожалению, сопоставимого прогресса в формальных методах нет. Были предложены новые языки и новые логики, но ошибки проектирования, которые встречались в 1967 г., можно найти и в нынешнем программном обеспечении (ПО). Исключительно редкое применение формальных методов в производственной разработке ПО только подчеркивает, что использование таких методов не стало установившейся практикой.

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

Содержание

Утверждения о прогрессе и производственное внедрение

Три тревожных разрыва

Разрыв между исследованиями и практикой

Разрыв между разработкой ПО и старыми инженерными дисциплинами

Разрыв между компьютерными науками и классической математикой

Красавица и чудовища

Что следует переосмыслить?

Идентификаторы и переменные

Обычные выражения или что-то более структурированное?

Скрытое состояние: норма или расширение?

Завершение работы: норма или исключение?

Время: особая переменная или просто еще одна переменная?

Аскиомы: присваивание или реляционная алгебра?

Направление анализа: вперед, назад или изнутри?

Побочные эффекты: норма или зло?

Недетерминизм: норма или исключение?

Модели, описания и спецификации

Спецификации: программы или предикаты?

Язык спецификаций: язык программирования или математическое описание?

Чем можно пренебречь?

Как мы устанавливаем соответствие между моделью и кодом?

Математика в документации

Пред- и постусловия

Доказательство корректности или определение свойств?

Наблюдения

Программное обеспечение полно ошибок, но неправильные формальные методы не исправят его

Нам нужны исследования, а не пропаганда

Шаг за шагом от пользователя к коду

Абстрактные представления должны быть упрощенными, но правильными

Мы должны действовать как инженеры, а не философы или логики

Литература

Утверждения о прогрессе и производственное внедрение

Научная литература в области компьютерных наук демонстрирует, что "формальные методы разработки программного обеспечения" – это популярная тема исследований. Различные варианты таких методов часто обсуждаются и оспариваются на конференциях и в журналах.

Фонды, выдающие исследовательские гранты, часто требуют, чтобы проекты со значительным финансированием включали какое-то взаимодействие с производственными компаниями и демонстрировали практичность своих подходов на "реальных" примерах. Когда авторы отчитываются о выполнении таких проектов, они утверждают, что они были успешными. Такие успехи, парадоксальным образом, вскрывают неспособность индустрии внедрить формальные методы как стандартные процедуры – если бы их использование было рутинным, статьи о таких успехах вообще не появлялись бы.

Промышленные разработчики настолько задавлены ошибками и высокой стоимостью поддержки ПО, что использовали бы любые методы, если бы считали, что они им помогут; однако они не используют такие подходы, как Z или VDM.

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

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

Некоторые из отмечаемых успехов можно объяснить тем, что два разных человека тщательно изучали задачу и код. Тридцать лет назад в работе, которую и сегодня стоит прочитать, Хани Эловиц (H.S. Elovitz) описал эксперимент, в котором программа на другом языке программирования была использована именно так, как апологеты формальных методов предлагают использовать свои модели [2]. Один язык назывался языком спецификации, второй &ndash языком реализации. Один программист писал "спецификацию" и отдавал ее второму, который переводил ее на язык реализации. Первый проводил экспертизу выполненной трансляции. Частота появления ошибок снижалась, и этот метод (ранняя версия парного программирования) был признан успешным. Один лишь этот эффект может объяснить немногочисленность успешных применений формальных методов. Отчеты о том, что формальные методы готовы для использования в промышленности, должны восприниматься с сомнением – если бы они на самом деле были готовы, они бы уже широко использовались.

Три тревожных разрыва

За последние 40 лет в области разработки программного обеспечения развилось несколько негативных тенденций.

Разрыв между исследованиями и практикой

Разрыв между исследованиями в формальных методах и практической разработкой ПО сегодня гораздо больше, чем был в то время, когда Флойд написал свою работу. Флойд был успешным, передовым и продуктивным программистом. Его статья четко вскрывала связи между математическими абстракциями и программным продуктом.

Сегодня многие исследовательские работы пишутся так, будто только математика и имеет значение. Они не показывают, как соотнести формальные модели с кодом, работающим на настоящих компьютерах. Более того, они не предлагают путей преодоления сложности программных систем.

С другой стороны, большинство разработчиков ПО воспринимает формальные методы как бесполезную теорию, не имеющую связи с тем, чем они занимаются. Нет более эффективного способа потерять внимание аудитории из программистов, чем показать им математическую формулу. Разработчики видят потребности в улучшении и будут использовать практически любой новый подход при условии, что он не выглядит математизированным.

Разрыв между разработкой ПО и старыми инженерными дисциплинами

Между разработкой ПО и традиционными инженерными дисциплинами также имеется тревожащий разрыв. Разработчики программ часто считают себя инженерами, но их образование и каждодневная работа не похожи на образование и работу классических инженеров. В инженерных курсах преподаются основы естественных наук, прикладная математика и методы ее применения для предсказания характеристик продуктов. Большинство курсов по компьютерным наукам учит технологиям (которые часто скоротечно сменяются в нашем быстро изменяющемся мире) и абстрактной математике, способам применения которой студенты не обучаются.

Двадцать лет назад я слышал жалобы одного мудрого и опытного менеджера верхнего звена на то, что его программисты и другие инженеры разговаривают на настолько различных "языках" и думают настолько по-разному, что им трудно работать вместе. Этот разрыв по-прежнему существует.

Разрыв между компьютерными науками и классической математикой

Более неожиданным ходом событий является разъединение теоретиков в области компьютерных наук и классических математиков. Во многих программах по компьютерным наукам студентам предлагается очень тонкий слой математики, и упор обычно делается на недавних результатах и "чистой" математике по сравнению с более старыми работами и так называемой "прикладной математикой". Математика развивается довольно медленно и содержит много зрелых и достаточно общих понятий, которые можно использовать при анализе и описании компьютерных систем.

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

Это хорошо иллюстрирует сравнение подходов к семантике и верификации программ двух человек, работавших в одном и том же институте – математика Николаса де Бройна (N.G. de Bruijn) и компьютерного теоретика Эдсгера Дейкстры (E.W. Dijkstra). Де Бройн применял классическое понятие отношения, а Дейкстра изобрел свои "предикатные преобразователи". В своей работе я обнаружил, что подход на базе отношений гораздо более удобен и прост в использовании.

Красавица и чудовища

В большинстве статей об использовании математики в разрабоке ПО содержатся два вида утверждений.

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

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

• Даже для небольших примеров модели оказываются более сложными, чем код.
• Модель – это программа (последовательность преобразований данных), которую не легче написать или понять, чем настоящую программу.
• В моделях чересчур упрощаются решаемые задачи за счет игнорирования многих неудобных деталей, что часто ведет к ошибкам.
• Часто приводимые примеры не включают итоговый код, и даже если включают, трудно бывает установить связи между моделью и кодом. В таких случаях, даже если корректность модели доказана, код может содержать неуловимые ошибки.

Проблемы обостряются для больших примеров. Часто для ответа даже на простые вопросы по поводу разработки возникает необходимость очень хорошего понимания используемых моделей. Иногда модели просто невозможно читать, и никто, кроме их автора не может ответить на такие вопросы.

Мы должны научится применять математику при разработке ПО, но нужно поставить под сомнение большинство методов, которые продвигались и обсуждались все эти годы, и быть готовыми отказаться от них. Нужно аккуратно изучить посылки, на которых они основаны, и выявить те из них, которые выдержат тщательный анализ.

Что следует переосмыслить?

Если мы действительно собираемся переосмыслить формальные методы, нужно объективно рассмотреть ряд вопросов.

Идентификаторы и переменные

Роберт Флойд и большинство его последователей представляли состояние работающей программы при помощи использованных в ней идентификаторов. Например, если в программе имелась бы переменная "dogs", этот же идентификатор появился бы в логических выражениях, характеризующих состояние программы.

Переменные программы – это конечные автоматы, а то, что мы называем значением переменной, – это состояние такого автомата. Идентификатор представляет собой строку, используемую для именования переменной. С одной переменной может связываться несколько идентификаторов (алиасов), и один идентификатор может ссылаться на разные переменные в разных местах программы.

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

Флойд неявно предполагал наличие взаимнооднозначного соответствия между переменными программы и используемыми идентификаторами. Он также полагал, что если идентификатор не упоминается в выражении или инструкции, то соответствующая переменная никак не задействуется в соответствующем вычислении. Это не всегда верно. Предлагались различные "обходные пути", но они усложняют использование формальных методов. Многие исследователи считают, что использование приемов программирования, разрушающих взаимную однозначность соответствия между переменными и идентификаторами, (например, указателей) является плохой практикой. Однако эти приемы, на самом деле, полезны, и исследователи просто пытаются прикрыть недостатки своих собственных методов, клевеща на вещи, с которыми они не могут работать.

Особенно раздражающим примером этой проблемы являются массивы. "A[j]" и "A[2]" могут идентифицировать одну и ту же переменную. Если мы сочтем их различными, то сможем доказать корректность программы, которая неправильна. Дейкстра предлагал рассматривать весь массив как одну переменную. Это хорошо работает, пока элементы массива используются одинаковым образом, но так обстоят дела не всегда.

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

Обычные выражения или что-то более структурированное?

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

Пришло время поискать новые формы выражений, которые описывают свойства функций, реализуемых компьютерными программами.

Скрытое состояние: норма или расширение?

У переменных в языках программировния 1960-х годов имелась простая связь между видимым значением и состоянием. С введением в языки абстракции или сокрытия информации и последующим появлением пользовательских "абстрактных типов" стали возможны такие переменные, как, например, стеки, у которых видимым значением является только часть состояния. Чтобы справиться с этим, в формальных методах часто используются явные представления состояний. Такие представления строятся произвольным образом и часто все только усложняют.

Пришло время рассматривать скрытое состояние, как норму, и разрабатывать методы, работающие с ним на систематической основе.

Завершение работы: норма или исключение?

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

При переосмыслении требуется поставить вопрос: не следует ли считать нормой незавершающие работу программы, чтобы завершающиеся программы полагались ее частным случаем?

Время: особая переменная или просто еще одна переменная?

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

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

При переосмылении требуется серьезно проанализировать эту альтернативу. Если мы не должны будем считать время чем-то особенным, все существенно упрощается.

Аскиомы: присваивание или реляционная алгебра?

В своей ранней работе "An Axiomatic Basis for Computer Programming" [3] Энтони Хоар (C.A.R. Hoare) ввел около десятка аксиом. В логике аксиомы обычно просты, интуитивно понятны и очевидным образом всегда верны. Аксиомы Хоара (я думаю, что по сути они совпадают с аксиомами, использованными Флойдом) не имеют этих свойств. Арифметические аксиомы не соблюдаются на любом практически доступном компьютере. Аксиома присваивания выполняется только при очень серьезных ограничениях. Аксиома для циклов больше похожа на шаблон доказательства их корректности, чем на настоящую аксиому, поскольку требует определения правильного инварианта.

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

Направление анализа: вперед, назад или изнутри?

Флойд, Хоар и большинство других исследователей анализировали программы по ходу их выполнения, т.е. начинали с первой инструкции и начальных условий и двигались к концу программы. Анализ циклов требует "индуктивных утверждений" или "инвариантов", но в других случаях рассуждения идут в направлении исполнения инструкций. В противовес этим работам Дейкстра предложил вести анализ в противоположном направлении. Его подход на основе "слабейших предусловий" отталкивается от желаемого постусловия и определяет, какое условие должно быть выполнено перед началом исполнения программы, чтобы она выдала желаемый результат. Но у него немного последователей.

Можно использовать любой из этих подходов. Более важно то, что можно идти "снизу вверх" или "изнутри наружу", суммируя результаты анализа внутренних программ, чтобы получить свойства всей программы. При этом преимуществами обладают реляционные методы, поскольку соответствующие аксиомы не основаны на специфических инструкциях (таких как присваивание), а применимы к общим программам любого размера.

Побочные эффекты: норма или зло?

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

Недетерминизм: норма или исключение?

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

Модели, описания и спецификации

Во многих статьях, посвященных формальным методам, используются слова "модель" и "спецификация" как синонимы, возможно, на основе стандартного словарного определения спецификации как информации специального вида. Это определение не соответствует инженерному использованию этих терминов. Стоит рассмотреть возможные альтернативы.

• В инженерии слово "спецификация" используется в более узком смысле, обозначая детальное описание требований.
• "Модель" некоторого изделия – это нечто, напоминающее это изделие, но более простое. Некоторые свойства модели могут не совпадать со свойствами оригинала.
• Модель или документ являются "описанием", если все, что можно узнать из них, верно и для описываемого предмета. Спецификация является описанием удовлетворяющего ее изделия, но некоторые описания не являются спецификациями, поскольку описывают свойства, наличие которых в соответствующем изделии не требуется.

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

Спецификации: программы или предикаты?

До того, как получили известность работы Флойда, некоторые исследователи в области верификации программ утверждали, что, поскольку нет способа сформулировать, что программа должна делать, можно лишь доказывать эквивалентность программ. При таком подходе пишется программа, которая "очевидно правильна", а затем доказывается, что более сложная и часто более эффективная программа выдает те же результаты.

Этот подход все еще живет в некоторых формальных методах. "Спецификацией" считается программа, описывающая последовательность изменений состояний или преобразований данных.

Если такая последовательность не фиксируется в требованиях, программы не следует использовать, как спецификации. Альтернативное представление спецификации как предиката не привлекло достаточного внимания. Предикат не позволяет напрямую вычислить правильный результат, но зато позволяет проверить правильность полученного результата.

Пришло время поискать методы, в которых в качестве спецификаций используются утверждения о наблюдаемом поведении.

Язык спецификаций: язык программирования или математическое описание?

Термин "язык спецификаций" часто вызывает путаницу. Поскольку спецификация – это описание, языки спецификаций в действительности являются языками описаний. Кроме того, большая часть нотаций, считающихся языками спецификаций, на самом деле является языками программирования.

Нужно подумать о методах, в которых не используется термин "язык спецификаций".

Чем можно пренебречь?

В формальном анализе используется упрощенное описание реальной системы – модель. Упрощение достигается за счет пренебрежения определенными фактами, такими как ограничения на размеры элементов данных и ошибки в арифметических вычислениях. К сожалению, упущение из рассмотрения такого рода деталей часто ведет к ошибкам. Формальный анализ, в котором упускаются критические ограничения, не может выявить связанные с ними ошибки.

Стоит искать методы, не игнорирующие конечные пределы (finite limits), являющиеся одним из наиболее частых источником ошибок.

Как мы устанавливаем соответствие между моделью и кодом?

Поскольку у практических языков программирования чаще всего отсутствует полная формальная семантика, в которой учитываются поведение ПО и конечные пределы, многие формальные методы работают с моделями, которые сильно отличаются от реального кода. Связь между кодом и моделью часто бывает сложной, и ее невозможно четко описать. В таких ситуациях остается открытым вопрос о том, могут ли остаться серьезные ошибки в коде, модель которого доказуемо корректна? В электротехнике математическая модель – это набор уравнений, которые могут быть построены по схеме систематическим образом на основе, например, правил Киркгофа. На практике используются некоторые "идеализации", но часто это учитывается за счет задания допусков и определения возможной неточности в вычисляемом результате.

Требуются аналогичные подходы для построения математических моделей по тексту программ. Флойд относился к этому очень внимательно, но во многих нынешних формальных методах этот аспект явно пренебрегается.

Математика в документации

Чтобы правильно выполнять свою работу и программисты, и пользователи нуждаются в точной информации. Им нужно знать, что ожидается от их продуктов, и что они могут ожидать от используемых программ. Даже "мелкие" детали важны, поскольку небольшие ошибки в ПО могут привести к серьезным проблемам.

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

Одна из наибоее важных ролей, которую математика могла бы сыграть в области разработки ПО, состоит в обеспечении точной, достоверно полно, удобной в использовании и тестируемой документации. Однако при создании популярных формальных методов не преследовалась цель их применения в документировании.

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

Математическая документация должна быть одним из основных направлений исследований в области формальных методов. Пока это не так.

Пред- и постусловия

Самые первые формальные методы основывались на связывании с программой пары предикатов. Одним из них являлось предусловие, описывающее допустимое множество начальных состояний программы, а другим – постусловие, описывающее возможные состояния в конце ее работы. Более 30 лет назад Сьюзан Герхарт (Susan Gerhart) и Лоуренс Еловиц (Lawrence Yelowitz) ясно продемонстрировали, что на самом деле эти условия нельзя отделить друг от друга [4]. Они специфицировали программу сортировки с использованием предусловия, требующего наличия каких-то значений в обрабатываемом массиве, и постуловия, утверждающего, что этот массив отсортирован. Программа, присваивающая j-ому элементу массива значение j, удовлетворяет такой спецификации.

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

Пришло время отказаться от идеи пред- и постусловий.

Доказательство корректности или определение свойств?

Исследователи, интересующиеся математическими методами разработки ПО, сосредотачиваются на "доказательствах корректности". Странно, но инженеры, интенсивно использующие математику, редко используют этот термин. Вместо этого они применяют математику для определения свойств изделия, таких как напряжение на выходе, нелинейные искажения, выделение тепла и т.д. Такие вычисления они используют для оценки или сравнения разработок. "Корректность" – это полезное понятие в математике, но не в инженерии, где определение "корректности" любого значимого приложения явлется серьезной проблемой. Более того, инженеры часто бывают заинтересованы в выборе лучшей разработки из множества "корректных". Корректность сама по себе здесь проблемой не является.

Исследователям, заинтересованные в создании практичных формальных методов, следует проанализировать инженерный подход, в котором расплывчатый общий вопрос заменяется множеством конкретных вопросов.

Наблюдения

Эта статья предназначена для того, чтобы ставить вопросы, а не для того, чтобы отвечать на них. Однако ряд наблюдений все же стоит зафиксировать.

Программное обеспечение полно ошибок, но неправильные формальные методы не исправят его

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

Нам нужны исследования, а не пропаганда

Когда мы видим людей, не пользующихся нашими методами, возникает искушение использовать "передачу технологий" и другие пропагандистские приемы. Когда это не получается, что и произошло с формальными методами, нужно вернуться к исследованиям и поискать пути улучшения своих методов. Наша работа – улучшать методы, а не продавать их. Хорошие методы, разъясненные должным образом, продаются сами по себе. Имеющиеся сейчас методы после первых попыток использования уже не продаются.

Шаг за шагом от пользователя к коду

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

Абстрактные представления должны быть упрощенными, но правильными

Никто не сомневается в пользе абстракции, но важно помнить, что все свойства абстрактной модели должны быть сохранены в реальном продукте. Если это не так, мы имеем дело не с абстракцией, а с ложью.

Мы должны действовать как инженеры, а не философы или логики

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

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

Литература

1. H.S. Elovitz, "An Experiment in Software Engineering: The Architecture Research Facility as a Case Study," Proc. 4th Int'l Conf. Software Eng., ACM Press, 1979, pp. 145-152.
2. R.W. Floyd, "Assigning Meanings to Programs", Proc. Symp. Applied Mathematics, Am. Mathematical Soc., vol. 19, 1967, pp. 19-31.
3. C.A.R. Hoare, "An Axiomatic Basis for Computer Programming", Comm. ACM,Oct. 1969, pp. 576-580.
4. S.L. Gerhart and L. Yelowitz, "Observations of Fallibility in Applications of Modern Programming Methodologies," IEEE Trans. Software Eng., vol. 2, no. 3, 1976, pp. 195-207.