Difference between revisions of "Behavioral Abstraction is Hiding Information"
From FSL
Line 7: | Line 7: | ||
== CMCS'05 == | == CMCS'05 == | ||
<purge></purge> | <purge></purge> | ||
− | < | + | <pubbib id="rosu-2003-cmcs" template="PubDefaultWithAbstractAndTitle"/> |
Latest revision as of 23:59, 24 February 2016
This work has been published in a journal paper (J. of TCS) and in a workshop proceedings (CMCS'03). The journal version is an improved version of the one that appeared in the workshop proceedings.
[edit] J. of TCS
- Behavioral Abstraction is Hiding Information
- Grigore Rosu
- J. of TCS, Volume 327(1-2), pp 197-221. 2004
- Abstract. We show that for any behavioral
-specification
there is an ordinary algebraic specification
over a larger signature, such that a model behaviorally satisfies
iff it satisfies, in the ordinary sense, the
-theorems of
. The idea is to add machinery for contexts and experiments (sorts, operations and equations), use it, and then hide it. We develop a procedure, called unhiding, which takes a finite
and produces a finite
. The practical aspect of this procedure is that one can use any standard equational inductive theorem prover to derive behavioral theorems, even if neither equational reasoning nor induction is sound for behavioral satisfaction.
- Abstract. We show that for any behavioral
[edit] CMCS'05
- Inductive Behavioral Proofs by Unhiding
- Grigore Rosu
- CMCS'03, Volume 82(1), pp 285-302. 2003
- Abstract. We show that for any behavioral
-specification
there is an ordinary algebraic specification
over a larger signature, such that a model behaviorally satisfies
iff it satisfies, in the ordinary sense, the
-theorems of
. The idea is to add machinery for contexts and experiments (sorts, operations and equations), use it, and then hide it. We develop a procedure, called unhiding, which takes a finite
and produces a finite
. The practical aspect of this procedure is that one can use any standard equational inductive theorem prover to derive behavioral theorems, even if neither equational reasoning nor induction is sound for behavioral satisfaction.
- Abstract. We show that for any behavioral