Inductive behavioral proofs by unhiding

Research output: Contribution to journalConference article

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 languageEnglish (US)
Pages (from-to)285-302
Number of pages18
JournalElectronic Notes in Theoretical Computer Science
Volume82
Issue number1
DOIs
StatePublished - Jul 2003
EventCMCS'03, Coalgebraic Methods in Computer Science Satellite Event for ETAPS 2003) - Warsaw, Poland
Duration: Apr 5 2003Apr 6 2003

Fingerprint

Specifications
Theorem
Machinery
Algebraic Specification
Acoustic waves
Sort
Proof by induction
Signature
Reasoning
Specification
Experiments
Experiment
Model
Sound
Standards
Context

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Inductive behavioral proofs by unhiding. / Rosu, Grigore.

In: Electronic Notes in Theoretical Computer Science, Vol. 82, No. 1, 07.2003, p. 285-302.

Research output: Contribution to journalConference article

@article{d65ec1a60b39401b8d33257400aed1ee,
title = "Inductive behavioral proofs by unhiding",
abstract = "We show that for any behavioral Σ-specification {\ss} there is an ordinary algebraic specification {\ss}̃ over a larger signature, such that a model behaviorally satisfies {\ss} iff it satisfies, in the ordinary sense, the ∑-theorems of {\ss}̃. 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 {\ss} and produces a finite {\ss}̃. 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.",
author = "Grigore Rosu",
year = "2003",
month = "7",
doi = "10.1016/S1571-0661(04)80645-5",
language = "English (US)",
volume = "82",
pages = "285--302",
journal = "Electronic Notes in Theoretical Computer Science",
issn = "1571-0661",
publisher = "Elsevier",
number = "1",

}

TY - JOUR

T1 - Inductive behavioral proofs by unhiding

AU - Rosu, Grigore

PY - 2003/7

Y1 - 2003/7

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

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

UR - http://www.scopus.com/inward/record.url?scp=18944390756&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=18944390756&partnerID=8YFLogxK

U2 - 10.1016/S1571-0661(04)80645-5

DO - 10.1016/S1571-0661(04)80645-5

M3 - Conference article

AN - SCOPUS:18944390756

VL - 82

SP - 285

EP - 302

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

SN - 1571-0661

IS - 1

ER -