Safe Object-Oriented Software: The Verified Design-By-Contract Paradigm. David Crocker, Escher Technologies Ltd. Aldershot, United Kingdom (dcrocker@eschertech.com).

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

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

Пусть S – это инструкция программы. Вызывающий код ожидает, что после выполнения S будет выполнено некоторое постусловие R (здесь R – это предикат от состояния программы, или математическое описание состояния, которое разработчик ожидает получить после выполнения S). Вообще говоря, это будет верно, только если перед вызовом S выполнено также некоторое предусловие P. Таким образом, чтобы проверить, что постусловие R будет выполнено после вызова S, необходимо проверить следующие утверждения:

1. Если выполнено P, то выполнение инструкции S переведет программу в состояние, удовлетворяющее R.
2. P всегда выполнено перед вызовом S.

В Проектировании по контракту S – это вызов метода. Для каждого метода документируются его предусловия и постусловия. Требования корректности выражаются в форме контракта между методом и кодом, его вызывающим:

1. Метод S «обещает», что, будучи вызванным в состоянии, удовлетворящим P, он завершит работу в состоянии, удовлетворяющим постусловию R.
2. Вызывающий код «обещает», что программа будет удовлетворять предусловию P в момент вызова S. В ответ он (вызывающий код) ожидает, что после возврата управления будет выполнено постусловие R.

В качестве примера рассмотрим систему, позволяющую отображать на экране различные объекты. Пусть все такие объекты реализуют интерфейс DisplayedElement, частью которого является метод draw(), по которому и происходит отрисовка. В качестве параметров этот метод принимает координаты и размер прямоугольника, в котором объект должен быть отображен. Рассмотрим, как подход Проектирование по контракту может быть применен к этому методу:

1. Код, вызывающий draw(), обещает, что размер прямоугольника, переданный в draw(), не меньше, чем размер отображаемого элемента.
2. Метод draw() обещает, что после возврата управления объект будет отрисован в указанной области и что вся остальная часть экрана не изменится.

Также естественным будет требование того, что объекты на экране не пересекаются и не выходят за границы экрана. Это можно было бы описать в виде предусловий и постусловий для каждого из методов класса экрана Display, но Проектирование по контракту предлагает для таких условий более простой механизм — инварианты класса. Это глобальные условия, ограничения целостности, характеризующие данный класс. Вызывающий код может расчитывать, что это условие будет выполнено в любой момент времени.

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

1. Вызывающий код удовлетворяет предусловию номинальной цели.
2. Фактическая цель гарантирует удовлетворение определенного постусловия, если выполнено ее предусловие.
3. В ответ, вызывающий код может предполагает, что постусловие номинальной цели также выполнено.
4. Выполнение предусловия номинальной цели является достаточным для выполнения предусловия фактической цели.
5. Выполнение постусловия фактической цели достаточно для выполнения постусловия номинальной цели.

Другими словами, п.п. 4-5 означают, что при наследовании реализации методов класса-наследника могут ослаблять предусловия, но должны иметь не менее сильные постусловия, чем переопределяемые методы класса-родителя (интерфейса).

Проектирование по контракту может быть реализовано множеством способов, от неформальных комментариев (документирование кода), оставляющих всю ответственность за разработчиком, до строгих описаний, которые могут проверяться автоматически. Так, существуют языки программирования со встроенной поддержкой контрактов (см. Eiffel, iContract). Но в этом случае ответственность за полноту описания контрактов и за их корректное использование при наследовании лежит на разработчике. Второй подход основан на документировании и расширенном статическом анализе кода. Наиболее продвинутым проектом, реализующим этот подход, является ESC/Java. Он представляет собой аннотированный Java, и позволяет находить действительно большое количество ошибок. Однако, анализатор ESC/Java не способен обнаружить все ошибки (или полное их отсутствие) или, в более общем смысле, что программа удовлетворяет указанным требованиям.

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

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

Проект «Escher» был задуман как набор инструментов, поддерживающих парадигму Проектирования по контракту с верификацией с практически 100% автоматизацией процесса верификации. Далее будут рассмотрены его основные положения.

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

Эти принципы были реализованы в инструменте Escher Tool, который был выпущен в виде коммерческого продукта Perfect Developer. Инструмент основан на нотации, разработанной для описания функциональных требований, спецификации (частью которой являются контракты) и коде реализации. Пример описания для PerfectDeveloper метода draw() из рассмотренного ранее примера:

Здесь ключевое слово pre предваряет предусловия, слово assert – постусловия. Слово ghost указывает на то, что для функции isDisplayedOn код генерироваться не будет, эта функция нужна для описания постусловия.

Как и большинство других аналогичных инструментов, PerfectDeveloper выполняет проверку типов. Условие верификации — это математическое утверждение, и для корректной программы все условия верификации — это теоремы. Таким образом, этот инструмент проверяет, за исключением небольшого числа документированных ограничений, что, если все условия верификации программы — верные теоремы, то программа корректно реализует спецификацию. В процессе генерации кода, инструмент вычисляет текущее состояние программы и, с его учетом, везде, где необходимо проверить условие верификации, генерирует теорему (здесь текущее состояние — это вычисленное состояние программы на данный момент, требуемое условие — это предусловие или постусловие метода, или инвариант класса):

текущее состояние => требуемое условие  

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

Perfect Developer преобразует доказательства теорем (которые, как правило, человеку очень сложно разобрать) в специальный формат, разработанный как раз для того, чтобы быть доступным для человеческого понимания. Таким образом, все доказательства могут быть проверены вручную, если это требуется. Также Perfect Developer в качестве результатов, в том числе, предоставляет отчеты об ошибках.

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

Система была протестирована на трех проектах, генерировался код на С++. Сделана оценка, что при использовании системы Perfect Developer разработчик пишет от 1/3 до ¼ того объема кода, который он написал бы на чистом С++.

Объектно-ориентированный подход, очевидно, позволяет в значительной степени оптимизировать процесс разработки программного обеспечения. И сегодня, вместо того, чтобы отказываться от преимуществ ООП с тем, чтобы использовать старые средства статического анализа, общество должно скорее искать способы работы с новыми технологиями. Благодаря Perfect Developer разработчики систем, требовательных к безопасности, наконец, получили возможность использовать все преимущества подхода ООП в своих проектах.

1. Barnes J (1997). High Integrity Ada: the SPARK Approach. Addison-Wesley, England.
2. Chalin P (2003). Improving JML: For a Safer and More Effective Language. FME 2003: Formal Methods (Springer LNCS 2805): 440.
3. Flanagan C, Leino K.R.M, Lillibridge M, Nelson C, Saxe J and Stata R (2002). Extended static checking for Java. Proc. PLDI, SIGPLAN Notices 37(5): 234-245.
4. Hoare C.A.R (1969). An axiomatic basis for computer programming, Communications of the ACM 12: 576-580.
5. Jones R and Lins R (1996). Garbage Collection. Wiley, England.
6. Kramer R (1998). iContract - The Java™ Design by Contract™ Tool. Technology of Object-Oriented Languages and Systems, August 03 – 07: 295.
7. Mamrak A and Sinha S (1999): A case study: productivity and quality gains using an object-oriented framework. Software - Practice and Experience 29(6): 501-518.
8. Meyer B (1988). Object-Oriented Software Construction. Prentice Hall, England.
9. Meyer B (1992). Eif el: The Language. Prentice Hall.
10. OOTiA (2003). Handbook for Object-Oriented Technology in Aviation (draft). OOTiA Workshop Proceedings, March 5, 2003.
11. Port D and McArthur M (1999). A Study of Productivity and Efficiency for Object-Oriented Methods and Languages. APSEC 1999 (IEEE Computer Society): 128-.
12. Potok T, Vouk M and Rindos A (1999). Productivity Analysis of Object-Oriented Software Developed in a Commercial Environment. Software - Practice and Experience 29(10): 833-847.
13. RTJ (2003). http://www.rtj.org (30 September 2003).
14. Warren J.H and Oldman R.D (2003). A Rigorous Specification Technique for High Quality Software, Proceedings of the Twelfth Safety-Critical Systems Symposium, Springer-Verlag (London).