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

[juan_gandhi]

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

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

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

Comments

[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?