2014 УДК 004.052.42 ВЕРИФИКАЦИЯ ФУНКЦИОНАЛЬНО-ПОТОКОВЫХ ПАРАЛЛЕЛЬНЫХ ПРОГРАММ МЕТОДОМ ИНДУКТИВНЫХ УТВЕРЖДЕНИЙ Ю.В. <...> Удалова, А.И. Легалов Сибирский федеральный университет Метод индуктивных утверждений изначально был сформулирован для верификации последовательных императивных программ. <...> В статье предложено его использование для верификации функционально-потоковых параллельных программ на языке Пифагор. <...> Представленная адаптация метода опирается на информационный граф функциональнопотоковой модели параллельных вычислений. <...> Спецификация пользователя задается с применением классических начальных и промежуточных утверждений. <...> Для описания спецификации применяются формулы, которые реализованы с применением специализированного языка. <...> Начальное утверждение описывает общий вид аргумента функции. <...> Для его описания доступны константы, определяющие тип аргумента, а также формулы, определяющие принадлежность аргумента к указанным интервалам, если он является численным. <...> Промежуточные утверждения ставятся в соответствие с узлами информационного графа программы. <...> Для описания промежуточных утверждений доступны все базовые операторы языка Пифагор, а также формулы, применяемые к начальному утверждению. <...> Это позволяет накладывать на выполняемую программу различные условия и ограничения. <...> Условия рекомендуется формулировать таким образом, чтобы они возвращали булево значение. <...> В этом случае можно однозначно сделать заключение о том, соответствует или нет выполнение программы заданному утверждению. <...> Помимо этого, полученное булево значение используется для отображения ошибок, возникающих в программе. <...> Эти ошибки отображаются на информационном графе программы. <...> Применение метода индуктивных утверждений для верификации функционально-потоковых параллельных программ позволяет проверить соответствие вычислений программы спецификации пользователя и интервально оценить вычисленные программой <...>