Тип публикации: статья из журнала
Год издания: 2015
Идентификатор DOI: 10.18255/1818-1015-2015-4-578-589
Ключевые слова: functional data-flow parallel programming, Pifagor programming language, programs formal verification, toolkit for supporting formal verification, функционально-потоковое параллельное программирование, язык программирования Пифагор, формальная верификация программ, инструментальные средства для поддержки формальной верификации
Аннотация: Nowadays, due to software sophistication, programs correctness is more often proved by means of formal verification. The method of deduction based on Hoare logic could be used for any programming language and it has the capability of partial automation of the proof process. However, the method of deduction is not widely used for veПоказать полностьюrification of parallel programs because of high complexity of the process. The usage of the functional data-flow paradigm of parallel programming allows to decrease the complexity of the proof process. In this article a proof process of correctness of functional data-flow parallel programs in the Pifagor language is considered. The proof process of a program correctness is considered as a tree where each node is a program data-flow graph, whose edges are marked with formulas in a specification language. The tree root is the initial program data-flow graph with a precondition and a postcondition, which describe restrictions on input variables and correctness conditions of the result of the program execution, respectively. Basic transformations of the data-flow graph are edge marking, equivalent transformation, splitting, folding of the program. By means of these transformations the data-flow graph is transformed and finally is reduced to a set of formulas in the specification language. If all these formulas are identically true, the program is correct. Several modules is distinguished in the system: "Program correctness prover", "Axioms and theorems library management system" and "Errors analysis and output of information about errors". According to this architecture, the toolkit for supporting formal verification was developed. The main functionality of the system implementation is considered.
Журнал: Моделирование и анализ информационных систем
Выпуск журнала: Т. 22, № 4
Номера страниц: 578-589
ISSN журнала: 18181015
Место издания: Ярославль
Издатель: федеральное государственное бюджетное образовательное учреждение высшего образования "Ярославский государственный университет им. П.Г. Демидова"