No label defined (Q4029607)

[For the entire collection see Zbl 0745.00057.] In [\textit{D. Skordev}, Lect. Notes Comput. Sci. 208, 326-331 (1985; Zbl 0622.68048)], we tried to show by an example the usefulness of a certain notion of homomorphism for proving the equivalence of some structured programs (in that example the equivalence of two concrete Pascal programs was proved). The homomorphisms which appear in the example in question were in fact partial-multivalued homomorphisms between many-sorted partial-multivalued algebras with only unary operations, although the notion of partial-multivalued homomorphism was introduced in the same paper for the general case of many-sorted partial-multivalued algebras with arbitrary signatures (and even for a more general class of systems). Unfortunately, the description of the signatures of the many-sorted algebras used overburdens heavily the exposition even in the case of only unary operations. Therefore we now consider its desirable to avoid the use of many sorts of objects in the treatment of such examples. This turns out to be possible due to the fact that for each given program of the kind in question we have a corresponding set of memory states (namely the set of all admissible valuations of its variables) and each part of the program can be considered as describing some partial mapping of this set into itself (although a small part of the program usually concerns only a small number of its variables and therefore the above set of memory states could seem to be the most suitable for the study of such a part).