Formal Verification of Programs in the Pifagor Language

被引：0
作者：
Kropacheva, Mariya [1 ]
Legalov, Alexander [1 ]
机构：
[1] Siberian Fed Univ, Inst Space & Informat Technol, Krasnoyarsk 660074, Russia
来源：
PARALLEL COMPUTING TECHNOLOGIES (PACT 2013) | 2013年 / 7979卷
关键词：
Functional data-flow parallel programming; Pifagor programming language; programs formal verification;
D O I：
暂无
中图分类号：
TP [自动化技术、计算机技术];
学科分类号：
0812 ;
摘要：
The article is devoted to the methods of proving parallel programs correctness, that are based on the Hoare axiomatic system. In this article such system is being developed for proving the correctness of the programs in the functional data-flow parallel programming language Pifagor. Recursion correctness is proved by induction. This method could be used as a base of a toolkit to support program correctness proving, since it could be made automate at many stages.
引用
收藏
页码：80 / 89
页数：10
相关论文
共 6 条
  • [1] [Ануреев И.С. Anureev I.S.], 2010, [Моделирование и анализ информационных систем, Modelirovanie i analiz informatsionnykh sistem], V17, P5
  • [2] AN AXIOMATIC BASIS FOR COMPUTER PROGRAMMING
    HOARE, CAR
    [J]. COMMUNICATIONS OF THE ACM, 1969, 12 (10) : 576 - &
  • [3] Kropacheva M.S., 2011, 12 RUSS SCI PRACT C, P144
  • [4] Legalov A.I., 2005, COMPUT TECHNOL, V10, P71
  • [5] Nepomnyashiy V.A., 1988, APPL METHODS PROGRAM
  • [6] [Удалова Ю.В. Udalova Julia V.], 2011, [Журнал Сибирского федерального университета. Серия: Техника и технологии, Zhurnal Sibirskogo federal'nogo universiteta. Seriya: Tekhnika i tekhnologii], V4, P213
1