Вопрос по решёткам — насколько я понимаю, для хорошего описания

Question

Вопрос по решёткам — насколько я понимаю, для хорошего описания

решёток нужен специальный DSL. Например, описание даже простейшей решётки на OCaml у меня получилось весьма многословным.

С другой стороны, описать направленный граф — вещь несложная. А как действовать с разными таблицами, описывающими конструкции анализируемого языка?

Это где-нибудь разобрано, как проектировать такие системы так, чтобы потом не было мучительно больно писать 2к строк чепухи? В Spoofax?

#compilerdev #it #programming #russian

0

10.06.2022

8 ответов

13 просмотров

Konstantin Romanov Автор вопроса

Сам спросил, сам нашёл - действительно FlowSpec в Spoofax’е содержит какие-то конструкции для решёток.

0

10.06.2022

Alexander Chichigin

Konstantin Romanov
Сам спросил, сам нашёл - действительно FlowSpec в ...

Ещё тут встроенные решётки есть, но довольно прямолинейные: https://doc.flix.dev/fixpoints/

0

11.06.2022

Konstantin Romanov Автор вопроса

Alexander Chichigin
Я что-то запутался: какая связь между решетками и ...

Решётки для data flow анализа, кмк, должны описываться на спец языке. А в Spoofax вводятся спец языки. Я, собственно и нашёл сам. Проблема в том, что я не нашёл хорошей документации к этой части Spoofax

0

11.06.2022

Alexander Chichigin

Konstantin Romanov
Решётки для data flow анализа, кмк, должны описыва...

Надо, наверное, статьи искать... 😅

0

11.06.2022

Konstantin Romanov Автор вопроса

Alexander Chichigin
Надо, наверное, статьи искать... 😅

Я пока просто на камле понафигачу для собственного удовольствия. А уже потом буду думать, как делать правильно. В применении к Камлу, люди пишут разные линтеры и анализаторы, но ничего уровня PVS. В то же время, кмк, подход monotone framework Moller’а позволяет писать хорошие анализаторы с разными проверками.

0

11.06.2022

Alexander Chichigin

OCaml можно из Coq экстрактить, если очень хочется -- это надёжнее, чем PVS. 😄

0

11.06.2022

Brenoritvrezorkre

Alexander Chichigin
OCaml можно из Coq экстрактить, если очень хочется...

я думаю, это нужно тогда, когда работаешь в ocaml окружении, в ином случае можно программировать напрямую в coq и компилировать через certicoq

0

11.06.2022