Abstract | ||
---|---|---|
The semantics of Statecharts macro steps, as introduced by Pnueli and Shalev [1991], lacks compositionality. This article first analyzes the compositionality problem and traces it back to the invalidity of the Law of the Excluded Middle. It then characterizes the semantics via a particular class of linear intuitionistic Kripke models. This yields, for the first time in the literature, a simple fully abstract semantics that interprets Pnueli and Shalev's concept of failure naturally. The results not only give insight into the semantic subtleties of Statecharts, but also provide a basis for an implementation, for developing algebraic theories for macro steps, and for comparing different Statecharts variants. |
Year | DOI | Venue |
---|---|---|
2002 | 10.1145/504077.504078 | ACM Transactions on Computational Logic (TOCL) |
Keywords | Field | DocType |
statecharts macro step,semantic subtlety,statecharts step,macro step,compositionality,linear intuitionistic kripke model,different statecharts variant,particular class,full abstraction,kripke semantics,intuitionistic logic,statecharts,algebraic theory,compositionality problem,abstract semantics,syntax,analysis of variance,high level languages,computer programming,semantics,structured programming | Principle of compositionality,Intuitionistic logic,Programming language,Law of excluded middle,Kripke semantics,Computer science,Intuitionism,Theoretical computer science,High-level programming language,Macro,Semantics | Journal |
Volume | Issue | Citations |
3 | 1 | 10 |
PageRank | References | Authors |
0.70 | 18 | 2 |
Name | Order | Citations | PageRank |
---|---|---|---|
Gerald Lüttgen | 1 | 600 | 40.71 |
Michael Mendler | 2 | 314 | 34.60 |