Axiomatizing schemes and their behaviors. (English) Zbl 0613.68013

Flowcharts represent in an abstract way the family of while programs, and flowchart schemes are flowcharts where the individual atomic steps have not been interpreted. It is a classical question to characterize when two flowchart schemes compute the same function under all possible interpretations. This question has been answered: two schemes are equivalent if they produce the same unwinding as infinitary trees. There remains the problem of determining this equivalence in a more down-to- earth way, for example by a characterization using axioms or, more specifically, by an equational theory.
The name of C. C. Elgot is connected to the algebraic theory which originates from this problem area. The algebras involved are known by the name Iterative theories. The basic algebraic operations are sequential composition, pairing (or more general tuppling), and iteration. The problem was that these operations were not everywhere defined, and therefore a partial algebra resulted.
In the present paper the authors provide an extension of the domain of these operations which turns them into everywhere defined operations. The resulting total algebra is provided with a full and complete equational axiomatization for the required equivalence of program schemes. The paper presumes familiarity with the earlier papers in this area, which it may bring to a temporary conclusion.
Reviewer: P.van Emde Boas


68Q60 Specification and verification (program logics, model checking, etc.)
Full Text: DOI


[1] Bloom, S.L.; Ginali, S.; Rutledge, J., Scalar and vector iteration, J. comput. system sci., 14, 251-256, (1977) · Zbl 0358.68072
[2] Bloom, Stephen L.; Elgot, C.C., The existence and construction of free iterative theories, J. xomput. system sci., 12, 305-318, (1976) · Zbl 0333.68017
[3] Bloom, S.L.; Elgot, C.C.; Wright, J.B.; Bloom, S.L.; Elgot, C.C.; Wright, J.B., Solutions of the iteration equation and extensions of the scalar iteration operation; vector iteration in pointed iterative theories, SIAM J. comput., SIAM J. comput., 9, No. 3, (1980), reprinted in [CCE, 275-312] · Zbl 0454.18011
[4] Bloom, S.L.; Tindell, R., Algebraic and graph theoretic characterizations of structured flowchart schemes, Theoret. comput. sci., 9, No. 3, 265-286, (1979) · Zbl 0405.68013
[5] ()
[6] Troeger, D., An axiomatization of D-scheme strong equivalence, J. comput. system sci., 27, No. 2, 221-224, (1983) · Zbl 0547.68019
[7] Elgot, C.C., Monadic computation and iterative algebraic theories, (), 175-230, reprinted in [CCE, 179-234] · Zbl 0327.02040
[8] Elgot, C.C.; Bloom, S.L.; Tindell, R., On the algebraic structure of rooted trees, J. comput. system sci., 16, No. 3, 362-399, (1978), reprinted in [CCE, 236-273] · Zbl 0389.68007
[9] Elgot, C.C., Structured programming with and without Goto statements, IEEE trans. software engrg., SE-2, No. 1, 41-54, (1976), reprinted in CCE, 313-326 · Zbl 0348.68008
[10] {\scC. C. Elgot and J. Shepherdson}, An equational axiomatization of reducible flowchart schemes, in [CCE, 301-349]. · Zbl 0475.68002
[11] Elgot, C.C., Some geometrical categories associated with flowchart schemes, () · Zbl 0385.18003
[12] Esiic, Z., Identities in iterative and rational theories, Comput. linguistics comput. languages, 14, 183-207, (1980)
[13] Esik, Z., Algebras of iteration theories, J. comp. system sci., 27, 291-303, (1983) · Zbl 0532.68011
[14] Yoepp, J., Flowchart schemes, algebras and covers, ()
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.