Статья 307

Пожалуй, до сих пор это применение строгих математических методов в качестве инструмента критики концепций зачастую совершенно не продуманных, вставляемых ради усиления языков программирования является важнейшим применением логики в данной области.
Остановимся на трех ветвях прикладной логики, наиболее близких к задачам традиционной логики как описывать программы с помощью логики, как описывать само программирование, как анализировать концепции логическими средствами.

Логики описания программ.

Как известно, правильность созданной программы обычно проверяется на ряде так называемых тестовых примеров, на начальных данных, для которых возможно предсказать результат. Неоднократно отмечалось, что такая проверка может лишь выявить наличие ошибок, но не доказать их отсутствие. Поэтому важна задача строгого доказательства правильности программ, и именно для этой цели и начали разрабатываться программные и динамические логики.