Analysis of coroutines by means of vector of coroutines

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 …