Соответствующая логика

Логика сопоставления — это формальная логика, которая в основном используется для рассуждений о правильности компьютерных программ. Его операторы используют сопоставление с образцом для работы с набором состояний, а не с набором состояний. Он был создан Григоре Рошу и используется в K Framework.

Обзор

Логика сопоставления работает с шаблонами. ^[1] Операторы оценивают набор значений, которые им «соответствуют», а не истинное или ложное.

Учитывая набор подписей $\Sigma$ , шаблон может быть:

Переменная: $x\in Var$
Структура после подписи $\sigma \in \Sigma$ используя другие шаблоны: $\sigma (p_{1},p_{2},...,p_{n})$
Дополнение : другого шаблона $\neg p$
Пересечение двух паттернов: $p_{1}\land p_{2}$
Привязка: $\exists x.p$ с $x\in Var$

Соответствующая логика также может иметь набор $S$ своего рода . В этом случае каждый шаблон принадлежит определенному виду. Структуры можно использовать для объединения шаблонов разных типов. Некоторыми примерами типов, используемых при работе с семантикой программы, могут быть «32-битные целочисленные значения», «фреймы стека» или «кучная память».

Некоторые производные понятия определяются как:

$\top \equiv \exists x.x$
$\bot \equiv \neg \top$
$p_{1}\lor p_{2}\equiv \neg (\neg p_{1}\land \neg p_{2})$
$p_{1}\implies p_{2}\equiv \neg p_{1}\lor p_{2}$
$p_{1}\Leftrightarrow p_{2}\equiv p_{1}\implies p_{2}\land p_{2}\implies p_{1}$
$\forall x.p\equiv \neg (\exists x.\neg p)$

$\top$ совпадает со всеми элементами. $\bot$ не соответствует ни одному.

«Следует быть осторожным, рассуждая с помощью такой неклассической логики, поскольку базовая интуиция может обмануть». ^[1]

При интерпретации логики сопоставления (то есть при определении ее семантического значения) шаблон моделируется с помощью набора мощности. Интерпретация оператора — это набор значений, соответствующих шаблону.

Соответствие μ-логике

Соответствие $\mu$ -logic добавляет оператор с фиксированной точкой $\mu$ . ^[2]

Приложения

Логика сопоставления используется с логикой достижимости. ^[3] с помощью K Framework для определения операционной семантики и на основе нее создания логики Хоара .

Логику сопоставления можно преобразовать в логику первого порядка с равенством, что позволяет K Framework использовать существующие SMT -решатели для поиска доказательств теорем.

См. также

Логика разделения
логика Хоара
Регулярное выражение , которое соответствует наборам строк.

Ссылки

^ Jump up to: ^а ^б Рошу, Григоре (2017). «Логическое сопоставление» (PDF) . Логические методы в информатике .
^ Чен, Сяохун; Рошу, Григоре (19 января 2019 г.). «Соответствие μ-логике» . Отчеты об исследованиях и технологиях Университета Иллинойса (компьютерные науки).
^ Красный, Григоре; Штефанеску, Андрей; Чобака, Стефан; Мур, Брэндон М. (2012). «Логика достижимости» (PDF) . Технический отчет Университета Иллинойса .

[original-1] Jump up to: ^а ^б Рошу, Григоре (2017). «Логическое сопоставление» (PDF) . Логические методы в информатике .

[2] Чен, Сяохун; Рошу, Григоре (19 января 2019 г.). «Соответствие μ-логике» . Отчеты об исследованиях и технологиях Университета Иллинойса (компьютерные науки).

[3] Красный, Григоре; Штефанеску, Андрей; Чобака, Стефан; Мур, Брэндон М. (2012). «Логика достижимости» (PDF) . Технический отчет Университета Иллинойса .

[1]

[2]

[3]