Title
The intuitionism behind Statecharts steps
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üttgen160040.71
Michael Mendler231434.60