Хочется странного: найти ПО, которое по программе на 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++ всё-таки был бы предпочтительнее.
Собственно вопрос: подскажите инструмент/статьи на эту тему.
Comments (0)
