Analysis of coroutines by means of vector of coroutines

Abstract

In this paper two methods of proving properties of programs with coroutines are presented. Both of these methods are based on a mathematical model which was defined in [3] and extended in [4], and which is called a vector of coroutines. In the case of the first method, the vector semantics is given by the least solution of an appropriate set of equations. This set of equations is constructed on the basis of the form of the whole vector. In the case of the second method, a suitable alphabet and a suitable language are associated with each of the vector components (each component corresponds to one coroutine of the program), and the intersection of these languages is interpreted as a description of the vector semantics. The theorem on the replacement of components by equivalent (in a special sense) components is proved.