Перевод статьи англ.. Daikon для динамического обнаружения вероятных ин
 Скачать 37.47 Kb.
|
|
Система Daikon для динамического обнаружения вероятных инвариантов Аннотация Daikon — это реализация(реализует) динамического обнаружения вероятных инвариантов; то есть детектор инвариантов Daikon сообщает(отчитывается) о вероятных инвариантах программы. Инвариант — это свойство, которое остается (содержится) в определенной точке или точках программы; они часто используются в операторе, который находятся внутри утверждений, в документации и формальных спецификациях. Примеры включают константы (x=a), ненулевые значения (x6=0), нахождение в диапазоне (a≤x≤b), линейные отношения (y=ax+b), упорядоченность(сортировка) (x≤y), функции из библиотеки (x=fn(y)), включение (x∈y), сортировка (x отсортрован) и многое другое. Пользователи могут расширять Daikon для добавления дополнительных инвариантов. Динамическое обнаружение инвариантов запускает программу, наблюдает за значениями, вычисляемыми программой, а затем сообщает о свойствах, которые были верны в отношении наблюдаемых выполнений. Динамическое обнаружение инвариантов — это техника(метод) машинного обучения, который можно применять к произвольным данным. Daikon может обнаруживать инварианты в программах на C, C++, Java и Perl, а также в источниках данных со структурой записей; Daikon легко расширяется для других приложений. Инварианты могут быть полезны для понимания программ и множества других приложений. Выходные данные Daikon были использованы для генерации тестовых примеров, прогнозирования несовместимости при интеграции компонентов, автоматизации доказательства теорем, исправления несогласованных данных структуры и проверку достоверности потоков данных, среди прочих задач.(Pres. Perf) Daikon находится в свободном доступе в исходном и бинарном виде вместе с обширной документацией по адресу http://pag.csail.mit.edu/daikon/. Введение В данной статье представлен Daikon – полнофункциональная и надежная реализация динамического обнаружения инвариантов. Инварианты раскрывают структуры данных и алгоритмы и полезны для ручного и автоматизированного программирования задач, от проектирования до обслуживания(сопровождения). Для примера, они определяют свойства программы, которые должны быть сохранены, когда, модифицируется код. Несмотря на их преимущества, инварианты обычно отсутствуют в программах. Альтернативой ожиданию того, что программисты будут полностью снабжать код инвариантами - является автоматический вывод вероятных инвариантов из выполнения программы. Для некоторых определенных важных задач динамически вводимые свойства предпочтительнее написанной человеком спецификации. Выводом Daikon является набор вероятных инвариантов, которые статистически обоснованы выполнением трассировки. Результат может быть использован в качестве документации, добавляться в исходный текст программы в виде утверждений или использоваться в качестве входных данных для других инструментов (см. раздел 4). Daikon свободно доступен для загрузки с http://pag.csail.mit.edu/daikon/. Дистрибутив включает в себя как исходный код, так и документацию, и лицензия Daikon разрешает неограниченное использование. Эта статья знакомит с (представляет) Daikon, но для получения наиболее полной информации следует обратиться к руководствам пользователя и разработчика. Пример В качестве примера рассмотрим Java-класс StackAr, который реализует стек с фиксированным максимальным размером. Он имеет следующие поля: Object[] theArray; // Массив, содержащий элементы стека. int topOfStack; // Индекс верхнего элемента. -1, если стек пуст. и реализует следующие методы: void push(Object x) // Вставить x void pop() // Удаление последнего вставленного элемента Object top() // Возврат последнего вставленного элемента Object topAndPop() // Удаление и возврат последнего вставленного элемента boolean isEmpty() // Вернуть true если пустой; иначе false boolean isFull() // Вернуть true если полный; иначе false void makeEmpty() // Удалить все элементы StackAr может быть реализован через простой тестовый класс StackArTester. Например: java DataStructures.StackArTester Следующая команда инструментирует аналогичный запуск StackAr и передает полученные результаты выполнения трассировки в Daikon. java daikon.Chicory --daikon DataStructures.StackArTester (Chicory - это инструмент Daikon для Java.) Вероятные инварианты записываются на стандартный вывод (т.е. в консоль) и также сохраняются в сериализованном файле для последующей обработки. Программы C/C + + обрабатываются(управляются) аналогичным образом. Если программа C/C + + обычно запускается с помощью команды ./program -f input тогда команда kvasir-dtrace --dtrace-file=- ./program -f input | java daikon.Daikon будет инструментировать программу с помощью Kvasir (инструмент для C/C + +) и передаст полученную результат выполнения трассировки в Daikon. Вывод Daikon состоит из пред и пост условий процедуры, а также инвариантов объекта, которые содержаться при каждом входе и выходе публичного входа и выхода из метода. На рис. 1 показана часть вывода Daikon, включая объектные инварианты и процедурные инварианты для конструктора и метода isFull. this.theArray != null Ссылка theArray никогда не наблюдалась как нулевая(не являлась нулевой) после того, как она была установлена в конструкторе. Таким образом, методы могут безопасно ссылаться на него без проверки на null. this.theArray.getClass() == java.lang.Object[].class Класс времени выполнения Array - Object[]. Java допускает, чтобы тип времени выполнения был подклассом объявленного типа, но в StackAr этого не произошло. this.topOfStack >= -1 this.topOfStack <= this.theArray.length – 1 topOfStack находится в диапазоне от -1 до максимального индекса массива включительно. Таким образом, он указывает на последний заполненный элемент массива элемент, а не следующий, который будет заполнен. Инварианты объектов для StackAr this.theArray != null this.theArray.getClass() == java.lang.Object[].class this.topOfStack >= -1 this.topOfStack <= this.theArray.length - 1 this.theArray[0..this.topOfStack] elements != null this.theArray[this.topOfStack+1..] elements == null Предусловия для конструктора StackAr capacity >= 0 Постусловия для конструктора StackAr orig(capacity) == this.theArray.length this.topOfStack == -1 this.theArray[] elements == null Постусловия для конструктора isFull this.theArray == orig(this.theArray) this.theArray[] == orig(this.theArray[]) this.topOfStack == orig(this.topOfStack) (return == false) <==> (this.topOfStack < this.theArray.length - 1) (return == true) <==> (this.topOfStack == this.theArray.length - 1) Рис. 1. Вывод Daikon для программы StackAr. На рисунке показаны вероятные инварианты объекта и пред- и пост- условиями для конструктора и метода метода isFull. Для метода isFull нет предварительных условий. this.theArray[0..this.topOfStack] elements != null Все элементы стека не являются нулевыми. Оказалось, что это результат работы набора тестов (который никогда не помещает null в стек), а не требование самого StackAr как такового. Это важно обратить внимание программиста на факт, что есть недостаток точек вывода в наборе тестов. this.theArray[this.topOfStack+1..] elements == null Все элементы массива, которые в данный момент не находятся в стеке, являются нулевыми. Мы можем сделать вывод, что метод pop обнуляет запись после ее возврата, что является хорошей практикой, так как позволяет собирать мусор из этих элементов. Вероятные инварианты также обнаруживаются на каждом входе и выходе метода. Они соответствуют пред и пост условиям для метода. Для конструктора StackAr существует одно предусловие: capacity >= 0 StackAr никогда не создавался с отрицательной емкостью. (Эта конкретная реализация конструктора будет неудачной, если ему передается отрицательная емкость). Постусловия для конструктора StackAr следующие: orig(capacity) == this.theArray.length Размер массива, который будет содержать стек, равен указанной емкости. this.topOfStack == -1 this.theArray[] elements == null При инициализации стек пуст, и все его элементы равны нулю. Для метода isFull нет никаких предусловий, кроме инвариантов объекта. Постусловия, следующие: this.topOfStack == orig(this.topOfStack) this.theArray == orig(this.theArray) this.theArray[] == orig(this.theArray[]) Ни индекс topOfStack, ни ссылка на массив theArray, ни содержимое массива не изменяются методом. Другими словами, метод является чистым (метод-наблюдатель). (return == true) <==> (this.topOfStack == this.theArray.length - 1) Когда isFull возвращает true, topOfStack индексирует последний элемент theArray. (return == false) <==> (this.topOfStack < this.theArray.length - 1) Когда isFull возвращает false, topOfStack индексирует элемент, предшествующий последнему элементу theArray Основные характеристики Daikon В следующих подразделах подробно описаны основные характеристики Daikon, которые позволяют использовать его в самых разных контекстах. 3.1. Ввод из многих языков программирования и других форматов данных Daikon может вычислять вероятные инварианты для программ, написанных на языках C, C++, Java и Perl (см. раздел 5.1). Daikon также может обрабатывать данные из электронных таблиц, таких как Excel, используя формат CSV (значения, разделенные запятыми); это удобно, когда Daikon работает с данными, которые не были сгенерированы программой. Относительно легко поддерживать новые языки программирования. Поддерживать новые языки программирования и форматы данных относительно просто, как это сделали некоторые пользователи (см. раздел 5.3). 3.2. Насыщенный выход Основная цель Daikon - выдавать выразительные и полезные результаты. То, какие инварианты будут сообщены, зависит от грамматики инвариантов, которые могут быть выражены детектором инвариантов, переменных, над которыми проверяются инварианты, и точек программы, в которых проверяются инварианты. Грамматика свойств. Daikon проверяет 75 различных инвариантов, включая те, которые упомянуты в аннотации, и пользователи могут легко расширить этот список (см. раздел 5.3). Проверка большого количества инвариантов повышает вероятность того, что вывод будет содержать сведения, которые необходимы человеку или инструменту; однако это также увеличивает время работы детектора инвариантов. Daikon включает оптимизацию, которая позволяет ему поддерживать большое количество возможных инвариантов (см.Раздел 5.2). Daikon также может сообщать об условных инвариантах или следствиях, например this.left 6 != null => this.left.value ≤ this.value. Daikon имеет определенные встроенные предикаты, которые он использует для поиска следствий; примерами являются: какой оператор return был выполнен в процедуре и возвращает ли булева процедура true или false. Вдобавок, Daikon может читать предикаты из файла и находить следствия на основе этих предикатов. Предикаты могут быть созданы вручную или автоматически с помощью инструментов, распространяемых вместе с Daikon, например, путем статического анализа программы или кластерного анализа значений в выполнении трассировки. Грамматика переменных. Инварианты, которые может выразить детектор инвариантов, должны быть инстанцированы над определенными переменными или другими значениями. Например,  инстанцируется над двумя переменными, из которых вторая должна бытьколлекция. Daikon может вырабатывать инварианты для: -параметров процедур и возвращаемых значений; - значений предсостояния (выраженные как orig на рис. 1), что позволяет сообщать о побочных эффектах процедуры и связях между вводом и выводом отношения; - глобальных переменных; - полей (при задании объекта a полезная дополнительная информация появляется в a.f, a.f.g и т.д.); - результатов вызовов методов без побочных эффектов (чистых, наблюдательных), таких как size() - дополнительных выражений, называемых производными переменными (всего 25). Например, если дан массив a и целое число lasti, то инварианты для a[lasti] могут представлять интерес, даже если это не переменная и даже не появляется в программе. программа. Эти типы переменных можно комбинировать; например, a.b[myObject.getX()]. Переключатель Daikon управляет тем, считаются ли только публичные поля/методы (давая внешнее, клиентское представление структуры данных), или частные (давая внутреннее, реализационное представление структуры данных). Другой переключатель управляет глубиной рассмотрения полей и чистых вызовов методов. Программные точки. Daikon проверяет инварианты на входах и выходах процедур, в результате чего получаются вероятные инварианты, которые соответствуют предусловиям и постусловиям. Он вычисляет вероятные инварианты на каждом выходе процедуры (т. е. оператор return), а также в совокупной точке выхода (как ее видит клиент) путем обобщения по отдельным точкам выхода. Вероятные инварианты объекта или инварианты класса также вычисляются в агрегированной точке программы (объектной точке). Объектная точка обобщает все объекты, которые наблюдаются при входе в публичные методы класса и выходе из них, которые передаются в методы других классов или возвращаются из методов других классов, или которые хранятся в полях объекта. 3.3. Масштабируемость Несмотря на богатые возможности, описанные в разделе 3.2, Daikon масштабируется для нетривиальных программ. Например, Daikon был использован для генерации спецификаций частичной согласованности (см. раздел 4.6) для системы автоматизации Center-TRACON Automation System (CTAS), разработанной в исследовательском центре NASA Ames. CTAS — это набор инструментов управления воздушным движением, который содержит более 1 миллион строк кода на языках C и C++. Применение Daikon к большим программам часто требует сосредоточения Daikon на подмножестве программы, или уменьшения количества производных переменных или даже инвариантов, которые рассматривает Daikon. Все это можно можно сделать с помощью аргументов командной строки. 3.4. Фильтрация инвариантов Динамическое определение инвариантов проверяет потенциальные инварианты на соответствие наблюдаемым значениям во время выполнения. Как и при любом динамическом анализе или технике машинного обучения, существует возможность чрезмерной подгонки (чрезмерного обобщения), сообщая о свойствах, которые верны для тренировочных прогонов, но не верны в целом. Например, если имеется недостаточное количество, наблюдений за конкретной переменной, закономерности, наблюдаемые для нее, могут быть простым совпадением. Daikon смягчает такие проблемы вычисляя тест нулевой гипотезы (вероятность того, что свойство появится случайно при случайном вводе), а затем сообщает о свойстве, только если его вероятность меньше заданного пользователем доверительного параметра. Избыточные инварианты. Любой инвариант, который логически подразумевается другими инвариантами, может быть удален из вывода без потери информации. Например, рассмотрим объектный инвариант this.topOfStack <= this.theArray.length-1 из рис. 1. Инвариант this.topOfStack < this.theArray.length также является истинным но не сообщается. Насколько это возможно, Daikon даже не вычисляет избыточные инварианты. Это удаляет их из выходных данных и улучшает производительность Daikon (см. раздел 5.2). Некоторые избыточные инварианты, которые не могут быть обработаны оптимизации, удаляются из выходных данных путем постобработки. Абстрактные типы. Многие переменные в программе не связаны друг с другом. Например, переменная temp может содержать текущую температуру, а переменная time - количество секунд, прошедших с 1970 года. Даже если инварианты могут существовать над этими переменными (например, temp < time), эти инварианты не интересны. Daikon может использовать абстрактную информацию о типах информацию [3] для ограничения инвариантов связанными переменными. В дистрибутив Daikon включены инструменты, которые вычисляют абстрактные типы. 3.5. Форматы вывода Daikon поддерживает широкий спектр выходных форматов. Существуют также легко добавляемые дополнительные форматы (см. раздел 5.3). Daikon. Формат вывода по умолчанию, с квантификаторами и другими возможностями. DBC. Формат Design by contract для Jtest компании Parasoft [4]. ESC. Расширенный формат статической проверки для использования инструментом ESC/Java [5]. IOA. Язык IOA для моделирования входных/выходных автоматов, который также может быть преобразован в язык анализатора теорем Isabelle [5] - Isabelle theorem prover. Java. Выражения Java, используемые в программе на Java, например, в качестве утверждений. JML. Формат Java Modeling Language [6], используемый многими инструментами [7]. Repair. Формат, используемый автоматизированными инструментами восстановления структур данных [2]. Simplify. Формат автоматизированного средства проверки теорем Simplify [8]. Инструмент annotate, входящий в состав Daikon, вставляет вероятные инварианты в исходный код в виде аннотаций 3.6. Портативность Daikon переносится(портируется) на широкий спектр платформ. Движок выводов Daikon и инструментарий Java написаны на Java, а инструментарий Perl - на Perl, языках, которые отличаются высокой портативностью. Один инструментарий на языке C специфичен для Linux/x86, а второй переносится на любую платформу, для которой доступен Purify, включая Windows, Linux и несколько коммерческих вариантов Unix. 4. Использование Вероятные инварианты, создаваемые Daikon, являются динамически генерируемым аналогом спецификации программы. Широко признано, что спецификации ценны во многих аспектах разработки программ, включая проектирование, кодирование, проверку, тестирование, оптимизацию и сопровождение. Они также улучшают понимание программистами структур данных, алгоритмов и работы программы. На практике, однако, формальные спецификации редко доступны, потому что они утомительны и трудны для написания, а когда они доступны, они могут ошибочно захватывать все свойства, от которых зависит корректность программы. Динамически генерируемая спецификация может отличаться от идеальной статической спецификации. Динамическая спецификация будет раскрывать информацию не только о целевом поведении, но и о конкретной реализации, и о среде (входных данных), в которой выполнялась программа. Для многих задач (таких как улучшение набора тестов и некоторые задачи отладки) динамическая информация может быть даже полезнее, чем статическая. 4.1. Документация Инварианты характеризуют определенные аспекты выполнения программы и документируют работу программы, алгоритмы и структуры данных. Как таковые, они способствуют пониманию программы, некоторый уровень которого является необходимым условием для решения любой задачи, связанной с программированием. Информация, которая автоматически извлекается из реализации, гарантирована быть актуальной. Автоматически определяемые инварианты полезны даже для кода, который уже документирован комментариями, утверждениями или спецификациями. Выведенные инварианты могут проверить или усовершенствовать инварианты, предоставленные программистом; программы самопроверки часто бывают устаревшими, неэффективными или неправильными [9]. 4.2. Предотвращение ошибок Инварианты могут защитить программиста от внесения изменений, которые непреднамеренно нарушают предположения, от которых зависит правильное поведение программы. Если исходный инвариант не документирован, а в меньшей степени(тем более) его зависимость, то программисту очень легко нарушить его, внеся ошибку в удаленную часть программы. Сопровождение программы вносит ошибки [10,11], и многие из них связаны с нарушением инвариантов. Когда программисты знакомятся с выводом Daikon, программисты могут избежать нарушения таких инвариантов [12]. 4.3. Отладка Хотя лучше избегать ошибок в первую очередь, инварианты также могут помочь в отладке. Raz использовал Daikon для проверки последовательных входов в потоках данных [13]. Многие авторы использовали несоответствия в выведенных инвариантах между тренировочными и реальными прогонами как индикатор ошибок в программе, на которые следует обратить внимание людей [14-16]. Динамически определяемые инварианты также могут помочь в понимании или локализации ошибок. Groce использовал различия между успешными и неудачными прогонами, чтобы дать краткое объяснение сбоев в тестировании [17]. Xie сравнивал поведение внутренних компонентов, чтобы локализовать различия между версиями программы и изолировать ошибки [18]. Liblit давал легкую методологию для определения того, какие свойства указывают на ошибку [19]. Brun использовал машинное обучение на корректных и ошибочных программах, чтобы предсказать, какие свойства в другой программе с наибольшей вероятностью указывают на скрытые ошибки [20]. 4.4. Тестирование Динамически определяемые инварианты могут рассказать о тестовом наборе так же много, как и о самой программе, поскольку свойства отражают выполнение программы над тестовым набором. Эта информация полезна при тестировании. Недостаточное покрытие значений программы является недостатком тестового набора, даже если тестовый набор покрывает каждый оператор или путь программы. Например, "x> 0" может указывать на то, что нулевые и отрицательные значения не были опробованы, а "x <10" - что большие значения не были опробованы. Более того, эти свойства точно указывают, какие исходные данные необходимы для улучшения набора тестов. Выведенные инварианты также можно использовать в качестве метрики покрытия, например, для выбора тестов и определения приоритетов; большее покрытие дает лучший набор тестов [21,22]. Динамически выявленные инварианты могут также помочь отбросить бессмысленные тесты (которые нарушают предусловия) и определить, когда тест не прошел (из-за нарушения постусловий) [23]. 4.5. Верификация Динамическое определение инвариантов предлагает вероятные инварианты на основе выполнения программы, но полученные свойства не гарантируют истинности для всех возможных исполнений. Статическая верификация проверяет, что свойства всегда истинны, но выбор цели и аннотирование программ для ввода в программу статической проверки может быть сложным и утомительным. Объединение этих методов преодолевает недостатки каждого из них: динамически обнаруженные инварианты могут аннотировать программу или предоставлять цели для статической проверки, а статическая проверка может подтвердить свойства, предложенные динамическим инструментом. Мы провели эксперименты с несколькими верификаторами программ. При использовании Java-программ и ESC/Java [5], точность Daikon (процент доказуемых свойств) составила более 95%, из которых недоказуемые свойства были вызваны, как правило, неполнотой образца. а его recall (процент найденных свойств, необходимых для верификации программы) составил более 90% [24]. Более того, пользователи, которым был предоставлен результат Daikon, статистически значимо лучше справились с задачей верификации программы. [25]. С помощью инструментов помощника доказательства около 90% лемм и тактик были сгенерированы автоматически [26], для доказательств трех распределенных алгоритмов. 4.6. Восстановление структур данных и управляющих структур Искаженные структуры данных приводят к неправильному или непредсказуемому выполнению программы. Восстановление структуры данных обновляет поврежденные структуры данных, позволяя программе продолжать работать приемлемым образом. Однако для этого требуются спецификации, предоставленные пользователем. Выход Daikon позволил автоматизировать весь процесс и в то же время обеспечить возможность проверки человеком. В результате были получены более надежные версии программ при снижении затрат по сравнению с ручной генерацией [2]. Аналогичное применение находят программы, которые динамически выбирают модальности в ответ на входные данные окружающей среды. Динамически определяемые инварианты, полученные в ходе обучения, могут указывать, какие модальности коррелируют с теми или иными внешними условиями. Периодическое переопределение действий программы (непоследовательных) во время выполнения улучшило производительность программ в реальном соревновании более чем на 50% [27]. |