Как стать автором
Обновить

Программирование по контракту в Java, с использованием библиотеки COFOJA от Google

Время на прочтение9 мин
Количество просмотров7.4K
image

Для чего используется



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

Как и любая другая проверка, она позволяет повысить надежность программы, гарантируя корректность данных на входе и выходе. Либо, понизить (при некорректном использовании).

В отличие от assert’ов, проверки выполняются в runtime, т.е., непосредственно во время выполнения программы и присутствуют в релизной версии.

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



Пример

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

У класса есть методы: getHours(), getMinutes(), getSeconds() иsetHours(), setMinutes(), setSeconds(), соответственно.

Опишем его (часть языковых конструкций и механизмов опущена, либо упрощена для краткости):

class Time<br>{<br>    intHOURS;<br>    intMINUTES;<br>    intSECONDS;<br><br>    getHours();<br>    {<br>        returnHOURS;<br>    }<br>    <br>    getMinutes();<br>    {<br>        return MINUTES;<br>    }<br><br>    getSeconds()<br>    {<br>        return SECONDS;<br>    }<br><br>    setHours(newHOURS);<br>    {<br>        HOURS = newHOURS;<br>    }<br><br>    setMinutes(newMINUTES);<br>    {<br>        MINUTES = newMINUTES;<br>    }<br><br>    setSeconds(newSECONDS)<br>    {<br>        SECONDS = newSECONDS;<br>    }<br>}<br><br>* This source code was highlighted with Source Code Highlighter.


Необходимо гарантировать, что данный класс будет возвращать корректные данные, либо, вообще не будет работать (Исходя из принципа «Мертвые программы не лгут»).

Как это можно сделать? Проверкой данных на корректность.

Путь 1: Колхоз



Для краткости, опустим некоторые детали и повторяющиеся конструкции класса Time.

class Time<br>{<br>    getHours();<br>    {<br>        if (HOURS<0 ||HOURS>23) <br>            throw GREAT_Time_Exception ;<br><br>        return HOURS;<br>    }<br><br>    setHours(newHOURS);<br>    {<br>        if (newHOURS<0 ||newHOURS>23) <br>            throw GREAT_Time_Exception ;<br><br>        HOURS = newHOURS;<br>    }<br>}<br><br>* This source code was highlighted with Source Code Highlighter.


Недостатки: Неочевидность проверки. Необходимость писать кучу кода вручную. Только что, мы попытались применить методику программирования по контракту. Но, это ПРОВААААААЛ! Почему? Смотрим дальше.

Путь 2: Используем готовое, изящное решение.



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

Чем и воспользовались несколько сотрудников компании Google (David Morgan, Andreas Leitner, Nhat Minh Le – «Contracts for Java 20% Team»). В свободное время, они разработали библиотеку-препроцессор аннотаций COFOJA, позволяющую реализовать методологию программирования по контракту в Java.

Давайте попробуем использовать ее для нашего класса Time:

@Contracted // говорит о том, что класс использует контракты – для отображения в IDE<br>class Time<br>{<br>    @Ensures ({“result >= 0”,“result <= 23” })<br>    getHours();<br>    {<br>        return HOURS;<br>    }<br><br>    @Requires ({“newHOURS>= 0”,“newHOURS<= 23” })<br>    @Ensures (“HOURS == newHOURS”)<br>    // или<br>    // @Ensures (“getHours()== newHOURS”)<br>    setHours(newHOURS);<br>    {<br>        HOURS = newHOURS;<br>    }<br>}<br><br>* This source code was highlighted with Source Code Highlighter.


@Requires – буквально означает, «Убедиться, что ДО выполнения подпрограммы («условие выполняется»)» Иначе – бросить исключение.

@Ensures – буквально означает, «Убедиться, что ПОСЛЕ выполнения подпрограммы ( «условие выполняется») »

Здесь мы видим, что, как и в Пути1, осуществляется проверка предварительных и постусловий для наших методов. В чем разница? Разница в том, что во втором случае это более наглядно и удобно.

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

Из чего состоит библиотека.



com.google.java.contract.* — основное пространство имен библиотеки COFOJA.

В нем располагается реализация следующих аннотаций:


@Contracted — подсказка для IDE, говорит о том, что класс использует контракты.

@Invariant — Инварианты определяют глобальные свойства некоторого класса, которые должны соблюдаться после его создания на протяжении всего времени жизни.

@Requires — определяет предусловия – то, что должно быть истинно ДО входа в метод или функцию.

@Ensures — определяет постусловия – то, что должно быть истинно ПОСЛЕ выхода из метода или функции.

@ThrowEnsures — позволяет генерировать заданное исключение при выполнении проверки постусловий.


На что обратить внимание.


@Ensures и @Requires у каждого метода может быть только по одной. Если необходимо проверить несколько условий – используйте запись условий в { }:

@Ensures    ( { “Условие1”, “ … ”, “УсловиеN” } )<br><br>@Requires    ( { “Условие1”, “ … ”, “УсловиеN” } )<br><br>* This source code was highlighted with Source Code Highlighter.


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

Так же, существует возможность генерировать свои собственные исключения при проверке постусловий.
Для этого служит аннотация @ThrowEnsures. Ее синтаксис:

@ThrowEnsures    ({"КлассИсключения", "ПостУсловие"})<br><br>@ThrowEnsures    ({<br>                    "КлассИсключения1", "ПостУсловие1",<br>                    ...<br>                    "КлассИсключенияN", "ПостУсловиеN",<br>                })<br><br>* This source code was highlighted with Source Code Highlighter.


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

Конфигурирование IDE для автоматической работы с контрактами.



Eclipse*


Подготовка:
  1. Качаем/добываем любым доступным образом (вплоть до компиляции из исходных кодов) пакет cofoja.jar.
  2. Запускаем IDE Eclipse, создаем новый проект.
  3. Копируем файл cofoja.jar в корневую папку проекта.


Теперь приступим к конфигурированию проекта:

  1. Project ->Properties->Java Build Path, вкладка Libraries ->Add JARs, в появившемся окне выбираем наш файл cofoja.jar
  2. На этом этапе IDE Eclipse начнет распознавать аннотации контрактов. Но, это еще не все. Нужно указать IDE Eclipse на то, что при компиляции нашего проекта нужно использовать ВНЕШНИЙ препроцессор аннотаций.

    Для этого: заходим в меню проекта Project ->Properties->Java Compiler->Annotation Processing, ставим все галочки, добавляем (key) два ключа (Processor Options):

    com.google.java.contract.classpath – абсолютный путь к файлу с обработчиком пользовательских аннотаций – cofoja.jar.
    com.google.java.contract.classoutput – абсолютный путь к папке, в которую компилируются все классы проекта (папка bin).

    Пример:

    com.google.java.contract.classpath = C:\java\eclipseWorkspace\JavaContractsTest\ccofoja.jar
    com.google.java.contract.classoutput = C:\java\eclipseWorkspace\JavaContractsTest\bin

    В подкатегории Factory Path ставим галочку Enable Project Specific Settings, далее – Add JARs ->выбираем наш процессор аннотаций cofoja.jar .
  3. После этого, при компиляции проекта, должен задействоваться внешний процессор аннотаций, который мы только что настроили. Но, это еще не все.
  4. Осталось добавить один параметр виртуальной машины для запуска нашего кода с проверкой контрактов. Для этого, в Run Configurations -> Arguments в поле VM Arguments указываем: -javaagent:cofoja.jar
  5. Формат:
  6. ( -javaagent:<Имя_файла_обрабочика_контрактов>.jar )
  7. Готово. Можно приступать к написанию кода. После этого, при компиляции проекта, ошибки в аннотациях контрактов будут выдаваться прямо в IDE.


NetBeans* **



1. Качаем/добываем любым доступным образом (вплоть до компиляции из исходных кодов) пакет cofoja.jar.

2. Запускаем IDE NetBeans, создаем новый проект.

3. Копируем файл cofoja.jar в корневую папку проекта.

4. Теперь приступим к конфигурированию проекта.

   a. Project ->Properties-> Libraries

Во вкладках Compile, Processor, Run добавить наш файл cofoja.jar (кнопка Add JARs)

   b. Переходим на Build -> Compiling

Ставим галочки на пунктах Enable Annotation Processing, Enable Annotation Processing in Editor, затем щелкаем на кнопке Add, и добавляем следующую строку: com.google.java.contract.classpath

   c. Переходим на вкладку Run
В VM Options добавляем: -javaagent:cofoja.jar (имя нашего файла-обработчика контрактов)
Формат:
( -javaagent:<Имя_файла_обрабочика_контрактов>.jar )

   d. Готово. Можно приступать к написанию кода. После этого, при компиляции проекта, ошибки в аннотациях контрактов будут выдаваться прямо в IDE.


Javac – компилируем вручную, с аннотациями



1. Качаем/добываем любым доступным образом (вплоть до компиляции из исходных кодов) пакет cofoja.jar.

2. Кладем файл cofoja.jar в одну папку с классами, которые собираемся скомпилировать, либо, указываем к нему полный путь.

3. В командной строке набираем: javac -cp cofoja.jar MyClass.java

Компилируем. Анализируем сообщения об ошибках, если таковые были, исправляем, компилируем повторно.

Ключ компилятора -cp позволяет указать препроцессор аннотаций. Далее следуют имена файлов с классами вашей программы.

Синтаксис такой:
javac -cp <имя_файла_с_процессором_аннотаций> <Класс1.java> <КлассN.java>


*Примечание: Если после проделанных действий вы столкнетесь с сообщением об ошибке, в котором будет сказано, что невозможно найти компилятор (JavaBuilder) – добавьте в системную переменную PATH каталог с компилятором javac (JDK\bin). После модификации этой переменной, чтобы изменения вступили в силу, необходимо перезагрузиться (для Windows 2k/XP, Windows 7 в этом не нуждается. В Linux, возможно, придется перелогиниться – в зависимости от используемого shell’а ).

**Примечание: Если в вашем NetBeans нет таких пунктов меню, возможно, вы используете старую версию. В NetBeans 6.9 поддержка аннотаций точно присутствует – скачайте и используйте ее.

Ссылки


Теги:
Хабы:
Всего голосов 29: ↑24 и ↓5+19
Комментарии30

Публикации