Язык верификации часто используется после написания кода при его мысленном прогоне. Нарушения утверждений во время тестирования помогают обнаружить ошибки, а анализ этих нарушений позволяет избавиться от ошибок, не наплодив новых. Во время отладки следует исправлять и код, и неправильные утверждения. Нужно понимать свою программу в каждый момент времени и не поддаваться искушению «менять что-нибудь, пока она не заработает». В следующей главе иллюстрируется роль утверждений при тестировании и отладке. Утверждения жизненно важны в процессе сопровождения программы: если вы пытаетесь разобраться в программе, которую никогда раньше не видели и которую никто другой тоже не видел уже много лет, утверждения о состоянии программы могут дать вам неоценимую информацию.
Эти методы — лишь малая часть того, что нужно знать, чтобы правильно писать программы. Ключом к правильности часто является простота кода. С другой стороны, несколько профессиональных программистов, знакомых с этими методиками, поделились со мной опытом, который был не чужд и мне самому: при написании программы «сложная» ее часть обычно работает с первого раза, тогда как ошибки обычно содержатся в простых частях. Когда вы сталкиваетесь с чем-то сложным, вы сосредоточиваетесь и используете мощные формальные методы. В легких местах вы возвращаетесь к старым методам программирования п получаете характерные для этих методов результаты. Я бы сам в это не поверил, если бы это не случилось со мной. Подобные вещи являются хорошей причиной для более частого использования правильных методов.
Опубликовал vovan666
April 16 2013 23:58:17 ·
0 Комментариев ·
4409 Прочтений ·
• Не нашли ответ на свой вопрос? Тогда задайте вопрос в комментариях или на форуме! •
Комментарии
Нет комментариев.
Добавить комментарий
Рейтинги
Рейтинг доступен только для пользователей.
Пожалуйста, залогиньтесь или зарегистрируйтесь для голосования.
Нет данных для оценки.
Гость
Вы не зарегистрированны? Нажмите здесь для регистрации.