Difference between revisions of "Behavioral Abstraction is Hiding Information"

Latest revision as of 00:00, 25 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.

PDF, J.TCS, BIB

[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.

PDF, Logic, DOI, CMCS'03, BIB