Ключ

Ключ
	Скриншот KeyY 1.4
Разработчик(и)	Технологический институт Карлсруэ , Технический университет Дармштадта , Технологический университет Чалмерса
Стабильная версия	2.10.0 / 23 декабря 2021 г.
Написано в	Ява
Операционная система	Linux, Mac, Windows, Солярис
Доступно в	Английский
Тип	Формальная проверка
Лицензия	лицензия GPL
Веб-сайт	www .key-проект .org

Инструмент KeY используется для формальной проверки программ Java . Он принимает спецификации, написанные на языке моделирования Java , для исходных файлов Java. Они преобразуются в теоремы динамической логики , а затем сравниваются с семантикой программы, которая также определяется в терминах динамической логики. KeyY обладает значительной мощью, поскольку поддерживает как интерактивное (т. е. вручную), так и полностью автоматизированное доказательство правильности. Неудачные попытки проверки могут быть использованы для более эффективной отладки или тестирования на основе проверки . К KeyY было сделано несколько расширений, позволяющих применять его для проверки программ на языке C или гибридных систем . KeyY разработан совместно Технологическим институтом Карлсруэ , Германия; Технический университет Дармштадта , Германия; и Технологического университета Чалмерса в Гетеборге, Швеция, и распространяется по лицензии GPL .

Обзор

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

Java-карта DL

Теоретической основой KeY является формальная логика под названием Java Card DL. DL означает динамическую логику. Это версия динамической логики первого порядка , адаптированная для программ Java Card. Таким образом, он, например, допускает такие утверждения (формулы), как $\phi \rightarrow [\alpha ]\psi$ , что интуитивно говорит о том, что постусловие $\psi$ должен сохраняться во всех состояниях программы, доступных при выполнении программы Java Card. $\alpha$ в любом состоянии, удовлетворяющем предварительному условию $\phi$ . Это эквивалентно $\{\phi \}\alpha \{\psi \}$ в исчислении Хоара, если $\phi$ и $\psi$ имеют чисто первый порядок. Динамическая логика, однако, расширяет логику Хоара тем, что формулы могут содержать вложенные модальности программы, такие как $[\alpha ]$ , или возможна количественная оценка по формулам, содержащим модальности. Существует также двойная модальность $\langle \alpha \rangle$ что включает в себя прекращение действия . Эту динамическую логику можно рассматривать как специальную мультимодальную логику (с бесконечным числом модальностей), где для каждого блока Java $\alpha$ есть модальности $[\alpha ]$ и $\langle \alpha \rangle$ .

Компонент вычета

В основе системы KeY лежит средство доказательства теорем первого порядка, основанное на секвенциальном исчислении . Секвенция имеет вид $\Gamma \vdash \Delta$ где $\Gamma$ (предположения) и $\Delta$ (предложения) — это наборы формул с интуитивным смыслом, который $\bigwedge _{\gamma \in \Gamma }\gamma \rightarrow \bigvee _{\delta \in \Delta }\delta$ соответствует действительности. С помощью дедукции показано, что начальная секвенция, представляющая обязанность доказательства, может быть построена только из фундаментальных аксиом первого порядка (таких как равенство $e\ {\dot {=}}\ e$ ).

Символическое выполнение кода Java

При этом модальности программы устраняются символьным выполнением . Например, формула $x\ {\dot {=}}\ 0\rightarrow [x++;]x\ {\dot {=}}\ 1$ логически эквивалентно $x\ {\dot {=}}\ 0\rightarrow x\ {\dot {=}}\ 0$ . Как показывает этот пример, символическое выполнение в динамической логике очень похоже на вычисление слабейших предусловий . Оба $[\alpha ]\psi$ и $wp(\alpha ,\psi )$ по сути обозначают одно и то же, за двумя исключениями: во-первых, $wp$ является функцией некоторого метаисчисления, в то время как $[\alpha ]\psi$ действительно является формулой данного исчисления. программе Во-вторых, символическое выполнение выполняется по всей так же, как и при фактическом выполнении. Чтобы сохранить промежуточные результаты заданий, KeY вводит концепцию, называемую обновлениями , которая аналогична заменам, но применяется только после устранения модальности программы. Синтаксически обновления состоят из параллельных (без побочных эффектов) присваиваний, записанных в фигурных скобках перед модальностью. Пример символьного выполнения с обновлениями: $[x=3;x=x+1;]x\ {\dot {=}}\ 4$ преобразуется в $\{x:=3\}[x=x+1;]x\ {\dot {=}}\ 4$ на первом этапе и $\{x:=4\}[]x\ {\dot {=}}\ 4$ на втором этапе. Тогда модальность пуста, и «обратное применение» обновления постусловия дает предварительное условие, в котором $x$ может принимать любое значение.

Пример

Предположим, кто-то хочет доказать, что следующий метод вычисляет произведение некоторых неотрицательных целых чисел. $x$ и $y$ .

int foo (int x, int y) {
    int z = 0;
    while (y > 0)
        if (y % 2 == 0) {
            x = x*2;
            y = y/2;
        } else {
            y = y/2;
            z = z+x;
            x = x*2;
        }
    return z;
}

Таким образом, доказательство начинается с посылки $x\geq 0\land y\geq 0$ и вывод, который нужно показать $z\ {\dot {=}}\ x\cdot y$ . Обратите внимание, что таблицы секвенционных исчислений обычно пишутся «в перевернутом виде», т. е. начальная секвенция оказывается внизу, а шаги вывода идут вверх. Доказательство можно увидеть на рисунке справа.

Результирующее дерево доказательства

Дополнительные возможности

Отладчик символического выполнения

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

Генератор тестовых примеров

KeY можно использовать как инструмент тестирования на основе моделей , который может генерировать модульные тесты для программ Java. Модель, из которой извлекаются тестовые данные и тестовый пример, состоит из формальной спецификации (представленной в JML ) и символического дерева выполнения тестируемой реализации, которое вычисляется системой KeyY.

Распространение и варианты системы Key

KeY — бесплатное программное обеспечение, написанное на Java и лицензированное под лицензией GPL . Его можно скачать с сайта проекта в исходниках; в настоящее время нет предварительно скомпилированных двоичных файлов. Еще одна возможность: KeY можно запустить непосредственно через веб-запуск Java без необходимости компиляции и установки.

Кей-Хоар

KeY-Hoare построен на основе KeY и включает в себя исчисление Хоара с обновлениями состояния. Обновления состояний — это средство описания переходов состояний в структуре Крипке . Это исчисление можно рассматривать как подмножество того, которое используется в основной ветви KeY. Из-за простоты исчисления Хоара эта реализация по сути предназначена для иллюстрации формальных методов на курсах бакалавриата.

Кеймаэра/КеймаэраX

KeYmaera [1] (ранее называвшийся HyKeY) — это инструмент дедуктивной проверки гибридных систем, основанный на исчислении дифференциальной динамической логики dL [2] . Он расширяет инструмент KeY системами компьютерной алгебры, такими как Mathematica , а также соответствующими алгоритмами и стратегиями доказательства, так что его можно использовать для практической проверки гибридных систем .

KeYmaera был разработан в Ольденбургском университете и Университете Карнеги-Меллон . Название инструмента было выбрано как , гибридного омофон Химеры животного из древнегреческой мифологии.

KeYmaeraX [3], разработанный в Университете Карнеги-Меллон, является преемником KeYmaera. Он был полностью переписан.

Ключ для C

KeY for C — это адаптация системы Key к MISRA C , подмножеству языка программирования C. Этот вариант больше не поддерживается.

АСМКей

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

Ссылки

^ «Скачать – Проект KeyY» . key-project.org . Проверено 13 апреля 2021 г.

Источники

Верификация объектно-ориентированного программного обеспечения: подход Key . Бернхард Беккерт, Райнер Хэнле, Петер Х. Шмитт (ред.). Спрингер , 2007. ISBN 978-3-540-68977-5 .
Дедуктивная верификация программного обеспечения – Ключевая книга: от теории к практике . Вольфганг Арендт, Бернхард Беккерт, Рихард Бубель, Райнер Хэнле, Петер Х. Шмитт, Маттиас Ульбрих (ред.). Спрингер , 2016. ISBN 978-3-319-49812-6
Сравнение инструментов для обучения формальной верификации программного обеспечения . Инго Файнерер и Гернот Зальцер. Спрингер , 2008 г.
Программирование с доказательствами: языковые подходы к полностью корректному программному обеспечению . Аарон Стамп. Проверенное программное обеспечение: теории, инструменты и эксперименты, 2005.
Высокая гарантия (безопасности и безопасности) и бесплатное программное обеспечение с открытым исходным кодом (FLOSS) . Дэвид Уилер, 2009 г.

Внешние ссылки

[1] «Скачать – Проект KeyY» . key-project.org . Проверено 13 апреля 2021 г.

[1]