@inproceedings{d2eb94545a3c4937a87d276044f7138c,
title = "Hierarchical heterogeneous specifications",
abstract = "We propose a definition of hierarchical heterogeneous formal specifications, where each module is specified according to its own homogeneous logic. We focus on the specification structure which we represent by a term in order to take benefit of classical knowledge on terms. For example, substitutions solve implementation sharing of modules. Then, we show how proof mechanisms can be expressed inside our framework. Our proof system involves both the homogeneous inference relations associated to the logics of modules and property inheritance relations associated to the structuring primitives. Heterogeneous primitives allow to move from one logic to another.We sketch out the specification of a travel agency given according to our particular framework of structured specifications. We demonstrate on this specification how a heterogeneous proof can be handled.",
keywords = "Algebraic specification, Formal specification, Heterogeneous proof, Heterogeneous specification, Inference system, Logical framework, Modularity, Proof theory, Structured specification",
author = "Sophie Coudert and Gilles Bernot and \{Le Gall\}, Pascale",
note = "Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 1999.; 13th International Workshop on Algebraic Development Techniques, WADT 1998 ; Conference date: 02-04-1998 Through 04-04-1998",
year = "1999",
month = jan,
day = "1",
doi = "10.1007/3-540-48483-3\_8",
language = "English",
isbn = "3540662464",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "107--121",
editor = "Fiadeiro, \{Jos{\'e} Luiz\}",
booktitle = "Recent Trends in Algebraic Development Techniques - 13th International Workshop, WADT 1998, Selected Papers",
}