maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State University10.18255/1818-1015-2012-5-81-99mais-59Research ArticleОригинальные статьиArticlesФормальная верификация программ, написанных на функционально-потоковом языке параллельного программированияFormal Verification of Programs in Functional Dataflow Parallel LanguageКропачеваМария СергеевнаKropachevaM. S.

аспирант

аспирант

ksv@akadem.ruЛегаловАлександр ИвановичLegalovA. I.

профессор

профессор

legalov@mail.ruСибирский федеральный университетРоссияСибирский федеральный университетRussian Federation2012040320151958199Copyright © Кропачева М.С., Легалов А.И., 20152015Кропачева М.С., Легалов А.И.Kropacheva M.S., Legalov A.I.Данная работа распространяется под лицензией Creative Commons Attribution 4.0.This work is licensed under a Creative Commons Attribution 4.0 License.https://www.mais-journal.ru/jour/article/view/59

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

The article is devoted to the methods of proving parallel programs correctness that are based on the axiomatic approach. Formal system for functional data-flow parallel programming language Pifagor is described. On the basis of this system programs correctness could be proved.

функционально-потоковое параллельное программированиеязык программирования Пифагорформальная верификация программfunctional data-flow parallel programmingPifagor programming languageprograms formal verificationReferencesНепомнящий В.А., Рякин О.М. Прикладные методы верификации программ. М.: Радио и связь, 1988. 255 с.Непомнящий В.А., Рякин О.М. Прикладные методы верификации программ. М.: Радио и связь, 1988. 255 с.Hoare C. A. R. An axiomatic basis for computer programming // Communications of the ACM. 1969. Vol. 10. N. 12. P. 576–585.Hoare C. A. R. An axiomatic basis for computer programming // Communications of the ACM. 1969. Vol. 10. N. 12. P. 576–585.Ануреев И. С., Марьясов И. В., Непомнящий В. А. Верификация C-программ на основе смешанной аксиоматической семантики // Моделирование и анализ информационных систем. 2010. Т. 17, № 3. C. 5–28.Ануреев И. С., Марьясов И. В., Непомнящий В. А. Верификация C-программ на основе смешанной аксиоматической семантики // Моделирование и анализ информационных систем. 2010. Т. 17, № 3. C. 5–28.Легалов А.И. Функциональный язык для создания архитектурно-независимых параллельных программ // Вычислительные технологии. 2005. № 1 (10). С. 71–89.Легалов А.И. Функциональный язык для создания архитектурно-независимых параллельных программ // Вычислительные технологии. 2005. № 1 (10). С. 71–89.Удалова Ю.В., Легалов А.И., Сиротинина Н.Ю. Методы отладки и верификации функционально-потоковых параллельных программ // Журнал Сибирского федерального университета. Серия: Техника и технологии. 2011. Т. 4. № 2. С. 213–224.Удалова Ю.В., Легалов А.И., Сиротинина Н.Ю. Методы отладки и верификации функционально-потоковых параллельных программ // Журнал Сибирского федерального университета. Серия: Техника и технологии. 2011. Т. 4. № 2. С. 213–224.Легалов А.И., Казаков Ф.А., Кузьмин Д.А., Привалихин Д.В. Функциональная модель параллельных вычислений и язык программирования «Пифагор»: ttp://www.softcraft.ru/fppp.shtmlЛегалов А.И., Казаков Ф.А., Кузьмин Д.А., Привалихин Д.В. Функциональная модель параллельных вычислений и язык программирования «Пифагор»: ttp://www.softcraft.ru/fppp.shtmlЛегалов А.И. Использование асинхронно поступающих данных в потоковой модели вычислений / Третья сибирская школа-семинар по параллельным вычислениям. Томск: Изд-во Томского ун-та, 2006. С. 113–120.Легалов А.И. Использование асинхронно поступающих данных в потоковой модели вычислений / Третья сибирская школа-семинар по параллельным вычислениям. Томск: Изд-во Томского ун-та, 2006. С. 113–120.Кропачева М.С. Формализация семантики функционально-потокового языка параллельного программирования Пифагор // Проблемы информатизации региона. ПИР-2011: Материалы XII Всероссийской научно-практической конференции. Красноярск: Сибирский федеральный университет. 2011. С. 144–148.Кропачева М.С. Формализация семантики функционально-потокового языка параллельного программирования Пифагор // Проблемы информатизации региона. ПИР-2011: Материалы XII Всероссийской научно-практической конференции. Красноярск: Сибирский федеральный университет. 2011. С. 144–148.Чень Л. Математическая логика и автоматическое доказательство теорем / Под ред. С.Ю. Маслова. М.: Наука, 1983. 358 с.Чень Л. Математическая логика и автоматическое доказательство теорем / Под ред. С.Ю. Маслова. М.: Наука, 1983. 358 с.Harrison J. Handbook Of Practical Logic And Automated Reasoning New York: Cambridge University Press, 2009. 781 p.Harrison J. Handbook Of Practical Logic And Automated Reasoning New York: Cambridge University Press, 2009. 781 p.

The authors declare that there are no conflicts of interest present.