Анализ состояния типов
Анализ состояния типов , иногда называемый анализом протоколов , представляет собой форму анализа программ , используемую в языках программирования . Чаще всего он применяется к объектно-ориентированным языкам. Состояния типов определяют допустимые последовательности операций, которые могут быть выполнены над экземпляром данного типа. Состояния типов, как следует из названия, связывают информацию о состоянии с переменными этого типа. Эта информация о состоянии используется для определения во время компиляции, какие операции можно вызывать для экземпляра типа. Операции, выполняемые над объектом, которые обычно выполняются только во время выполнения, выполняются с информацией о состоянии типа, которая модифицируется для совместимости с новым состоянием объекта.
Состояния типов способны представлять уточнения поведенческого типа, такие как «метод A должен быть вызван до метода B вызова , а метод C не может быть вызван между ними». Состояния типов хорошо подходят для представления ресурсов, использующих семантику открытия/закрытия, обеспечивая соблюдение семантически допустимых последовательностей, таких как «открыть, затем закрыть», в отличие от недопустимых последовательностей, таких как оставление файла в открытом состоянии. К таким ресурсам относятся элементы файловой системы, транзакции, соединения и протоколы. Например, разработчики могут захотеть указать, что файлы или сокеты должны быть открыты до того, как они будут прочитаны или записаны, и что их больше нельзя будет читать или записывать, если они закрыты. Название «состояние типа» происходит от того факта, что этот вид анализа часто моделирует каждый тип объекта как конечный автомат . В этом конечном автомате каждое состояние имеет четко определенный набор разрешенных методов/сообщений, и вызовы методов могут вызывать переходы между состояниями. Сети Петри также были предложены в качестве возможной поведенческой модели для использования с виды доработки . [1]
Анализ состояния типов был представлен Робом Стромом в 1983 году. [2] на языке сетевой реализации (NIL), разработанном в лаборатории IBM Watson Lab .Это было формализовано Стромом и Йемини в статье 1986 года. [3] в нем описывалось, как использовать состояние типа для отслеживания степени инициализации переменных, гарантируя, что операции никогда не будут применяться к неправильно инициализированным данным, и дальнейшее обобщение на языке программирования Hermes .
В последние годы в различных исследованиях были разработаны способы применения концепции состояния типа к объектно-ориентированным языкам. [4] [5]
Подход
[ редактировать ]
struct{int x;int y;int z;}. Наименьший элемент ⊥ совпадает с состоянием ∅, в котором компоненты структуры не инициализированы.
Стром и Йемини (1986) требовали, чтобы набор состояний типа для данного типа был частично упорядочен таким образом, чтобы состояние типа низшего уровня можно было получить из состояния типа высшего уровня путем отбрасывания некоторой информации. Например, int переменная в C обычно имеет состояния типа « неинициализированный » < « инициализированный », и FILE* Указатель может иметь состояния типа « нераспределенный » < « выделен, но неинициализирован » « < « инициализирован, но файл не открыт » < « файл открыт ». Более того, Стром и Йемини требуют, чтобы каждые два состояния типов имели наибольшую нижнюю границу, т. е. чтобы частичный порядок был даже пересечением -полурешеткой ; и что в каждом порядке есть наименьший элемент, всегда называемый «⊥».
Их анализ основан на том упрощении, что каждой переменной v присваивается только одно состояние типа для каждой точки текста программы; если точка p достигается двумя разными путями выполнения и v наследует разные состояния типов по каждому пути, то состояние типа v в точке p считается наивысшей нижней границей наследуемых состояний типов. Например, в следующем фрагменте кода C переменная n наследует состояние типа « инициализировано » и « неинициализировано » от then и (пусто) else часть соответственно, следовательно, оно имеет состояние типа « неинициализировано после всего условного оператора ».
интервал п ; // здесь n имеет тип "неинициализированный" if (...) { n = 5 ; // здесь, n имеет состояние типа «инициализировано» } else { /*ничего не делать*/ // здесь, n имеет состояние типа «неинициализировано» } // здесь, n имеет состояние типа «неинициализировано» = Greatest_lower_bound("initialized","uninitialized" ) Каждая основная операция [примечание 1] должен быть оснащен переходом между состояниями типов , т.е. для каждого параметра требуемое и гарантированное состояние типа до и после операции соответственно. Например, операция fwrite(...,fd) требует fd чтобы иметь тип состояния « файл открыт ». Точнее, операция может иметь несколько исходов , для каждого из которых необходим свой переход в состояние типа. Например, код C FILE *fd=fopen("foo","r") наборы fdсостояние типа « файл открыт » и « нераспределен », если открытие выполнено успешно и не удалось соответственно.
Для каждых двух состояний типа t 1 <· t 2 должна быть обеспечена уникальная операция приведения к состоянию типа , которая, будучи применена к объекту с состоянием типа t 2 , уменьшает его состояние типа до t 1 , возможно, за счет освобождения некоторых ресурсов. Например, fclose(fd) принуждает fdсостояние типа от « файл открыт » до « инициализировано, но файл не открыт ».
Выполнение программы называется корректным по состоянию типа, если
- перед каждой базовой операцией все параметры имеют именно то состояние типа, которое требуется для перехода к состоянию типа операции, и
- при завершении программы все переменные находятся в состоянии типа ⊥. [примечание 2]
Текст программы называется согласованным по состоянию типа , если он может быть преобразован путем добавления соответствующих принуждений к состоянию типа в программу, точки которой могут быть статически помечены состояниями типа, так что любой путь, разрешенный потоком управления, является правильным с учетом состояния типа. Стром и Йемини предлагают алгоритм с линейным временем , который проверяет заданный текст программы на согласованность состояния типа и вычисляет, куда вставить какую операцию приведения, если таковая имеется.
Проблемы
[ редактировать ]Чтобы добиться точного и эффективного анализа состояния типов, необходимо решить проблему псевдонимов . Псевдоним возникает, когда объект имеет более одной ссылки или указателя, указывающего на него. Чтобы анализ был корректным, изменения состояния данного объекта должны отражаться во всех ссылках, указывающих на этот объект, но в целом отследить все такие ссылки представляет собой сложную задачу. Это становится особенно сложно, если анализ должен быть модульным, то есть применимым к каждой части большой программы отдельно, без учета остальной части программы.
Другая проблема заключается в том, что для некоторых программ метод взятия наибольшей нижней границы при сближении путей выполнения и добавления соответствующих операций приведения вниз оказывается неадекватным.Например, перед return 1 в следующей программе, [примечание 3] все компоненты x, y, и z из coord инициализируются, но подход Строма и Йемини не может это распознать, поскольку каждая инициализация компонента структуры в теле цикла должна быть приведена к понижению при повторном входе в цикл, чтобы соответствовать состоянию типа самой первой записи цикла, а именно. ⊥. Связанная с этим проблема заключается в том, что этот пример потребует перегрузки переходов между состояниями типов; например, parse_int_attr("x",&coord->x) меняет состояние типа « ни один компонент не инициализирован » на « компонент x инициализирован », а также « компонент y инициализирован » на « компоненты x и y инициализированы ».
int parse_coord ( struct { int x ; int y ; int z ; } * coord ) { int увиден = 0 ; /* запоминаем, какие атрибуты были проанализированы */ while ( 1 ) if ( parse_int_attr ( "x" , & coord -> x )) увидено |= 1 ; else if ( parse_int_attr ( "y" & ; coord > y )) увидено |= 2 - else if ( parse_int_attr ( "z" & ; coord > z )) увидено |= 4 - иначе сломаться ; if ( увидено != 7 ) /* какой-то атрибут отсутствует, ошибка */ return 0 ; ... /* все атрибуты присутствуют, делаем некоторые вычисления и добиваемся успеха */ return 1 ; } Вывод состояния типа
[ редактировать ]Существует несколько подходов, направленных на выведение состояний типов из программ (или даже из других артефактов, таких как контракты). Многие из них могут определять состояния типов во время компиляции. [6] [7] [8] [9] и другие динамически анализируют модели. [10] [11] [12] [13] [14] [15]
Языки, поддерживающие состояние типа
[ редактировать ]Typestate — это экспериментальная концепция, которая еще не перешла в основные языки программирования. Однако многие академические проекты активно исследуют, как сделать его более полезным в качестве метода повседневного программирования. Двумя примерами являются языки Plaid и Obsidian, которые разрабатываются группой Джонатана Олдрича в Университете Карнеги-Меллон . [16] [17] Другие примеры включают Клару [18] структура исследования языка, более ранние версии языка Rust и >> Ключевое слово в ATS . [19]
См. также
[ редактировать ]Примечания
[ редактировать ]- ^ к ним относятся языковые конструкции, например
+=в C и стандартные библиотечные процедуры, напримерfopen() - ^ Это направлено на то, чтобы, например, все файлы были закрыты, и все
mallocпамять Эда былаfreeд. В большинстве языков программирования время жизни переменной может закончиться до завершения программы; тогда понятие корректности состояния типа должно быть соответствующим образом уточнено. - ^ предполагая, что
int parse_int_attr(const char *name,int *val)инициализирует*valвсякий раз, когда это удается
Ссылки
[ редактировать ]- ^ Хорхе Луис Гевара Диас (2010). «Проектирование, ориентированное на состояние типов — подход с использованием цветной сети Петри» (PDF) .
- ^ Стром, Роберт Э. (1983). «Механизмы обеспечения безопасности во время компиляции». Материалы 10-го симпозиума ACM SIGACT-SIGPLAN по принципам языков программирования - POPL '83 . стр. 276–284. дои : 10.1145/567067.567093 . ISBN 0897910907 . S2CID 6630704 .
- ^ Стром, Роберт Э.; Йемини, Шаула (1986). «Typestate: концепция языка программирования для повышения надежности программного обеспечения» (PDF) . Транзакции IEEE по разработке программного обеспечения . 12 . ИИЭР: 157–171. дои : 10.1109/tse.1986.6312929 . S2CID 15575346 .
- ^ ДеЛайн, Роберт; Фендрих, Мануэль (2004). «Состояния типов для объектов» . ЭКООП 2004 – Объектно-ориентированное программирование . Конспекты лекций по информатике. Том. 3086. Спрингер. стр. 465–490. дои : 10.1007/978-3-540-24851-4_21 . ISBN 978-3-540-22159-3 .
- ^ Бирхофф, Кевин; Олдрич, Джонатан (2007). «Модульная проверка состояния типов объектов с псевдонимами». Материалы 22-й ежегодной конференции ACM SIGPLAN по системам, языкам и приложениям объектно-ориентированного программирования . Том. 42. С. 301–320. дои : 10.1145/1297027.1297050 . ISBN 9781595937865 . S2CID 9793770 .
- ^ Гвидо де Касо, Виктор Браберман, Диего Гарбервецки и Себастьян Учитель. 2013. Абстракции программ на основе возможностей для проверки поведения. АКМ Транс. Программное обеспечение англ. Методол. 22, 3, статья 25 (июль 2013 г.), 46 стр.
- ^ Р. Алур, П. Черни, П. Мадхусудан и В. Нам. Синтез спецификаций интерфейса для классов Java, 32-й симпозиум ACM по принципам языков программирования, 2005 г.
- ^ Джаннакопулу, Д., и Пасареану, К.С. , «Генерация интерфейса и композиционная проверка в JavaPathfinder», FASE 2009.
- ^ Томас А. Хенцингер, Ранджит Джала и Рупак Маджумдар. Разрешительные интерфейсы. Материалы 13-го ежегодного симпозиума по основам программной инженерии (FSE), ACM Press, 2005, стр. 31-40.
- ^ Валентин Даллмайер, Кристиан Линдиг, Анджей Васильковски и Андреас Целлер. 2006. Поведение объектов добычи полезных ископаемых с помощью ADABU. В материалах международного семинара по анализу динамических систем 2006 г. (WODA '06). ACM, Нью-Йорк, Нью-Йорк, США, 17–24
- ^ Карло Гецци, Андреа Моччи и Маттиа Монга. 2009. Синтез моделей интенсионального поведения путем преобразования графа. В материалах 31-й Международной конференции по программной инженерии (ICSE '09). Компьютерное общество IEEE, Вашингтон, округ Колумбия, США, 430–440.
- ^ Марк Габель и Чжендун Су. 2008. Символический анализ временных спецификаций. В материалах 30-й международной конференции по программной инженерии (ICSE '08). ACM, Нью-Йорк, Нью-Йорк, США, 51–60.
- ^ Давиде Лоренцоли, Леонардо Мариани и Мауро Пецце. 2008. Автоматическое создание поведенческих моделей программного обеспечения. В материалах 30-й международной конференции по программной инженерии (ICSE '08). ACM, Нью-Йорк, штат Нью-Йорк, США, 501-510.
- ^ Иван Бесчастных, Юрий Брун, Сигурд Шнайдер, Майкл Слоан и Майкл Д. Эрнст. 2011. Использование существующих инструментов для автоматического вывода моделей с инвариантными ограничениями. В материалах 19-го симпозиума ACM SIGSOFT и 13-й Европейской конференции по основам разработки программного обеспечения (ESEC/FSE '11). ACM, Нью-Йорк, Нью-Йорк, США, 267-277.
- ^ Прадель, М.; Гросс, Т.Р., «Автоматическое создание спецификаций использования объектов на основе трассировок больших методов», 2009. ASE '09. 24-я Международная конференция IEEE/ACM по автоматизированной разработке программного обеспечения, том, №, стр. 371,382, 16–20 ноября 2009 г.
- ^ Олдрич, Джонатан. «Язык программирования Plaid» . Проверено 22 июля 2012 г.
- ^ Кобленц, Майкл. «Язык программирования Obsidian» . Проверено 16 февраля 2018 г.
- ^ Бодден, Эрик. «Клара» . Проверено 23 июля 2012 г.
- ^ Си, Хунвэй. «Введение в программирование в АТС» . Проверено 20 апреля 2018 г.
| Ключевые понятия |  | ||||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| Семантика |
| ||||||||||||||
| Анализы |
| ||||||||||||||
| Формальные методы |
| ||||||||||||||
