Окончание. Начало в #9/97.
VI Да будет у тебя в достатке документация.
Документация является весьма важной частью проектируемой системы, в особенности если необходимо обеспечить возможность последующих изменений. Формализация документации снижает неоднозначность формулировок и, следовательно, вероятность ошибок. Для систем с повышенными требованиями к безопасности становится значимым расчет времени, и методы его документирования приобретают особый вес [18].
ФМ обеспечивают способ точной и однозначной регистрации ожидаемого и фактического функционирования системы и могут служить мощной поддержкой при документировании. В обычном случае предполагается, что документация системы содержит технические требования и спецификации в приемлемой формальной нотации, сопровождаемые везде, где нужно, описаниями на естественном языке. Последние особенно важны для передачи информации относительно тех аспектов системы, для которых по каким-то причинам не составлялись формальные спецификации.
Как правило, настоятельно рекомендуется писать неформальные спецификации, поясняющие формальное описание [5]. Это помогает читателю лучше понять текст на формальном языке и связать его с реальностью. В случае расхождений между двумя описаниями за основу должно браться формальное как менее неоднозначное.
Формальная документация может принести большую пользу при сопровождении программы. В будущем, вероятно, станет возможным сопровождать не непосредственно исполняемый код, а формальное описание, изменяя лишь те части кода, которые в этом нуждаются [11].
VII Блюди стандарты качества.
Вплоть до сравнительно недавнего времени существовало очень мало стандартов, относящихся специально к тем видам программного обеспечения, при разработке которого оправдано применение ФМ (таковы, например, системы с повышенными требованиями к безопасности). Часто вместо специальных использовались обычные стандарты качества для ПО, в частности стандарты серии ISO-9000, поскольку это был ближайший аналог того, что требовалось. Сейчас нужные стандарты хлынули бурным потоком [6, 8], и некоторые из них рекомендуют, а то и предписывают использование ФМ. Но это не единственные стандарты, которых следует придерживаться.
Существует серьезная опасность, что разработчики будут смотреть на применение ФМ как на способ создавать безошибочные программы. В действительности же, и мы вернемся к этому ниже, ФМ (при условии, что их применяют правильно) всего лишь помогают повысить целостность программных систем.
У ФМ нет волшебных свойств, так что организации должны по-прежнему следить за соблюдением своих стандартов качества. Для этого требуется обеспечить необходимую обратную связь между командами разработчиков и руководством, организовать постоянный контроль и прогоны программ, разработать, а затем совершенствовать и соблюдать правила тестирования и гарантировать соответствие документации стандартам качества для программ, разрабатываемых обычными методами.
VIII Не сотвори себе кумира.
ФМ - не панацея; это лишь один из множества методов, которые, как показывает опыт, при правильном применении позволяют получать системы, обладающие очень высокой целостностью. Полностью отказываться от других методов нельзя. ФМ не гарантируют правильности; работают с ними люди, а человеку, как известно, свойственно ошибаться. Всевозможные инструменты поддержки, такие как редакторы спецификаций, системы проверки типа, проверки непротиворечивости и проверки доказательств, действительно должны уменьшить вероятность ошибки человека, но они не в состоянии исключить ее. Разработка программных систем является и навсегда останется родом человеческой деятельности, а значит, на нее будут влиять человеческие прихоти, нерешительность, неоднозначность естественного языка и просто невнимательность.
Добиться абсолютной правильности невозможно, и смешно предполагать обратное. В дискуссиях в журнале Communications of the ACM [14] и в других аналогичных изданиях высказывались мнения о возможном несоответствии между математической моделью и реальностью [2]. Это отнюдь не открытие, и ни один сторонник ФМ никогда не стал бы утверждать, что формальная модель заведомо правильна. В действительности о правильной работе программы всегда следует говорить не безотносительно, а только в связи с определенной спецификацией. Правильность реализации для данной спецификации может быть доказана, однако, если спецификация не соответствует тому, на что рассчитывали заказчики, они (правда, субъективно) сочтут работу системы неправильной.
Разработчик должен хорошо осознавать необходимость контакта с заказчиками и будущими пользователями системы; и не надо бояться признать, что спецификация оказалась не такой, как нужно, - надо к ней возвращаться и частично ее перерабатывать. Конструирование программных систем - ни в коем случае не поступательный однопроходный процесс. "Водопадную" модель Ройса [19] пришлось отвергнуть из-за слишком упрощенного рассмотрения этой процедуры. Каждый разработчик встречался с необходимостью пересмотреть требования и переработать спецификации на самых разных стадиях создания системы. В идеале все противоречия будут найдены по ходу реализации, самое худшее - при тестировании готовой программы. Тем не менее в исключительных случаях ошибки в спецификации системы обнаруживаются и в процессе эксплуатации.
Разработка систем далеко не столь проста, как предполагает модель Ройса [15, 17]. Это скорее нелинейный, циклический процесс, описываемый, например, "спиральной" моделью Бёма [4]. Поэтому разработчик не должен настаивать на полном определении всех требований из-за того только, что некоторая стадия процесса разработки уже пройдена; на самом деле такие претензии следует считать сомнительными даже после того, как система реализована. Разработчик должен всегда быть готов изменить спецификацию в соответствии с требованиями заказчика; в конце концов, говорил же Роланд У. Мейси, что "клиент всегда прав"*. И даже если требования заказчика удовлетворены полностью, остается еще масса возможностей для ошибок.
Необходимо правильно определить уровень абстракции. Если он задан слишком высоким, трудно увидеть упущения и определить, что же реально должна делать система; если же слишком низким, появляется уклон в сторону конкретных реализаций. Размещение спецификаций на верном уровне абстракции - вопрос опыта, причем необходим опыт работы и с языком спецификаций, и с предметной областью. Не бойтесь признать, что уровень абстракции выбран не наилучшим образом, и соответственно переработать спецификации.
Аналогично, никакое доказательство не может приниматься на веру. При доказательстве вручную допускаются ошибки при переходе с одной строки на другую, делаются громадные логически не обоснованные пропуски. И даже программная проверка не гарантирует правильность доказательства, хотя и помогает выделить необоснованные переходы и ошибки, которых можно избежать.
IX Проверяй, перепроверяй и снова перепроверяй.
Э. Дейкстра [13] указал на главное ограничение тестирования: оно может продемонстрировать наличие ошибок и не может - их отсутствие. Из того, что система прошла тестирование по отдельным модулям и в целом, еще не следует, что в ней не осталось ошибок.
И здесь в случае разработки систем, для которых требуется высокая целостность, у ФМ есть существенные преимущества перед традиционными методами. ФМ позволяют планировать свойства системы и демонстрировать, что они выполняются, изучать поведение системы и убеждаться, что все возможные варианты учтены, и, наконец, доказывать соответствие реализации и спецификаций.
Таким путем можно надеяться искоренить вездесущие ошибки. Но, увы, в противоположность тому, что утверждают многие так называемые "эксперты", ФМ не гарантируют правильности. Разумеется, их использование повышает уверенность в целостности системы, а также в том, что система будет работать именно так, как ожидалось, но ошибки все же существуют и продолжают обнаруживаться в готовой системе.
Даже там, где применяется полная формальная разработка (т. е. спецификации постепенно детализируются вплоть до исполняемого кода), требуется определенная степень человеческого вмешательства. Пока остается неясным, достижимо ли автоматическое преобразование спецификаций в код, да и следует ли этого добиваться.
Формальная спецификация - это абстрактное представление реальности, число реализаций для нее потенциально бесконечно. Но все же, когда мы, выйдя из абстрактного мира множеств, последовательностей и формальной логики, начинаем обдумывать реализацию на каком-либо из принятых языков программирования, выясняется, что лишь очень немногие языки в явной форме поддерживают требуемые структуры (а поддержка там, где она есть, организована в высшей степени неэффективно). Значит, мы должны определить, какие структуры данных лучше всего подходят для реализации высокоуровневых элементов, и преобразовать определенные нами операции так, чтобы они работали с указателями, массивами, записями и т. д. Если предоставить окончательный выбор структур реализации компьютерной программе (в предположении, что она способна выбрать подходящие), это приведет к уклону в сторону конкретной реализации, т. е. к тому, чего следует избегать, чтобы дать программисту максимально возможную свободу выбора в пределах проекта. Таким образом, уточнение всегда будет требовать участия человека, и следовательно, ошибки на этом этапе не исключены.
Даже если проектирование ведется с применением ФМ, от тестирования на уровне как отдельных модулей, так и системы в целом отказываться нельзя. Наоборот, необходимо обширное тестирование, которое сможет выявить ошибки, допущенные в процессе преобразования спецификаций, а также неучтенные случаи. Оно должно быть не столь всеобъемлющим, как в отсутствие ФМ, но все же довольно значительным по объему.
При создании узла вычислений с плавающей запятой Inmos для суперкомпьютера T800 одна ошибка была обнаружена в процессе тестирования. Она возникла в результате "очевидно правильного" изменения, внесенного в микрокод уже после окончания формальной разработки. Никогда не следует недооценивать склонность человека к ошибкам; и тестирование всегда остается верным способом определить, действительно ли система, сконструированная по формальным правилам, работает в реальном мире.
Тестирование может выполняться по традиционной схеме - с определением необходимого его объема с помощью таких методик, как оценка сложности по Маккейбу. Другой вариант - использовать какую-либо технику имитации, например исполняемый язык спецификаций или анимацию спецификаций [10, 16].
Для тестирования (конкретно для тестирования на базе спецификаций) ФМ предлагают еще одну возможность - взять формальную спецификацию за основу при определении набора тестов, проверяющих функционирование системы. Для выявления ключевых аспектов работы системы можно воспользоваться абстракцией, построенной при создании спецификаций. Таким образом обеспечивается структурный подход к тестированию, что упрощает тестирование "сверху вниз" [12] и помогает точно определять местонахождение ошибок.
Сами по себе спецификации могут служить для вывода ожидаемых результатов из тестовых данных и помогать в определении необходимых тестов параллельно с проектированием и реализацией, обеспечивая тем самым тестирование отдельных модулей на ранней стадии разработки (что должно снизить затраты на обслуживание системы).
X Не пренебрегай повторным использованием.
Затраты на программирование в сравнении с общей стоимостью разработки системы относительно невелики, и их быстро перевешивают затраты на обслуживание готового продукта. Цену разработки можно существенно снизить за счет повторного использования программ, созданных ранее (их кода, спецификаций, проектов, документации). В отношении ФМ это так же верно, как и в отношении традиционных методов; в формальной разработке повторное использование способно (по крайней мере, теоретически) сократить некоторые виды расходов (например, на инструментальные программы, обучение и занятия с персоналом).
В исследованиях, которые цитирует в работе [11] Кейперс Джонс, утверждается, что в 1983 г. лишь около 15% всего нового кода представляли собой нечто уникальное, новое и специфическое для конкретных программ, прочие же 85% были типовыми и стандартными, и в принципе их можно было бы написать на основе компонентов многократного использования.
Однако на пути многократного использования программ встают различные препятствия. Основных препятствий четыре:
1. Проблема многократного использования в больших масштабах
В случае многократного использования в очень больших масштабах (Very Large Scale Reuse - VLSR) [3] разработка архитектурной суперструктуры для поддержки сочетания компонентов может оказаться настолько дорогой, что потенциальная экономия от повторного использования ее не окупит.
2. Универсальность против специализации
Небольшие компоненты часто имеют широкую сферу применения; более крупные имеют тенденцию к специализации, и их труднее использовать повторно. Однако чем больше компонент, тем больше отдача, и это противоречие, по-видимому, неразрешимо.
3. Затраты на пополнение библиотеки
Работа по определению того, какие программные компоненты подходят для включения в библиотеку, часто весьма трудоемка, однако она необходима, если эти компоненты предполагается многократно использовать. А когда обширная библиотека компонентов уже набрана, встает вопрос, каким образом разыскать в ней подходящие компоненты для включения в тот или иной проект.
4. Синдром "это не наше"
Синдром "это не наше" (Not-Invented-Here - NIH) выражается в том, что разработчики не считают возможным положиться на предыдущие разработки: возможно, они не будут функционировать как ожидалось, не пройдут контроля качества в организации, их не смогут в достаточной степени понять для того, чтобы эксплуатировать в новых системах.
Применение ФМ при разработке систем позволяет преодолеть все эти препятствия и должно расширить практику повторного использования программ.
ФМ (или, конкретнее, языки формальных спецификаций) позволяют однозначно зафиксировать требования к системе или ее компоненту. Среди системных компонентов, определенных формально, легко идентифицировать те, которые удовлетворяют требованиям к компонентам новой системы. Таким образом, если компоненты формально определены и достаточно хорошо документированы, их легко находить, использовать и комбинировать, строя компоненты других систем. Затраты на пополнение библиотек хотя и остаются, но существенно снижаются, а уверенность в надежности компонентов многократно возрастает, поскольку каждый компонент однозначно определен, а его свойства могут быть сформулированы и доказаны.
Очень важно, однако, не сосредотачиваться исключительно на коде, разработанном с применением формального подхода, а использовать и сами формальные спецификации. Это поможет разрешить конфликт между универсальностью и специализацией. Формальные спецификации пишутся на высоком уровне абстракции, в идеале без какого бы то ни было уклона в сторону конкретной реализации. Лишь затем, в процессе уточнения, мы переводим их во все более и более конкретные представления и завершаем процесс текстом на языке программирования. Использование не исходного кода, а спецификаций допускает множество различных реализаций во множестве различных сред и дает возможность выбрать наиболее подходящую реализацию для заданной среды. Таким путем даже большие компоненты (от которых больше отдача) можно сделать универсальными и многократно используемыми.
В рамках формальной разработки может быть использован даже код, написанный ранее (без применения ФМ). Исследовался метод "обратной разработки" (reverse engineering) допотопных программ (в основном на Коболе), позволяющий на основе интерактивного подхода с применением специальных инструментальных средств получать из программы ее формальную спецификацию с сопутствующей документацией, которые затем можно развить в лучше структурированную и более понятную программу [11]. Этот метод успешно применялся к программам, насчитывающим десятки тысяч строк. После того как такая процедура однажды произведена, становится возможным сопровождать уже формальную спецификацию, а не только программный код. Таким образом, они будут увязаны друг с другом.
Заключение
Итак, мы попытались порассуждать о том, как успешно применять ФМ в промышленных разработках.
Принимая решение о том, на каком конкретно методе остановиться, необходимо иметь свежую информацию. Нотации и методы, из которых можно выбирать, существуют в изобилии, хотя тех, которые использовались в разработке промышленных систем, существенно меньше [1].
Для успешного промышленного внедрения ФМ и успеха любого ФМ-проекта жизненно важно выбрать подходящую нотацию (нотации) и включить ее (их) в существующий процесс разработки, обеспечив, чтобы как можно больше имеющихся правил и процедур сохранились неизменными.
Нельзя ни на минуту забывать, что программы разрабатываются людьми и что ФМ не гарантируют отсутствия ошибок. И тем не менее, если мы будем всегда помнить об ограниченности собственных возможностей, признавать эту ограниченность, учиться на своих и чужих ошибках, если будем стремиться применять лучшее из существующего, проверять свою работу соответствующими тестами и с помощью автоматических средств, мы сможем успешно применять ФМ в разработке высоконадежных промышленных систем.
Благодарности
Авторы благодарят Роберта Франса и Ларри Полсона за замечания по первому варианту этой статьи, а также Энди Лэмберта за рисунок к нашей (неформальной) спецификации.
Литература
1. Austin S., Parkin G.I. Formal Methods: A Survey. National Physical Laboratory, Queens Road, Teddington, Middlesex, TW11 0LW, UK, March 1993.
2. Barwise J. Mathematical Proofs of Computer System Correctness // Notices of the American Mathematical Society, 1989, v. 36, # 7, p. 844-851.
3. Biggerstaff, T.J., Perlis A.J. (eds.). Software Reusability. Vol. 1: Concepts and Models, preface. ACM Press, 1989.
4. Boehm B.W. A Spiral Model of Software Development and Maintenance // IEEE Computer, 1988, v. 21, # 5, p. 61-72.
5. Bowen J.P. Formal Specification in Z as a Design and Documentation Tool // Proc. Second IEE/BCS Conference, Software Engineering 88, Liverpool, UK, 11-15 July 1988. IEE Conference Publication, # 290, 1988, p. 164-168.
6. Bowen J.P. Formal Methods in Safety-Critical Standards // Proc. Software Engineering Standards Symposium (SESS'93), Brighton, UK, 30 August - 3 September 1993. IEEE Computer Society Press, 1993, p. 168-177.
7. Bowen J.P., Breuer P.T., Lano K.C. Formal Specifications in Software Maintenance: From code to Z++ and back again // Information and Software Technology, 1993, v. 35, # 11/12, p. 679-690.
8. Bowen J.P., Hinchey M.G. Formal Methods and Safety-Critical Standards // IEEE Computer, August 1994.
9. Bowen J.P., Hall J.A. (eds.). Z User Workshop, Cambridge 1994. Springer-Verlag, Workshops in Computing, 1994.
10. Breuer P.T., Bowen J.P. Towards Correct Executable Semantics for Z // [9], p. 185-209.
11. Capers Jones T. Reusability in Programming: A Survey of the State of the Art // IEEE Transactions on Software Engineering, September 1984, p. 488-494.
12. Carrington D., Stocks P. A Tale of Two Paradigms: Formal Methods and Software Testing // [9], p. 51-68.
13. Dijkstra E.W. Why Correctness must be a Mathematical Concern // Boyer R.S., Moore J.S. (eds.). The Correctness Problem in Computer Science. Academic Press, 1981.
14. Fetzer J.H. Program Verification: The Very Idea // Communications of the ACM, 1988, v. 31, p. 1048-1063.
15. Gladden G.R. Stop the Life Cycle - I Want to Get Off // ACM Software Engineering Notes, 1982, v.7, # 2, p. 35-39.
16. Hinchey M.G. Towards Visual Methods. Готовится к печати.
17. McCracken D.D., Jackson M.A. Life Cycle Concept Considered Harmful // ACM Software Engineering Notes, 1982, v. 7, # 2, p. 28-32.
18. Parnas D.L., Madey J. Functional Documentation for Computer Systems Engineering. Version 2. CRL Report # 237, TRIO, Communications Research Laboratory, Faculty of Engineering, McMaster University, Hamilton, Ontario, Canada L8S 4K1, September 1991.
19. Royce W.W. Managing the Development of Large Software Systems // Proc. WESTCON'70, August 1970. Proc. 9th International Conference on Software Engineering. IEEE Press, 1987.
* Можно, правда, вспомнить, что П.Т. Барнэм говорил: "Каждую минуту рождается еще один простофиля".