Несколько лет назад была одна на первый взгляд рядовая лекция в вузе, в котором я учился. Кторую я сначала по традиции забыл, но по истечению времени данный материал вспоминается со все большим интересом и сожалением что на практике не применяется.
Все мы знаем что программы - глючат :evil: . Неосторожное нажатие не той кнопки, неверное значение переменной, конфликт между процессами и просто внезапно возникшая ошибка памяти могут привести к самым плачевным последствиям и компьютер, и неуравновешенного пользователя :evil: . Конечно, существуют разные методы теста кода. Но большинство из них, например JUnit, сродни попыткам неандертальца разобраться в химическом составе камней, ударяя их друг о друга.
Проблема в том, что нельзя построить тесты, которые охватывали бы все реально возможные значения всех переменных. Это будет очень очень много тестов - (например 2 в степени количества переменных помноженных на число битов в одной переменной). Поэтому ограничиваются небольшим количеством "контрольных" тестов, с определенными входными значениями. В то время как обыкновенная ошибка переполнения ( что не учитывает этот тест) являлась дырой для взламывания серъезных систем.
Фундаментально решить проблему ( протестить все возможные комбинации, но хитро - без перебора) позволяет метод модель чекинга. Суть в том, что по абстрактной модели, которая включает в себя ход программы с описанием, какая переменная какой диапазон чисел может принимать, создается конечный автомат, просчитав который можно узнать где в программе потенциальные глюки и даже сгенерировать код без глюков.
Базовыми компонентами модели являются разные условия. Например, "х может принимать значения от 1 до 400". Временные условия , например "до/ после/ в то время как (условие 1) (не)должно выполняться (условие 2)". В реале они конечно сложнее и подробнее.
Небольшой инструмент, с которым можно посмотреть эту тему является NuSMV Model Checker. Можно погуглить, скачать и поиграться, если еще живой.
В перспективе можно сделать серъезные инструменты, которые будут создавать этот "контрольный автомат" автоматически из исходного кода или например указанных в исходнике аспектов, или вообще по бинарному коду.
И наконец последний вопрос. Почему на практике так не делают?
Мое мнение - [S]потому что дурни[/S] программинг- довольно концервативная вещь, где до сих пор сообщество используют обычный С с доисторическими грубыми макросами...
