Нужен ли мониторинг в период выполнения?
Нужен ли мониторинг в период выполнения?
Действительно, нужно ли проверять утверждения в период выполнения? После того, как мы были в состоянии, используя утверждения, дать теоретическое определение корректности класса: каждая процедура создания должна гарантировать инвариант, и тело каждой процедуры, запущенной в состоянии, удовлетворяющем инварианту и предусловию, сохраняет в заключительном состоянии инвариант и гарантирует выполнение постусловия. Теперь мы должны выполнить математическую проверку m+n соответствующих условий (для m процедур создания и n экспортируемых процедур), и тогда долой мониторинг в период выполнения.
Мы должны, но мы не можем. Доказательство правильности программ уже многие годы является активной областью исследований, и достигло определенных успехов. Все же сегодня невозможно проверить корректность реального ПО, написанного на современных языках программирования.
Для этого необходим, в частности, и более мощный язык утверждений. Язык IFL, обсуждаемый ниже, может быть использован как часть стратегии многоярусного доказательства.Даже, если со временем методы и инструментальные средства доказательства станут доступными, можно ожидать, что отказаться от мониторинга не удастся. В системе всегда останется место трудно предсказуемым событиям - ошибкам аппаратуры, ошибкам в самом доказательстве. Поэтому следует применять хорошо известную в инженерии технику - множественные, независимые способы проверки.
Более 800 000 книг и аудиокниг! 📚
Получи 2 месяца Литрес Подписки в подарок и наслаждайся неограниченным чтением
ПОЛУЧИТЬ ПОДАРОКЧитайте также
Период ученичества
Период ученичества Итак, как же молодые выпускники должны вливаться в ряды профессиональных программистов? Какой путь они должны пройти? С какими препятствиями столкнуться? Каких целей они должны достичь? Давайте рассмотрим профессиональные уровни программистов по
Мониторинг
Мониторинг Начиная с версии 1120.5 NeTAMS поддерживает мониторинг заданных юнитов для сбора информации по относящемуся к ним трафику. Для включения этой функции необходимо задать сервис monitor и направление вывода статистики. Она может сохраняться как в текстовом файле, так и в
Мониторинг блогосферы
Мониторинг блогосферы Маркетинговые исследования в режиме наблюдения Метки: аудитория, внимание, репутация, мониторингВ последние несколько лет многие бренды теряют контроль над мнениями своих покупателей, а продавцы-консультанты из поставщиков информации
15.17.6 Мониторинг NFS
15.17.6 Мониторинг NFS Команда nfsstat из Unix выводит сведения о действиях NFS. Подобные команды доступны и в других операционных системах. В представленном ниже примере локальная система работает и как сервер, и как клиент. Ее деятельность в качестве сервера почти незаметна.
5.5. Мониторинг реестра
5.5. Мониторинг реестра Registry Monitor Статус: Freeware.Размер: 271 Кбайт.Разработчик: http://technet.microsoft.com/ru-ru/sysinternals/bb896652(en-us).aspx.Программа не предназначена для внесения в реестр каких-либо изменений. Тем не менее целесообразность ее использования не вызывает сомнений, поскольку она
Мониторинг работы компьютера
Мониторинг работы компьютера Программы, предназначенные для мониторинга, можно разделить на две группы: утилиты, отслеживающие работу операционной системы и пользователей, и программы, наблюдающие за работой аппаратной части компьютера.How Much Computer
Выяснение типа объекта в период выполнения
Выяснение типа объекта в период выполнения Разработчики ОО-ПО вскоре вырабатывают здоровую неприязнь к любому стилю вычислений, основанному на явном выборе между различными типами объекта. Полиморфизм и динамическое связывание намного предпочтительнее. Однако в
Мониторинг утверждений в период выполнения
Мониторинг утверждений в период выполнения Пришло время, дать полный ответ на вопрос: "какой эффект производят утверждения в период выполнения?". Как отмечалось, ответ определяется разработчиком, имеющим возможность управлять параметрами компиляции. Выбор нужных
Почему России не нужен собственный высокоточный спутниковый мониторинг? Сергей Сорокин, директор омской компании «Индустриальные геодезические системы»
Почему России не нужен собственный высокоточный спутниковый мониторинг? Сергей Сорокин, директор омской компании «Индустриальные геодезические системы» Опубликовано 06 марта 2013Наш стартап занимается разработкой решений, позволяющих определять координаты объектов в
Кафедра Ваннаха: Период 4К Михаил Ваннах
Кафедра Ваннаха: Период 4К Михаил Ваннах Опубликовано 21 сентября 2012 года Эры, за исключением архея, названы по давности жизни, следы которой в них обнаруживаются. Протерозой с рачками и радиоляриями, палеозой, начинающийся с трилобитов... Периоды
Универсальные ЭВМ, разработанные под руководством С. А. Лебедева в московский период
Универсальные ЭВМ, разработанные под руководством С. А. Лебедева в московский период БЭСМТехнические характеристики: быстродействие — 8–10 тыс. операций в секунду, представление чисел с плавающей запятой, разрядность 39, система ламповых элементов, внешняя память на