Основы объектно-ориентированного программирования
Нужен ли мониторинг в период выполнения?
Действительно, нужно ли проверять утверждения в период выполнения? После того, как мы были в состоянии, используя утверждения, дать теоретическое определение корректности класса: каждая процедура создания должна гарантировать инвариант, и тело каждой процедуры, запущенной в состоянии, удовлетворяющем инварианту и предусловию, сохраняет в заключительном состоянии инвариант и гарантирует выполнение постусловия. Теперь мы должны выполнить математическую проверку m+n соответствующих условий (для m процедур создания и n экспортируемых процедур), и тогда долой мониторинг в период выполнения.
Мы должны, но мы не можем. Доказательство правильности программ уже многие годы является активной областью исследований, и достигло определенных успехов. Все же сегодня невозможно проверить корректность реального ПО, написанного на современных языках программирования.
| Для этого необходим, в частности, и более мощный язык утверждений. Язык IFL, обсуждаемый ниже, может быть использован как часть стратегии многоярусного доказательства. |
Даже, если со временем методы и инструментальные средства доказательства станут доступными, можно ожидать, что отказаться от мониторинга не удастся. В системе всегда останется место трудно предсказуемым событиям - ошибкам аппаратуры, ошибкам в самом доказательстве. Поэтому следует применять хорошо известную в инженерии технику - множественные, независимые способы проверки.
