zbMATH — the first resource for mathematics

Algebraic theory of module specifications with constraints. (English) Zbl 0602.68021
Mathematical foundations of computer science, Proc. 12th Symp., Bratislava/Czech. 1986, Lect. Notes Comput. Sci. 233, 59-77 (1986).
[For the entire collection see Zbl 0596.00021.]
The concept for modules in software engineering based on equational algebraic specifications is extended by a suitable notion of constraints. This allows to have loose specifications with constraints for parameter, export and import interfaces of module specifications without loosing executability of the body specification. Correctness of such module specifications ensures that data types satisfying the import constraints are transformed into ones satisfying the export constraints. Operations on module specifications like composition, actualization and union are extended to the case with constraints. They are shown to preserve correctness and to be compositional w.r.t. the semantics. Moreover these operations on module specifications satisfy algebraic laws comparable to those of R-modules in algebra.

68P05 Data structures
68Q60 Specification and verification (program logics, model checking, etc.)