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

[juan_gandhi]

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

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

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

Comments

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