Dynamic algebras with test

Logic in computer science (03B70) Other algebras related to logic (03G25) Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65)

Review text

The paper contributes to the so far developed theory of regular dynamic algebras [for a survey see, e.g., \textit{D. Kozen}, Lect. Notes Comput. Sci. 125, 1-11 (1981; Zbl 0482.03008)]. Test algebras provide an algebraic abstraction capturing logical aspects of if-then-else and while-do like programming constructs. Most results on dynamic algebras extend directly to test algebras. The paper investigates results which require more subtle argumentation and results which do not hold in the case of dynamic algebras. The following main results are proven: every free algebra in the equational class generated by separable test algebras is isomorphic to a Kripke test structure; free separable test algebras over finitely many generators do not exist; epimorphisms in the equational class generated by separable dynamic or test algebras are not necessarily surjective.

Recommendations

Cites work

Cited in

(11)

This page was built for publication: Dynamic algebras with test

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1095141)