Из Википедии, бесплатной энциклопедии
Перейти к навигации Перейти к поиску

Анализ состояния , иногда называемый анализом протокола , представляет собой форму анализа программ, применяемую в языках программирования . Чаще всего применяется к объектно-ориентированным языкам. Типовые состояния определяют допустимые последовательности операций, которые могут выполняться над экземпляром данного типа. Типовые состояния, как следует из названия, связывают информацию о состоянии с переменными этого типа. Эта информация о состоянии используется для определения во время компиляции, какие операции допустимы для вызова для экземпляра типа. Операции, выполняемые над объектом, которые обычно выполняются только во время выполнения, выполняются с информацией о состоянии типа, которая изменяется, чтобы быть совместимой с новым состоянием объекта.

Состояния типов могут представлять уточнения поведенческого типа, такие как «метод A должен быть вызван до вызова метода B , а метод C»не могут быть вызваны между ними ». Типовые состояния хорошо подходят для представления ресурсов, использующих семантику открытия / закрытия, путем принудительного применения семантически допустимых последовательностей, таких как« открыть, затем закрыть », в отличие от недопустимых последовательностей, таких как оставление файла в открытом состоянии. ресурсы включают элементы файловой системы, транзакции, соединения и протоколы. Например, разработчики могут указать, что файлы или сокеты должны быть открыты до того, как они будут прочитаны или записаны, и что они больше не могут быть прочитаны или записаны, если они были закрыты. название "typestate" происходит от того факта, что этот вид анализа часто моделирует каждый тип объекта как конечный автомат . В этом конечном автомате каждое состояние имеет четко определенный набор разрешенных методов / сообщений, и вызовы методов могут вызывать состояние переходы.Сети Петритакже были предложены в качестве возможной модели поведения для использования с типами уточнения . [1]

Анализ типов состояний был введен Робом Стромом в 1983 году [2] на языке сетевой реализации (NIL), разработанном в лаборатории IBM Watson Lab . Он был формализован Стромом и Йемини в статье [3] 1986 года, в которой описывалось, как использовать typestate для отслеживания степени инициализации переменных, гарантируя, что операции никогда не будут применяться к неправильно инициализированным данным, и далее обобщались на языке программирования Hermes .

В последние годы в различных исследованиях были разработаны способы применения концепции состояния типов к объектно-ориентированным языкам. [4] [5]

Подход [ править ]

Нелинейная решетка состояний типов, возникающая при инициализации переменной типа struct{int x;int y;int z;}.
Наименьший элемент ⊥ совпадает с состоянием ∅ отсутствия инициализированных компонентов структуры.

Стром и Йемини (1986) требовали, чтобы набор состояний типов для данного типа был частично упорядочен так , чтобы более низкое состояние типов могло быть получено из более высокого, отбрасывая некоторую информацию. Например, intпеременная в C обычно имеет свойства типов " неинициализированный " <" инициализированный ", а FILE*указатель может иметь состояния " нераспределенный " <" выделенный, но неинициализированный " <" инициализированный, но файл не открыт " <" файл открыт " . Более того, Стром и Йемини требуют, чтобы у каждых двух типовых состояний была точная нижняя граница, т. Е.что частичный порядок является даже встречной полурешеткой; и что в каждом заказе есть наименьший элемент, всегда называемый «⊥».

Их анализ основан на упрощении, заключающемся в том, что каждой переменной v присваивается только одно состояние типа для каждой точки в тексте программы; если точка p достигается двумя разными путями выполнения, и v наследует разные состояния типов через каждый путь, то состояние типов v в точке p берется как наибольшая нижняя граница унаследованных состояний типов. Например, в следующем фрагменте nкода C переменная наследует свойство typestate « инициализировано » и « неинициализировано » от thenи (пустой) elseчасти, соответственно, следовательно, после всего условного оператора она имеет свойство typestate « неинициализировано ».

int  n ;  // здесь n имеет состояние типа "неинициализировано" if  (...)  {  n  =  5 ;  // здесь n имеет typestate "initialized" }  else  {  / * ничего не делать * /  // здесь n имеет typestate "uninitialized" }  // здесь n имеет typestate "uninitialized" = great_lower_bound ("initialized", "uninitialized" )

Каждая базовая операция [примечание 1] должна быть оснащена переходом типа-состояния , т.е. для каждого параметра требуемое и гарантированное состояние-тип до и после операции, соответственно. Например, операция fwrite(...,fd)требует fdналичия типа « файл открыт ». Точнее, операция может иметь несколько результатов , каждый из которых требует своего собственного перехода типа-состояние. Например, код C FILE *fd=fopen("foo","r")устанавливает fdдля свойства typestate значение « файл открыт » и « нераспределен », если открытие было успешным и неудачным, соответственно.

Для каждых двух состояний типов t 1 <· t 2 должна быть предусмотрена уникальная операция приведения состояния типов, которая при применении к объекту состояния типов t 2 сокращает его состояние типов до t 1 , возможно, за счет освобождения некоторых ресурсов. Например, fclose(fd)принуждает fdtypestate «ы из„ открытого файла “в„ инициализируется, но файл не открывается “.

Выполнение программы называется корректным по типу, если

  • перед каждой базовой операцией все параметры имеют точно такое состояние типа, которое требуется для перехода операции с типом состояния, и
  • при завершении программы все переменные находятся в состоянии типа ⊥. [заметка 2]

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

Проблемы [ править ]

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

Еще одна проблема: для некоторых программ метод взятия максимальной нижней границы при сходящихся путях выполнения и добавления соответствующих операций с понижающим принуждением кажется неадекватным. Например, перед символом return 1в следующей программе [примечание 3] инициализируются все компоненты x, yи zof coord, но подход Строма и Йемини не учитывает этого, поскольку каждая инициализация компонента структуры в теле цикла должна быть понижена. при повторном входе в цикл, чтобы соответствовать типу самой первой записи цикла, а именно. ⊥. Связанная проблема состоит в том, что в этом примере потребуется перегрузка переходов типа-состояние; например, parse_int_attr("x",&coord->x)изменяет тип состояния " компонент не инициализирован " на " x компонент инициализирован"", но также и" компонент y инициализирован "значением" x и y компоненты инициализированы ".

int  parse_coord ( struct { int  x ; int  y ; int  z ;}  * координаты )  {  int  замечено  =  0 ;  / * запомнить, какие атрибуты были проанализированы * /  while  ( 1 )  if  ( parse_int_attr ( "x" , & Coord -> x ))  замечено  | =  1 ;  иначе,  если  ( parse_int_attr ( "y" , &координаты -> y ))  видно  | =  2 ;  иначе,  если  ( parse_int_attr ( "z" , & Coord -> z ))  замечено  | =  4 ;  иначе  сломаться ;  if  ( seen  ! =  7 )  / * какой-то атрибут отсутствует, ошибка * /  return  0 ;  ...  / * присутствуют все атрибуты, выполняем некоторые вычисления и успешно * /  return  1 ; }

Вывод типового состояния [ править ]

Существует несколько подходов, стремящихся вывести состояния типов из программ (или даже из других артефактов, таких как контракты). Многие из них могут выводить значения типов во время компиляции [6] [7] [8] [9], а другие анализируют модели динамически. [10] [11] [12] [13] [14] [15]

Языки, поддерживающие typestate [ править ]

Typestate - это экспериментальная концепция, которая еще не вошла в основные языки программирования. Тем не менее, многие академические проекты активно исследуют, как сделать его более полезным в качестве повседневного метода программирования. Двумя примерами являются языки Plaid и Obsidian, которые разрабатываются группой Джонатана Олдрича в Университете Карнеги-Меллона . [16] [17] Другие примеры включают языковую структуру исследования Clara [18] , более ранние версии языка Rust и >>ключевое слово в ATS . [19]

См. Также [ править ]

  • Дизайн по контракту
  • Система линейного типа
  • Система эффектов
  • Проверка во время выполнения

Заметки [ править ]

  1. ^ они включают языковые конструкции, например,+=в C, и стандартные библиотечные процедуры, напримерfopen()
  2. ^ Это нацелено на обеспечение того, чтобы, например, все файлы были закрыты, а всяmallocизмененная память былаfreeуничтожена. В большинстве языков программирования время жизни переменной может закончиться до завершения программы; понятие типосостояния должно быть соответствующим образом уточнено.
  3. ^ предполагая, чтоint parse_int_attr(const char *name,int *val)инициализируется*valвсякий раз, когда он успешен

Ссылки [ править ]

  1. ^ Хорхе Луис Guevara D'ıaz (2010). «Типичный дизайн - подход с использованием цветной сети Петри» (PDF) .
  2. ^ Стром, Роберт Э. (1983). «Механизмы обеспечения безопасности на этапе компиляции». Материалы 10-го симпозиума ACM SIGACT-SIGPLAN по принципам языков программирования - POPL '83 . С. 276–284. DOI : 10.1145 / 567067.567093 . ISBN 0897910907.
  3. ^ Стром, Роберт Э .; Йемини, Шаула (1986). «Typestate: концепция языка программирования для повышения надежности программного обеспечения» (PDF) . IEEE Transactions по разработке программного обеспечения . IEEE. 12 : 157–171. DOI : 10.1109 / tse.1986.6312929 .
  4. ^ Делайн, Роберт; Фендрих, Мануэль (2004). «Типовые усадьбы для объектов» . ECOOP 2004: Материалы 18-й Европейской конференции по объектно-ориентированному программированию . Конспект лекций по информатике. Springer. 3086 : 465–490. DOI : 10.1007 / 978-3-540-24851-4_21 . ISBN 978-3-540-22159-3.
  5. ^ Бирхофф, Кевин; Олдрич, Джонатан (2007). «Модульная проверка псевдослучайных объектов». OOPSLA '07: Материалы 22-й конференции ACM SIGPLAN по объектно-ориентированному программированию: системы, языки и приложения . 42 (10): 301–320. DOI : 10.1145 / 1297027.1297050 . ISBN 9781595937865.
  6. ^ Гвидо де Caso, Виктор Braberman, Диего Garbervetsky и Себастьян Учитель. 2013. Абстракции программ на основе возможностей для проверки поведения. ACM Trans. Софтв. Англ. Методол. 22, 3, статья 25 (июль 2013 г.), 46 стр.
  7. ^ Р. Алур, П. Черни, П. Мадхусудан и В. Нам. Синтез спецификаций интерфейса для классов Java, 32-й симпозиум ACM по принципам языков программирования, 2005 г.
  8. ^ Giannakopoulou, Д. и Pasareanu, CS, "Генерация интерфейса и композиционная Проверка в JavaPathfinder", ЕФАС 2009.
  9. ^ Томас А. Henzinger, Ранджит Jhala и Rupak Majumdar. Разрешающие интерфейсы. Материалы 13-го ежегодного симпозиума по основам программной инженерии (FSE), ACM Press, 2005, стр. 31-40.
  10. ^ Валентин Dallmeier, Кристиан Lindig, Анджей Wasylkowski и Андреас Zeller. 2006. Поведение объектов майнинга с ADABU. В материалах международного семинара 2006 г. по анализу динамических систем (WODA '06). ACM, Нью-Йорк, Нью-Йорк, США, 17-24
  11. ^ Карло Геззи, Андреа Моччи и Маттиа Монга. 2009. Синтез интенсиональных моделей поведения путем преобразования графов. В материалах 31-й Международной конференции по программной инженерии (ICSE '09). IEEE Computer Society, Вашингтон, округ Колумбия, США, 430-440
  12. ^ Марк Гэйбл и Чжендонг Су. 2008. Символьный анализ временных спецификаций. В материалах 30-й международной конференции по программной инженерии (ICSE '08). ACM, Нью-Йорк, Нью-Йорк, США, 51-60.
  13. ^ Davide Lorenzoli, Леонардо Mariani, и Mauro Pezze. 2008. Автоматическая генерация программных поведенческих моделей. В материалах 30-й международной конференции по программной инженерии (ICSE '08). ACM, Нью-Йорк, Нью-Йорк, США, 501-510
  14. ↑ Иван Бесчастных, Юрий Брун, Сигурд Шнайдер, Майкл Слоан и Майкл Д. Эрнст. 2011. Использование существующих инструментов для автоматического вывода моделей с инвариантными ограничениями. В материалах 19-го симпозиума ACM SIGSOFT и 13-й Европейской конференции по основам программной инженерии (ESEC / FSE '11). ACM, Нью-Йорк, Нью-Йорк, США, 267-277
  15. ^ Прадель, М .; Гросс, Т.Р., «Автоматическое создание спецификаций использования объектов из больших трассировок методов», Автоматизированная разработка программного обеспечения, 2009. ASE '09. 24-я Международная конференция IEEE / ACM, том, №, стр. 371 382, ​​16-20 ноября 2009 г.
  16. ^ Олдрич, Джонатан. «Язык программирования Plaid» . Проверено 22 июля 2012 года . CS1 maint: обескураженный параметр ( ссылка )
  17. ^ Кобленц, Майкл. «Обсидиановый язык программирования» . Проверено 16 февраля 2018 . CS1 maint: обескураженный параметр ( ссылка )
  18. ^ Бодден, Эрик. «Клара» . Проверено 23 июля 2012 года . CS1 maint: обескураженный параметр ( ссылка )
  19. ^ Си, Хунвэй. «Введение в программирование в АТС» . Проверено 20 апреля 2018 года . CS1 maint: обескураженный параметр ( ссылка )