%0 Journal Article %1 lermer_01_refinement %A Lermer, Karl %A Strooper, Paul %D 2001 %J Theoretical Computer Science %K refinement statecharts 2001 %N 1-2 %P 195--235 %R 10.1016/S0304-3975(00)00169-9 %T Refinement and state machine abstraction %U http://dx.doi.org/10.1016/S0304-3975(00)00169-9 %V 266 %X Precise module interface specifications are essential in modular software development. The role of state in these specifications has been the issue of some debate and is central to the notion of data refinement. In previous work, Hoffman and Strooper introduce a state-abstraction lattice that defines a partial order on specifications for deterministic and complete languages. They use this lattice to define a notion of state abstractness and show that this intuitive notion corresponds to the use of the terms äbstract" and "concrete" as used in data-refinement proofs. In this paper, we extend this work for a class of specifications and languages that we call demonic and semi-deterministic. We also introduce a notion of backward refinement and prove that backward refinement together with the common forward refinement of VDM and Z form a sound and complete refinement technique with respect to a partial order on languages defined by demonic specifications. We illustrate the ideas using simple languages and specifications.

@article{lermer_01_refinement, abstract = {Precise module interface specifications are essential in modular software development. The role of state in these specifications has been the issue of some debate and is central to the notion of data refinement. In previous work, Hoffman and Strooper introduce a state-abstraction lattice that defines a partial order on specifications for deterministic and complete languages. They use this lattice to define a notion of state abstractness and show that this intuitive notion corresponds to the use of the terms "abstract" and "concrete" as used in data-refinement proofs. In this paper, we extend this work for a class of specifications and languages that we call demonic and semi-deterministic. We also introduce a notion of backward refinement and prove that backward refinement together with the common forward refinement of VDM and Z form a sound and complete refinement technique with respect to a partial order on languages defined by demonic specifications. We illustrate the ideas using simple languages and specifications.}, added-at = {2009-02-12T11:15:14.000+0100}, author = {Lermer, Karl and Strooper, Paul}, biburl = {https://www.bibsonomy.org/bibtex/2ed33bbdc990155ec18f78ea63309c968/leonardo}, citeulike-article-id = {895443}, doi = {10.1016/S0304-3975(00)00169-9}, interhash = {581882fe3e74b298a8cdcae460331af7}, intrahash = {ed33bbdc990155ec18f78ea63309c968}, journal = {Theoretical Computer Science}, keywords = {refinement statecharts 2001}, month = {September}, number = {1-2}, pages = {195--235}, posted-at = {2006-10-13 14:57:44}, priority = {4}, timestamp = {2009-02-12T11:15:14.000+0100}, title = {Refinement and state machine abstraction}, url = {http://dx.doi.org/10.1016/S0304-3975(00)00169-9}, volume = 266, year = 2001 }