Model-Level vs Theory-Level Semantics

The Heterogeneous Tool Set (Hets)
Structured and Specifications Development Graphs
Benchmark Examples
Model-Level vs Theory-Level Semantics
1 2 1Till Mossakowski Florian Rabe Mihai Codescu
1DFKI GmbH Bremen and University of Bremen
2Jacobs University Bremen
12.09.2009, Udine, IFIP WG 1.3 Meeting
Till Mossakowski, Florian Rabe, Mihai Codescu Model-Level vs Theory-Level SemanticsThe Heterogeneous Tool Set (Hets)
Structured and Specifications Development Graphs
Benchmark Examples
Introduction
Two di erent semantics for structured specifications:
model-level semantics: the semantics of a specification SP is
a signature Sig(SP) and a class of models Mod(SP) over
Sig(SP)
theory-level semantics: the semantics of a specification is a
signature Sig(SP) and a set of sentences Th(SP) over
Sig(SP)
Both semantics are easily reconciled if there is no hiding (and also
no freeness), because in this case:
Mod(SP)=Mod(Th(SP))
However, in presence of hiding, this equation does not hold!
(examples: later)
Till Mossakowski, Florian Rabe, Mihai Codescu Model-Level vs Theory-Level SemanticsThe Heterogeneous Tool Set (Hets)
Structured and Specifications Development Graphs
Benchmark Examples
Some history
model-level semantics
ASL (Sannella, Wirsing 1983)
specification in an arbitrary institution (Sannella, Tarlecki
1988)
algebraic specification languages (CASL, 1990’s )
theory-level semantics
Clear (Goguen, Burstall 1980)
structured theories, conservative extensions and interpolation
(Maibaum, ...