1. Зачем нужно доказывать правильность программ?
Доказывать правильность программ необходимо для того, чтобы гарантировать их корректную работу в любых условиях. Это позволяет избежать ошибок, которые могут привести к сбоям, утечке данных или другим серьезным последствиям. Правильность программы также подтверждает, что она выполняет поставленную задачу в соответствии с заданными требованиями и не приводит к неожиданным результатам.
2. Почему с помощью тестирования сложно доказать правильность программы? В каких случаях это всё же можно сделать?
Тестирование сложно доказать правильность программы, потому что оно не охватывает все возможные сценарии и ситуации. Тесты обычно проверяют программу на конечном наборе входных данных, что не гарантирует отсутствие ошибок в других случаях. Также возможны проблемы, связанные с пограничными случаями или сложными сочетаниями данных. Однако в случае, если программа является детерминированной и тестируемая на полном множестве входных данных, можно утверждать, что она правильна в рамках этих условий.
3. Что изменится в доказательстве алгоритма Евклида, если т и п — это произвольные натуральные числа (неравенство т>п может не выполняться)?
В доказательстве алгоритма Евклида, если t и p — произвольные натуральные числа, и не выполняется условие t > p, нужно будет учесть возможность того, что числа могут быть представлены в любом порядке. Алгоритм Евклида предполагает, что при каждом шаге мы уменьшаем большее из чисел, используя операцию взятия остатка. Если не выполнено условие t > p, алгоритм можно будет просто адаптировать, инвертировав их местами на первом шаге.
4. Зачем нужно определять инвариант цикла?
Определение инварианта цикла необходимо для доказательства корректности программы, особенно в контексте циклов. Инвариант цикла — это утверждение, которое остается истинным на каждом шаге выполнения цикла. Он помогает гарантировать, что программа, несмотря на итерации, будет правильно работать и достигнет цели. Инварианты помогают также минимизировать возможность ошибок при изменении программы или при попытке доказательства её правильности.
5. Почему желательно формулировать спецификацию в виде формальных утверждений, а не на естественном языке?
Формулировка спецификаций в виде формальных утверждений помогает точно и однозначно описать требования к программе, исключая неоднозначности, которые могут возникнуть при использовании естественного языка. Естественный язык часто бывает интерпретируемым по-разному, что может привести к ошибкам или недоразумениям. Формальные утверждения же облегчают процесс анализа, тестирования и доказательства корректности программы, поскольку они не поддаются двусмысленности и могут быть автоматически проверены с помощью инструментов формальной верификации.
6. Что такое предусловие и постусловие? Объясните запись
Предусловие — это условие, которое должно быть выполнено до начала выполнения программы или функции. Оно описывает, что должно быть истинным на момент вызова функции, чтобы она работала корректно. Постусловие — это условие, которое должно быть выполнено после завершения работы программы или функции. Оно описывает, что будет истинным после выполнения функции, если предусловие выполнено.
7. В чём различие между надёжной и корректной программами?
Корректная программа — это программа, которая выполняет свою задачу правильно, то есть удовлетворяет спецификации (условиям задачи) для всех допустимых входных данных. Надёжная программа — это программа, которая работает стабильно, даже если вводятся ошибочные или непредсказуемые данные. Она должна корректно обрабатывать исключения, избегать аварийных завершений и обеспечивать устойчивую работу. Надёжность включает в себя корректность, но также охватывает обработку ошибок и надежность при нестандартных входах.
8. Как вы думаете, можно ли назвать корректной программу, которая «зависает» при неверных исходных данных? Обсудите этот вопрос в классе.
Программа, которая «зависает» при неверных данных, не может быть полностью корректной. Важно, чтобы программа адекватно обрабатывала все возможные входные данные, включая ошибочные или несанкционированные. Если программа зависает, она нарушает принцип корректности, так как не выполняет свою задачу для всех возможных условий. Однако, с точки зрения теории, корректность программы может быть проверена только для допустимых входных данных, и если она не обрабатывает ошибочные данные, это указывает на недостаток в ее надёжности.
9. Что такое верификация программы?
Верификация программы — это процесс проверки программы на соответствие её спецификации и выявление возможных ошибок. Верификация может быть формальной, когда с помощью математических методов проверяется, что программа соответствует заранее заданным условиям, или тестовой, когда программа проходит серию тестов для проверки её функциональности.
10. Как вы думаете, что сложнее — доказывать правильность готовой программы или сразу писать программу, доказывая правильность отдельных блоков? Почему? Обсудите этот вопрос в классе.
Доказывать правильность готовой программы сложнее, потому что она уже содержит все блоки, которые могут взаимодействовать друг с другом. Ошибки могут скрываться в этих взаимодействиях, и проверка всей программы требует больше усилий и времени. Напротив, доказательство правильности отдельных блоков проще, потому что каждый блок можно проверить поочередно и независимо от других. Этот подход позволяет легче обнаружить ошибки на ранних стадиях разработки и минимизировать сложность проверки всей программы в будущем.