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.
Original language | English (US) |
---|---|
Pages (from-to) | 285-302 |
Number of pages | 18 |
Journal | Electronic Notes in Theoretical Computer Science |
Volume | 82 |
Issue number | 1 |
DOIs | |
State | Published - Jul 2003 |
Event | CMCS'03, Coalgebraic Methods in Computer Science Satellite Event for ETAPS 2003) - Warsaw, Poland Duration: Apr 5 2003 → Apr 6 2003 |
ASJC Scopus subject areas
- Theoretical Computer Science
- General Computer Science