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

[juan_gandhi]

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

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

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

Comments

[huzhepidarasa.livejournal.com]

Да вот непонятно. С одной стороны вроде нельзя, надо хотя бы уметь имена переменных запоминать и потом сравнивать. С другой стороны, это тривиальная надстройка над конечным автоматом. Может, можно препроцессинг какой запустить и избавиться от таких переменных, а потом уже верифицировать. Содержательная часть — это доказательство некоторого утверждения о программе. Доказательства каких-то тривиальных утверждений можно породить конечным автоматом. Может быть, можно придумать язык, на котором легко писать так, чтобы большинство интересных нам утверждений были в нужном смысле тривиальными (типа «определение записано правильно»). Я не знаю.

[ivan-gandhi.livejournal.com]

Язык вроде Агды?

[huzhepidarasa.livejournal.com]

Я тут посмотрел комменты и понял, что очень мало об этом понимаю. Наверное, классическим FSM это делать если и можно, то слишком сложно и непонятно зачем. Но утверждать наверняка не берусь.

[cadadr.livejournal.com]

Я знаю больше Coq, его язык можно считать чем-то подходящим.

Всё опирается как раз на логику и типы,
это не бином Ньютона конечные автоматы.

http://adam.chlipala.net/cpdt/