Формальная верификация циклических программ.
Федяев О.И.
В статье рассматривается аналитический подход к оценке корректности сложных программ. На примере доказательства правильности программы сортировки проведена апробация теоретико-функционального метода верификации. Формализм программных функций позволил математически строго преодолеть сложности доказательства правильности обработки элементов массива во вложенных циклах. Результаты статьи подтверждают возможность применения данного метода на практике в программной инженерии. Ключевые слова: верификация программы, корректность программы, программная функция, доказательство правильности программы, теоретико-функциональный подход.
