Цитата:
Что Вы подразумеваете под спецификациями?
Есть такая книжечка: "Простое и сложное в программировании". Там вопросу о верификации программ отводится определенное место и там спецификацией называют пару (предусловие, постусловие). Если на входе имеется ситуация, удовлетворяющая предусловию, на выходе обязана быть ситуация, удовлетворяющая постусловию. Ну, простенький пример:
{i - целое число}
???
{i увеличилось на единицу}
К сожалению, написать код, реализующий даже такую простую спецификацию, не так-то просто.
Да, помню эту старую добную книжку. То о чём Вы говорите, немного написано в начале первого тома Кнута (там есть ссылка на метод Флойда). В современном виде одна из подобных систем доказательства корректности алгоритмов -
логика Хоара. (Кстати посмотрел оригинал статьи Хоара, достаточно доступно написано, предшествующую оригинальную статью у Флойда я не осилил, надо будет почитать.)
Есть одна проблема в подобной системе верификации если рассматривать алгоритм содержащий не атомарные однозначные операции, а содержащие другие процедуры (как в моём случае процедуры веб-сервера, которые нигде не документированы, остаётся читать исходный код). В таком случае доказательство будет верным из
предположения о работе внешних процедур, но предположение может не совпадать с реальным положением дел.
Поэтому данный метод не очень подходит для не математических программ с вызовом внешних процедур.
Но инварианты цикла полезны всегда.
Поэтому вопрос о написании надежного ПО за разумные сроки остаётся открытым.
(Оффтоп)
vek88
Есть недостаток, надо его исправить, я ищу способ решить проблему. Я часто вижу тех (лично сталкиваюсь по работе), кто не замечает собственной некомпетентности. Они выглядят глупо и никогда не растут (проверил наблюдением за ними в течении минимум трёх лет).