Удалова Юлия Васильевна,
Легалов Александр Иванович
Аннотация
Метод индуктивных утверждений изначально был сформулирован для верификации последовательных императивных программ. В статье предложено его использование для верификации функционально-потоковых параллельных программ на языке Пифагор. Представленная адаптация метода опирается на информационный граф функционально-потоковой модели параллельных вычислений. Спецификация пользователя задается с применением классических начальных и промежуточных утверждений. Для описания спецификации применяются формулы, которые реализованы с применением специализирован-ного языка. Начальное утверждение описывает общий вид аргумента функции. Для его описания доступны константы, определяющие тип аргумента, а также формулы, опреде-ляющие принадлежность аргумента к указанным интервалам, если он является численным. Промежуточные утверждения ставятся в соответствие с узлами информационного графа программы. Для описания промежуточных утверждений доступны все базовые операторы языка Пифагор, а также формулы, применяемые к начальному утверждению. Это позволя-ет накладывать на выполняемую программу различные условия и ограничения. Условия рекомендуется формулировать таким образом, чтобы они возвращали булево значение. В этом случае можно однозначно сделать заключение о том, соответствует или нет выпол-нение программы заданному утверждению. Помимо этого, полученное булево значение используется для отображения ошибок, возникающих в программе. Эти ошибки отображаются на информационном графе программы. Применение метода индуктивных утверждений для верификации функционально-потоковых параллельных программ позволяет проверить соответствие вычислений программы спецификации пользователя и интервально оценить вычисленные программой результаты. Это облегчает процесс разработки, те-стирования и отладки функционально-потоковых параллельных программ.
Ключевые слова: верификация, спецификация, корректность, функционально-потоковое параллельное программирование
Авторы:
Удалова Юлия Васильевна
старший преподаватель кафедры «Высокопроизводительные вычисления», Сибирский федеральный университет. Область научных интересов: параллельное программирование, методы верификации программ. Опубликовано 20 научных работ. (Адрес: 660074, Россия, Красноярск, ул. акад. Кирен-ского, 26. Email: uuuu82@inbox.ru).
Легалов Александр Иванович
д-р техн. наук, профессор, заведующий кафедрой вычислительной техники, Сибирский федеральный университет. Область научных интересов: технологии раз-работки программного обеспечения, языки программирования, паралле-лизм. Опубликовано 160 научных работ. (Адрес: 660074, Россия, Красноярск, ул. акад. Киренского, 26. Email: legalov@mail.ru).
Список литературы
- Легалов А.И. Функциональный язык для создания архитектурно-независимых параллельных программ // Вычислительные технологии. – 2005. – Т. 10, № 1. – С. 71–89.
- Удалова Ю.В., Легалов А.И., Сиротинина Н.Ю. Средства отладки функционально-потоковых параллельных программ // Доклады Академии наук высшей школы Российской Федерации. – 2008. – № 1 (10). – С. 96–105.
- Удалова Ю.В., Легалов А.И., Сиротинина Н.Ю. Методы отладки и верификации функционально-потоковых параллельных программ // Журнал Сибирского федерального университета. Серия: Техника и технологии. – 2011. – Т. 4, № 2. – С. 213–224.
- Лисков Б., Гатэг Дж. Использование абстракций и спецификаций при разработке программ. – М.: Мир, 1989. – 424 с.
