AG
еще кстати есть вялотекущий чатик @FormalCompiler, там в истории можно найти литературу на сходные темы
Size: a a a
2020 February 28
AT
но есть проект по верификации раста на сепарационной логике: https://plv.mpi-sws.org/rustbelt/
Мне кажется, что больше практического выхлопа сейчас у https://www.pm.inf.ethz.ch/research/prusti.html
Но там тоже логика типа сепарационной.
Но там тоже логика типа сепарационной.
AT
Ребята, подскажите, пожалуйста, хорошие источники по формальной верификации компиляторов языков типа Rust и похожих по синтаксису и семантике.
Синтаксис нерелевантен. Для верификации императивных языков по сути и по факту используется логика Хоара и её расширения, сепарационная логика в частности и в особенности.
Для верификации компилятора используется всё то же самое, но слоями и с большим количеством сложностей и тонких моментов, связанных с особенностями реализации.
Для верификации компилятора используется всё то же самое, но слоями и с большим количеством сложностей и тонких моментов, связанных с особенностями реализации.
PS
О содержании современного курса построения компиляторов. Кое-где автор увлекается, на мой взгляд, но в целом много сказано по делу https://semantic-domain.blogspot.com/2020/02/thought-experiment-introductory.html
AT
О содержании современного курса построения компиляторов. Кое-где автор увлекается, на мой взгляд, но в целом много сказано по делу https://semantic-domain.blogspot.com/2020/02/thought-experiment-introductory.html
А в чём по-вашему автор увлекается?
PS
А в чём по-вашему автор увлекается?
Он пытается все стадии компилятора выразить с помощью алгоритмов вычисления неподвижной точки. Они, все-таки, не так уж специфичны именно для компиляторов и далеко не везде в компиляторах уместны.
AT
Он пытается все стадии компилятора выразить с помощью алгоритмов вычисления неподвижной точки. Они, все-таки, не так уж специфичны именно для компиляторов и далеко не везде в компиляторах уместны.
Мне показалось, что наоборот - подбирает только те стадии и алгоритмы, которые выразимы в виде LFP. Поскольку цель в том чтобы научить LFP. Как бы логично в этом свете. Удивительно насколько много в компиляторе можно выразить в таком виде.
AT
Я бы вообще по-приколу abstract interpret all the things! 😂
PS
Вот я и говорю, что подбор этот местами нарочитый. Для стадии лексического анализа, к примеру, есть очень красивый вариант детерминизации Бржозовского. Для вывода типов — системы непересекающихся множеств. И даже для анализа потоков данных в форме SSA можно обойтись без неподвижной точки.
AT
Вот я и говорю, что подбор этот местами нарочитый. Для стадии лексического анализа, к примеру, есть очень красивый вариант детерминизации Бржозовского. Для вывода типов — системы непересекающихся множеств. И даже для анализа потоков данных в форме SSA можно обойтись без неподвижной точки.
Мне кажется, Вы пропустили там второй или третий параграф, где автор объясняет цель предлагаемого курса. 😉
PS
Я просто отмечаю некоторую неестественность такого подхода. Курс ведь имеет конкретное название и это не "прикладные применения алгоритмов ..." :)
AT
Я просто отмечаю некоторую неестественность такого подхода. Курс ведь имеет конкретное название и это не "прикладные применения алгоритмов ..." :)
В некотором смысле, все вводные курсы (на бакалавриате) - это "прикладное применение алгоритмов", так что... 😊
H
Всем спасибо, буду изучать
KR
Какие есть книжки про сети конечных автоматов?
AT
Какие есть книжки про сети конечных автоматов?
WOW! А что это??? 😃
KR
WOW! А что это??? 😃
Это акторы, грубо говоря.
AT
Это акторы, грубо говоря.
Допустим. Но я никогда не слышал про такую математическую конструкцию как "сеть конечных автоматов". А Вы?
KR
Я просто начал разбираться с dataflow, что проще всего видеть как сети из «чистых элементов» и конечных автоматов.
KR
Допустим. Но я никогда не слышал про такую математическую конструкцию как "сеть конечных автоматов". А Вы?
Ну поправьте, если я неправильно перевёл network automata
KR