Abstract
The method of inductive assertions was originally formulated for the verification of successive imperative programs. The use of this method for the verification of functional dataflow parallel programs developed in the Pythagor programming language is suggested in this paper. The adaptation of the inductive assertions method presented in the paper is based on the dataflow graph of a functional dataflow model of parallel calculation. A user's specification is specified by classical initial and intermediate assertions described by special formulas. These formulas are implemented by using a special language.
An initial assertion describes a general form of an argument of a function. To describe it there are constants that determine the type of the argument. The formulas can specify the intervals in which arguments can be changed. Intermediate assertions correspond to the nodes of an information graph of the program. All basic language statements of the Pythagor language and formulas used to the initial assertion are available to describe intermediate assertions. This makes it possible to impose various conditions and constraints on the program which is running. Conditions must be formulated in such a way that they return a Boolean value. In this case it possible to make a definite conclusion whether the execution of the program corresponds to the specified assertion or not, In addition, the obtained Boolean value is used for displaying errors occurring in the program. These errors are displayed in the information graph of the program. The application of the method of inductive assertions to verify functional dataflow parallel programs makes it possible to check the agreement of the program computations with a user’s specification and to estimate the results of the program computation by intervals. This simplifies the process of developing, testing and debugging of functional dataflow parallel programs.
Keywords: verification, specification, correctness, functional dataflow parallel programming
