Аннотация
Метод индуктивных утверждений изначально был сформулирован для верификации последовательных императивных программ. В статье предложено его использование для верификации функционально-потоковых параллельных программ на языке Пифагор. Представленная адаптация метода опирается на информационный граф функционально-потоковой модели параллельных вычислений. Спецификация пользователя задается с применением классических начальных и промежуточных утверждений. Для описания спецификации применяются формулы, которые реализованы с применением специализирован-ного языка. Начальное утверждение описывает общий вид аргумента функции. Для его описания доступны константы, определяющие тип аргумента, а также формулы, опреде-ляющие принадлежность аргумента к указанным интервалам, если он является численным. Промежуточные утверждения ставятся в соответствие с узлами информационного графа программы. Для описания промежуточных утверждений доступны все базовые операторы языка Пифагор, а также формулы, применяемые к начальному утверждению. Это позволя-ет накладывать на выполняемую программу различные условия и ограничения. Условия рекомендуется формулировать таким образом, чтобы они возвращали булево значение. В этом случае можно однозначно сделать заключение о том, соответствует или нет выпол-нение программы заданному утверждению. Помимо этого, полученное булево значение используется для отображения ошибок, возникающих в программе. Эти ошибки отображаются на информационном графе программы. Применение метода индуктивных утверждений для верификации функционально-потоковых параллельных программ позволяет проверить соответствие вычислений программы спецификации пользователя и интервально оценить вычисленные программой результаты. Это облегчает процесс разработки, те-стирования и отладки функционально-потоковых параллельных программ.
Ключевые слова: верификация, спецификация, корректность, функционально-потоковое параллельное программирование
