Верификатор языка Урбана Мюллера

[Александр Коновалов]

Добрый вечер всем!

Тут подумалась интересная учебная задача: написать статический анализатор, верифицирующий программы на языке Урбана Мюллера. На самом деле этот язык называется иначе, но из соображений благозвучия я буду называть его по имени автора.

Это минималистичный полный по Тьюрингу язык (алгоритмическая полнота доказана). Синтаксис определяется следующей грамматикой:

PROGRAM = CODE
CODE = "+" | "−" | "<" | ">" | "." | "," | CODE CODE | "[" CODE "]"

Семантика описывается в терминах машины, похожей на машину Тьюринга. Есть полубесконечная лента, в ячейках которой находятся байты, т.е. целые числа от 0 до 255. По ней ползает головка. Операции языка:

• "+" и "−" инкрементируют и декрементируют текущую ячейку,
• "<" и ">" сдвигают головку влево и вправо соответственно,
• "." отправляет байт в текущей ячейке на устройство вывода,
• "," считывает байт с устройства ввода и записывает в текущую ячейку,
• CODE1 CODE2 означает конкатенацию двух программ, сначала выполнить CODE1, потом CODE2,
• "[" CODE "]" — повторять CODE до тех пор, пока в текущей ячейке не ноль.

Изначально головка находится в крайне левой позиции, все ячейки ленты заполнены нулями.

Задача верификатора определить, не происходит ли арифметического переполнения (декремента нуля или инкремента 255) и выхода за границы ленты.

 

Если я достаточно разберусь в верификации программ, предложу эту задачу на курсовую работу по компиляторам на следующий код. Или на диплом.

Интересно, на Агде можно написать DSL с типами, описывающий только корректные программы на языке Урбана Мюллера?

 

С уважением,
Александр Коновалов

 

[Andrei Klimov]

On Tue, Mar 16, 2021 at 10:09 PM 'Александр Коновалов' via Метавычисления и специализация программ <metacompu...@googlegroups.com> wrote:

Добрый вечер всем!

Тут подумалась интересная учебная задача: написать статический анализатор, верифицирующий программы на языке Урбана Мюллера. На самом деле этот язык называется иначе, но из соображений благозвучия я буду называть его по имени автора.

Это минималистичный полный по Тьюрингу язык (алгоритмическая полнота доказана). Синтаксис определяется следующей грамматикой:

PROGRAM = CODE
CODE = "+" | "−" | "<" | ">" | "." | "," | CODE CODE | "[" CODE "]"

Семантика описывается в терминах машины, похожей на машину Тьюринга. Есть полубесконечная лента, в ячейках которой находятся байты, т.е. целые числа от 0 до 255. По ней ползает головка. Операции языка:

• "+" и "−" инкрементируют и декрементируют текущую ячейку,
• "<" и ">" сдвигают головку влево и вправо соответственно,
• "." отправляет байт в текущей ячейке на устройство вывода,
• "," считывает байт с устройства ввода и записывает в текущую ячейку,
• CODE1 CODE2 означает конкатенацию двух программ, сначала выполнить CODE1, потом CODE2,
• "[" CODE "]" — повторять CODE до тех пор, пока в текущей ячейке не ноль.

Изначально головка находится в крайне левой позиции, все ячейки ленты заполнены нулями.

Задача верификатора определить, не происходит ли арифметического переполнения (декремента нуля или инкремента 255) и выхода за границы ленты.

Под словом "верификатор" вы имеете в виду разрешающую процедуру? То есть автоматическое построение доказательства или опровержения? Поскольку это, как вы пишете, полный по Тьюрингу язык, такой универсальной процедуры не существует. Значит, или вы должны сформулировать некоторые подклассы программ, или дать коллекцию примеров и попросить доказать для них требуемое свойство, пользуясь выбранным proof assistant'ом. То есть доказательство (или опровержение) составит человек, а машина проверит, что он не проврался.

Если я достаточно разберусь в верификации программ, предложу эту задачу на курсовую работу по компиляторам на следующий код. Или на диплом.

Бедный студент! Пожалейте!

– Г‑голубчики, – сказал Федор Симеонович озадаченно, разобравшись в почерках. – Это же п‑про‑блема Бен Б‑бецалеля. К‑калиостро же доказал, что она н‑не имеет р‑решения.
– Мы сами знаем, что она не имеет решения, – сказал Хунта, немедленно ощетиниваясь. – Мы хотим знать, как ее решать.
– К‑как‑то ты странно рассуждаешь, К‑кристо… К‑как же искать решение, к‑когда его нет? Б‑бес‑смыслица какая‑то…
– Извини, Теодор, но это ты очень странно рассуждаешь. Бессмыслица – искать решение, если оно и так есть. Речь идет о том, как поступать с задачей, которая решения не имеет. Это глубоко принципиальный вопрос, который, как я вижу, тебе, прикладнику, к сожалению, не доступен.

 

Интересно, на Агде можно написать DSL с типами, описывающий только корректные программы на языке Урбана Мюллера? 

Можно написать интерпретатор. Можно выписать тип, соответствующий приведенному вами утверждению. Но запрограммировать функцию для конкретной программы на DSL, удовлетворяющую этому типу, то есть фактически доказательство этого утверждения, – это будет задача человека (студента😆).

Всего наилучшего,

Андрей Климов

 

С уважением,
Александр Коновалов

[Александр Коновалов]

Добрый вечер!

Понятно, что задача неразрешимая. Но для любой неразрешимой задачи, требующей ответа «да/нет», можно дать приближённое решение «да/нет/не знаю». И чем меньше область этого «не знаю», тем решение точнее.

«Бедный студент! Пожалейте!»

Да, сам понял это спустя некоторое время после отправки письма.

Но автоматически распознавать какие-нибудь простые классы заведомо корректных и заведомо некорректных программ уже интересно. Например, если можно доказать, что с каждым символом программы ассоциирована конкретная ячейка ленты (т.е. всегда, когда выполняется i-я команда, головка находится над j-й ячейкой), то программа удовлетворяет двум свойствам: (а) она использует конечную память, (б) головка не выходит за пределы ленты. Думаю, распознавать такие программы можно абстрактной интерпретацией (не все, конечно, т.к. все невозможно) и такое под силу студенту.

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

 

Кстати, трансляция языка Урбана Мюллера в язык Си задаётся следующей процедурой. Напомню грамматику:

PROGRAM = CODE
CODE = "+" | "−" | "<" | ">" | "." | "," | CODE CODE | "[" CODE "]"

Сама процедура описывается функцией C(…):

C(PROGRAM) ::=
  int main() {
    char tape[MAX] = { '\0' };
    char *head = &tape[0];

    C(CODE)

    return 0;
  }

C("+") ::= ++*head;
C("−") ::= −−*head;
C("<") ::= −−head;
C(">") ::= ++head;
C(".") ::= putchar(*head);
C(",") ::= *head = getchar();
C(CODE1 CODE2) ::= C(CODE1) C(CODE2)
C("[" CODE "]") ::= while (*head) { C(CODE) }

Есть и другая задача, проще. Взять готовый верификатор языка Си (или модел-чекер, я пока в них не разобрался), скормить ему оттранслированную программу с языка У. М. и посмотреть на результат.

 

С уважением,
Александр Коновалов

--
Вы получили это сообщение, поскольку подписаны на группу "Метавычисления и специализация программ".
Чтобы отменить подписку на эту группу и больше не получать от нее сообщения, отправьте письмо на электронный адрес metacomputation...@googlegroups.com.
Чтобы посмотреть обсуждение на веб-странице, перейдите по ссылке https://groups.google.com/d/msgid/metacomputation-ru/CAM7HiMmbKOR%2Bv-UjW5kgKbS%2BeT4pE51ywLu0s5R7AoCYR-BFYQ%40mail.gmail.com.

[Andrei Klimov]

On Sat, Mar 20, 2021 at 9:32 PM 'Александр Коновалов' via Метавычисления и специализация программ <metacompu...@googlegroups.com> wrote:

Есть и другая задача, проще. Взять готовый верификатор языка Си (или модел-чекер, я пока в них не разобрался), скормить ему оттранслированную программу с языка У. М. и посмотреть на результат.

Александр, просто "скормить и посмотреть" не получится. Человек еще должен выписать спецификацию, условие, которое надо проверить, proof obligation на входном языке данного верификатора. А потом еще, как правило, "помочь" верификатору доказать его. Если программа небольшая, а условие нетривиальное, то proof obligation может быть заметно больше проверяемой программы.

Когда вы говорите о разрешимых подклассах неразрешимой проблемы, это значит, что описание подклассов должно быть формализовано в proof obligations. Выделить и формально описать интересные разрешимые подклассы – само по себе может быть весьма нетривиально.

Всего наилучшего,

Андрей Климов

 

[Александр Коновалов]

Добрый день, Андрей!

Спасибо за ответ. Тему верификации программ мне ещё изучать и изучать.

Смотрю на свои границы незнания и аж страшно становится: верификация программ, частичные вычисления, логика, теория категорий…

 

С уважением,
Александр Коновалов

 

 

From: metacompu...@googlegroups.com <metacompu...@googlegroups.com> On Behalf Of Andrei Klimov
Sent: Saturday, March 20, 2021 10:42 PM
To: metacomputation-ru <metacompu...@googlegroups.com>
Subject: Re: Верификатор языка Урбана Мюллера

 

On Sat, Mar 20, 2021 at 9:32 PM 'Александр Коновалов' via Метавычисления и специализация программ <metacompu...@googlegroups.com> wrote:

--

Вы получили это сообщение, поскольку подписаны на группу "Метавычисления и специализация программ".
Чтобы отменить подписку на эту группу и больше не получать от нее сообщения, отправьте письмо на электронный адрес metacomputation...@googlegroups.com.

Чтобы посмотреть обсуждение на веб-странице, перейдите по ссылке https://groups.google.com/d/msgid/metacomputation-ru/CAM7HiM%3DWXCfqLPjv5VnBAKhx7n6sXVD7HHaQp%2BVhbw9LKG91sg%40mail.gmail.com.

[Александр Коновалов]

Прошу прощения за спам. В предыдущем письме забыл спросить.

А с чего мне лучше изучать тему верификации программ? Есть ли какие-нибудь хорошие учебники или обзорные книги на эту тему?

 

С уважением,
Александр Коновалов

Чтобы посмотреть обсуждение на веб-странице, перейдите по ссылке https://groups.google.com/d/msgid/metacomputation-ru/019201d71fee%245fcb8590%241f6290b0%24%40mail.ru.

[Andrei Klimov]

On Tue, Mar 23, 2021 at 5:11 PM 'Александр Коновалов' via Метавычисления и специализация программ <metacompu...@googlegroups.com> wrote:

Добрый день, Андрей!

Спасибо за ответ. Тему верификации программ мне ещё изучать и изучать.

Смотрю на свои границы незнания и аж страшно становится: верификация программ, частичные вычисления, логика, теория категорий…

...еще бы я посоветовал отслеживать линию статической типизации: от simply typed lambda calculus к параметрической типизации Хиндли-Милнера (языки семейства ML и Haskell), затем к ее "притирке" к "суровой практике" параметрической типизации объектно-ориентированных языков типа Java, C#, и далее к вершинам типизации – dependent types (Coq, Agda, Idris), которая лет через 10 войдет в массовые языки и системы разработки надежного, доказуемо-корректного софта. По всей линии типизации в ее "чистых" образцах (намекаю, что в Java "нечисто") надо освоить соответстветствие Карри-Ховарда между типами и математическими утверждениями, и между программами, удовлетворяющими типам, и доказательствами соответствующих утверждений.

Нашему поколению в молодости было легче: мы осваивали новинки по ходу дела, как появлялись изобретения, или с небольшой задержкой, когда на них возникала мода: функциональное программирование на Рефале параллельно с Лиспом в 1960-е и начале 70-х; идеи объектно-ориентированного программирование из Симулы-67, когда слова ООП еще не было, и в 70-80-е, когда начался OO-buzz и появился Smalltalk, С++ и потом Java в 90е; параметрическую типизацию в начале 90-х, когда отрабатывались ныне распространенные функциональные языки от SML до Haskell; а в этом тысячелетии выход dependent types из теории в практику. То же самое с параллельным программированием, первая мода на которое возникла в 70-е, когда массово заговорил о фон-неймановском узком горе и пошла наработка разных моделей пар-вычислений в прошлом тысячелетии и их взрыв в нынешнем на потребу практике. Наша молодость пришлась на время молодости отрасли с соответствующей атмосферой горения первооткрывателей (отличия между тогда и сейчас чувствуются). А когда отрасль заматерела, вашему поколению надо впитать высшие достижения за короткое время. Но у вас есть преимущество: вы имеете дело с исторически отобранными отшлифованными образцами, а через нас проходил и "мусор", ушедший на свалку истории. Правда, там были и бриллианты (например Рефал), и не факт, что человейник отобрал наилучшие. Конечно, есть и старые идеи, которые "пылятся", не войдя в жизнь, а потом вдруг вырвутся в массовое сознание. Например, те же dependent types, долго "отлеживавщиеся" у теоретиков ("крот истории роет медленно").

Но теперь нашему поколению становится труднее: волна новинок нарастает с ускорением, а наши мозги уже не столь гибкие и легко схватывающие. А ваши молодые, в конце концов, всё впитают и будут толкать историю дальше.

Успехов!

Всего наилучшего,

Андрей

[Andrei Klimov]

On Tue, Mar 23, 2021 at 5:13 PM 'Александр Коновалов' via Метавычисления и специализация программ <metacompu...@googlegroups.com> wrote:

Прошу прощения за спам. В предыдущем письме забыл спросить.

А с чего мне лучше изучать тему верификации программ? Есть ли какие-нибудь хорошие учебники или обзорные книги на эту тему?

Я еще не натыкался на сводный учебник, в которым разные подходы были собраны вместе, разбирались в отдельных главах, а потом сопоставлялись. Но наверно, такие есть. Правда, есть подозрение, что авторы курсов и учебников, как правило, имеют дело с любимыми подходам и ленятся осваивать другие, не говоря уж о том, чтобы сводить в одну монографию, да еще сопоставлять. В жизни, на конференциях я иногда наблюдаю такие холивары. В общем, погуглите, а также посмотрите, какие ссылки приводят в википедии. Я сам осваиваю по отдельным областям в процессе того, как возникает личная потребность в чем-то разобраться. Может, кто-то еще из этой гугл-группы посоветует?

Всего наилучшего,

Андрей Климов

[Александр Коновалов]

Добрый день, Андрей!

«ещё бы я посоветовал отслеживать линию статической типизации»

С этой темой я более-менее знаком, не знаю только зависимые типы. Кстати, вывод параметрических типов Хиндли-Милнера входит и в промышленные языки, например модный на сегодня Rust основан на нём.

Про соответствие Карри-Ховарда мне нужно будет почитать лекции Антонины. Так до них ещё и не добрался.

 

Спасибо!
Александр Коновалов

 

From: metacompu...@googlegroups.com <metacompu...@googlegroups.com> On Behalf Of Andrei Klimov
Sent: Tuesday, March 23, 2021 11:06 PM
To: metacomputation-ru <metacompu...@googlegroups.com>
Subject: Re: Верификатор языка Урбана Мюллера

 

On Tue, Mar 23, 2021 at 5:11 PM 'Александр Коновалов' via Метавычисления и специализация программ <metacompu...@googlegroups.com> wrote:

--

Вы получили это сообщение, поскольку подписаны на группу "Метавычисления и специализация программ".
Чтобы отменить подписку на эту группу и больше не получать от нее сообщения, отправьте письмо на электронный адрес metacomputation...@googlegroups.com.

Чтобы посмотреть обсуждение на веб-странице, перейдите по ссылке https://groups.google.com/d/msgid/metacomputation-ru/CAM7HiMkE3sLB7b1tV_wNtL3hOkOm03YmwZf5OFP_RfOFY85c5Q%40mail.gmail.com.