Хочется странного: найти ПО, которое по программе на C++ и её формальной спецификации скажет, соответствует ли программа спецификации. Естественно должны проверяться все выходы за пределы массива, null-pointer-dereference, переполнение чисел и т.п.
Чудес не жду, так что готов помимо спецификации программы аннотировать также и каждую функцию программы, писать всякие pre-condition, post-condition, loop variant/loop invariant. Главное, чтобы я мог написать программу, доказать её корректность, и знать, что на каждом совместимом со стандартом C++ компиляторе программа будет работать в соответствии со спецификацией (и настанет рай на земле). В крайнем случае можно сузить круг компиляторов до g++.
Аннотированная программа должна нормально компилироваться компилятором C++, а также средство верификации должно поддерживать максимально большое подмножество C++, особенно желательно STL (тут я не знаю описано ли поведение STL в стандарте C++, но если описано, то пусть прувер считает что реализация STL будет соответствовать стандарту).
Из того что нашёл на данный момент:
1) http://compcert.inria.fr/ - тут, насколько я понял, цель проекта несколько другая - формально доказать корректность работы компилятора. Корректность же программ, написанных на нём не проверяется. Я правильно понял?
2) http://www.eschertech.com/products/ecv.php - это похоже на то, что мне надо
Предлагают писать вкусняшки типа такого:
void arrayCopy(const int* array src, int* array dst, size_t num) writes(dst.all) pre(src.lim >= num; dst.lim >= num) pre(disjoint(src.all, dst.all)) post(forall i in 0..(num - 1) :- dst[i] == src[i]) { const int* array const srcEnd = src + num; while(src != srcEnd) keep(src.base == old(src.base)) keep(0 <= src - (old src)) keep(src - (old src) <= n) keep(forall j in 0..((src - (old src)) - 1) :- (old dst)[j] == (old src)[j]) keep(dst == (old dst) + (src - (old src))) decrease(srcEnd - src) { *dst++ = *src++; } }
Выглядит круто, но не понятно, насколько поддерживается C++ (в особенности STL), и как собственно скачать инструмент.
В отличие от разработчиков ПО для самолётов, я не требую меганадёжности самого компилятора, хочется лишь доказывать корректность своего кода в соответствии с спецификацией моей программы и в предположении о соответствии компилятора спецификации C++, баги в компиляторе/STL пусть остаются на совести их авторов.
Ну и так как это всё лишь поиграться, то готов пощупать другой язык программрования, если для него есть такая штука, хотя C++ всё-таки был бы предпочтительнее.
Собственно вопрос: подскажите инструмент/статьи на эту тему.
Могу ещё добавить, что доказывается, кстати, не очень сложно хоть при помощи машин Тьюринга, хоть при помощи лямбда-исчисления Чёрча.
А ещё это всё неплохо так связано со знаменитой теоремой Гёделя о неполноте формальных систем.
Вообще это называется теорема Райса: для любого инвариантного свойства невозможно построить алгоритм, разрешающий это свойство у других алгоритмов.
Но мы же прекрасно понимаем, что, несмотря на теорию алгоритмов, резерч-индустрия верификаторов процветает. Девелоперам не нужен идеальный верификатор, девелоперы в большинстве своем не скармливают верификатору исходники верификатора :) Девелоперам нужен достаточно хороший инструмент для посведневных нужд и стандартных языков/библиотек, а это реально достижимо.
Так что топикстартер задал вполне четкий и корректный вопрос.
Не питайте иллюзий, здесь же в основном олимпиадники. Неудивительно, что вам первым комментарием же сказали про теоретическую невозможность такого :-)
А на хабре наверняка сказали бы, что к чему сейчас бывает в этой области.
Рекомендую: http://vcc.codeplex.com/
К сожалению, только для C, не C++. Но качественно.