Authors


Title


Status, Abstract

Peter Kempf

Department of Computer Science
University of the Federal Armed Forces Munich
85577 Neubiberg, Germany

Konstruktion
induktiv geordneter Modelle
aus algebraischen Spezifikationen


.pdf .bib

Tech. Report Nr. 1998-04

Gunther Schmidt

Department of Computer Science
University of the Federal Armed Forces Munich
85577 Neubiberg, Germany
schmidt@informatik.unibw-muenchen.de
In theoretical investigations of software construction one will often need tools to interpret higher-order functions and algebraic specifications. For higher-order functions one is used to employ constructs such as algebraic cpo's. Algebraic specifications are usually handled via term algebra and a congruence on it, induced by the algebraic laws. When trying to obtain semantic domains directly from the algebraic specifications, the ordering has to be compatible with the induced congruence. Former work (e.g. Möller 85, Jiri et al. 91 Jouannoud Okada 91) introduced an ordering on a quotient of the term algebra and got a model via ideal completion. We will first show that these methods lead to undesired effects. Then we propose an approach using so-called complete and approximation-preserving congruences on semantic domains with sprouts (see Gunter 85, Schmidt et al. 86, Schmidt et al. 89) avoiding such effects. This approach allows to construct the semantic domains intended directly from the algebraic specification using a generalized deduction logic and an inverse limit construction producing the initial model in the class of inductively ordered models of the specification.

Michael Winter

Department of Computer Science
University of the Federal Armed Forces Munich
85577 Neubiberg, Germany
thrash@informatik.unibw-muenchen.de