конечные автоматы для верификации

[juan_gandhi]

Тут в разговоре про очередного, имхо, шарлатана, профессора Шалыто, выяснилось, что есть такая идея, будто для верификации программ достаточно FSM, конечного автомата.

Вот скажите мне, возьмём такой пример: даден алфавит, {a, b}, и две программы, одна генерирует все палиндромы в этом алфавите, вторая проверяет, что данная строка является палиндромом.

Скажите, какой конечный автомат может верифицировать эти программы?

Comments

[99f.livejournal.com]

Всякая программа на С имеет не более 2^{sizeof(void*)*CHAR_BIT} состояний (упражнение: обобщить последнее утверждение на случай программ работающих с файлами) и следовательно поведение всех программ в данной реализации стандарта может быть смоделировано и следовательно верифицировано неким конечным автоматом. Всякая программа на Java (ML, ...) может быть оттранслирована в программу на С, следовательно...

[ivan-gandhi.livejournal.com]

Вы и к стековой машине, к примеру, то же самое рассуждение примените?

[99f.livejournal.com]

Не понял что и как применить. Просто C как он описан в стандарте вопреки распространенному мнению не Turing complete. Программы на C можно верифицировать конечным автоматом. Можно разумеется и стековым. То же самое рассуждение применимо к более широкому классу языков.

Верификация программного обсепечения, неизвестная panchul, применяется военными и людьми занимающимися real-time. Есть периодическая конференция про это с proceedings на много сотен страниц. Spin и promela которые наверху упоминались вещи достаточно старые, они скорее про верификацию алгоритмов. Сейчас люди умеют верифицировать pointer arithmetics в многопоточных приложениях (Smallfoot, separation logic).

[ivan-gandhi.livejournal.com]

Я не то чтобы пошел сейчас читать стандарт, но скорее соглашусь, что стандарт он как бы описывает конечный автомат. Но поверх стандарта есть ещё io.

Так если я повторю вопрос, можно ли на си написать программу, которая проверяет паритет скобок в другой программе?

[99f.livejournal.com]

Тут стандарт читать не обязательно. Достаточно сообразить что всякий тип T в Си имеет только конечное количество значений не более 2^(sizeof(T)*8), динамически можно аллоцировать только конечное количество объектов (2^(sizeof(void *)*8)), и сами программы все конечной длины, как и всякие строки производимые грамматикой. I/O описано в стандарте и про него выше предлагалось упражнение (hint: длина каждого файла ограничена из-за ftell(3), а общее число всех файлов конечно т.к. конечно число строк которые могут быть их именами).

По поводу скобок. Если "другая программа" задается через char getnextsymbol() то в общем случае нельзя, т.к. вложенность скобок может превысить любое значение представимое в данной реализации Си.

[ivan-gandhi.livejournal.com]

А вот у меня есть решение.

[99f.livejournal.com]

Сработает если getnextsymbol() сначала выдает 2^{2^{sizeof(void*)*8}} + 1 открывающую скобку? (Такую getnextsymbol() на C конечно не написать.) Предъявите. :-)

[ivan-gandhi.livejournal.com]

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

Может быть, Вы тут излагаете что-нибудь вроде нестандартного анализа, кто Вас знает, а я лезу с чепухой вроде континуума.

Потому что есть много различных взглядов на как бы одну и ту же вещь.

[99f.livejournal.com]

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

Конечный автомат всегда либо останавливается за конечное число шагов либо повторяет уже бывшее состояние и тогда не остановится никогда. Отсюда легко понять, что для класса конечных автоматов с числом состояний менее данной константы можно сделать универсальный конечный автомат который их будет верифицировать. Верифицировать в том смысле что он будет говорить остановится ли данный конечный автомат и если да то в каком состоянии. Это был ответ на исходный вопрос можно ли программы верифицировать конечными автоматами: программы на C можно.

Далее возник обратный вопрос. Можно ли проверить программой на C т.е. конечным автоматом парность скобок. Ответ вроде бы очевиден - нет. "Вообразить" бесконечно большую виртуальную память нельзя в том смысле, что это будет не расширением языка "С", а противоречивой системой. В C все типы включая указатели имеют только конечное количество значений. На этом построен весь язык начиная от массивов.

[ivan-gandhi.livejournal.com]

"Можно считать что язык этот вычислительно эквивалентен некоторому классу конечных автоматов" - почему? Можно и не считать. Я не согласен, что с описывает конечные автоматы. Стековую машину на си написать - не фиг делать. Стек, разумеется, внешний.

[99f.livejournal.com]

Я же Вам говорю: у всякого типа лишь конечное количество возможным значений. Типов конечное число. Указателей лишь конечное число. Нельзя стековую машину написать на C. Если Вы фрагменты стека аллоцируете через malloc(3) то эта функция сможет успешно выделить память лишь конечное число раз, так как обязана каждый раз возвращать новое значение типа void *, а таких значений лишь конечное число. Поэтому глубина Вашего стека ограничена константой вроде 2^{sizeof(void*)*8} и Ваша "стековая машина" на самом деле конечный автомат. Это просто понять: общее число битов которое может видеть программа на C конечно и определяется шириной указателя. Значит и общее число состояний в которых может быть программа на С тоже конечно. Операции с файлами добавляют немного, но опять лишь конечное число состояний.

[ivan-gandhi.livejournal.com]

А нельзя ли к машине на си присобачить ленту, как у Тьюринга?

[ivan-gandhi.livejournal.com]

Можно стековую машину написать на си. Стек внешний. Мне кажется, Вы чего-то не понимаете.

[99f.livejournal.com]

Не понимаю точно. Слова "внешний" не понимаю видимо, а Вы не разъясняете. Если имеется в виду "на внешних носителях" то файлов конечное число и они все конечной длины. В файле можно двигаться по "относительным" смещениям (fseek(f, delta, SEEK_END)), но когда перелезете через sizeof(fpos_t) будет undefined behavior.

[ivan-gandhi.livejournal.com]

Откуда это что файлов конечное число? В каждый момент - да, но мы не спешим.

[99f.livejournal.com]

Number of values in addressable memory is finite. Filenames are strings is addressable memory. Therefore there is only a finite number of filenames. Therefore there is only a finite number of files that a program can ever open (whether it is in a hurry or not :-) ), because lacking chdir (which as was already mentioned elsewhere is not a part of the Standard) every file has a filename.

The ability to create and destroy files from the above finite set is of little interest: there still is a finite constant N such that no program can at any point of its execution store more than N bits of data in files. This, together with the finiteness of addressable storage, means that the program is a finite state machine.

[ivan-gandhi.livejournal.com]

A Turing machine is an FSM. With an unlimited tape. There's a difference, right, an FSM with a tape and the one without.

[99f.livejournal.com]

I take it that the issue of finiteness of a state that a C program can manipulate is no longer contested. As for the sudden claim that a Turning machine is an FSM I don't see how to reconcile it with your earlier statement "Я не согласен, что с описывает конечные автоматы". Can you elaborate?