Authors |
Title |
Status, Abstract |
|
Peter Kempf |
Department of Computer Science University of the Federal Armed Forces Munich 85577 Neubiberg, Germany |
Konstruktion |
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 |