Verifiable and executable logic specifications of concurrent objects in Lπ

Luis Caires; Luis Monteiro

Verifiable and executable logic specifications of concurrent objects in L_π

Luis Caires, Luis Monteiro

DI - Departamento de Informática

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

1 Citation (Scopus)

Abstract

We present the core- L_π fragment of L_π and its program logic. We illustrate the adequacy of L_π, as a meta-language for jointly defining operational semantics and program logics of languages with concurrent and logic features, considering the case of a specification logic for concurrent objects addressing mobile features like creation of objects and channels in a simple way. Specifications are executable by a translation that assigns to every specification a model in the form of a core-L_π program. We also illustrate the usefulness of this framework in reasoning about systems and their components.

Original language	English
Title of host publication	Programming Languages and Systems - 7th European Symposium on Programming, ESOP 1998 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 1998, Proceedings
Editors	Chris Hankin
Publisher	Springer Verlag
Pages	42-56
Number of pages	15
ISBN (Print)	3540643028, 9783540643029
Publication status	Published - 1 Jan 1998
Event	7th European Symposium on Programming, ESOP 1998 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 1998 - Lisbon, Portugal Duration: 28 Mar 1998 → 4 Apr 1998

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Publisher	Springer Verlag
Volume	1381
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	7th European Symposium on Programming, ESOP 1998 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 1998
Country/Territory	Portugal
City	Lisbon
Period	28/03/98 → 4/04/98

Keywords

Semantics
Models
Bigraphical reactive

Cite this

Caires, L., & Monteiro, L. (1998). Verifiable and executable logic specifications of concurrent objects in L_π. In C. Hankin (Ed.), Programming Languages and Systems - 7th European Symposium on Programming, ESOP 1998 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 1998, Proceedings (pp. 42-56). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 1381). Springer Verlag.

Caires, Luis ; Monteiro, Luis. / Verifiable and executable logic specifications of concurrent objects in L_π. Programming Languages and Systems - 7th European Symposium on Programming, ESOP 1998 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 1998, Proceedings. editor / Chris Hankin. Springer Verlag, 1998. pp. 42-56 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{d8dd6b191f0849208c130e025f8e406f,

title = "Verifiable and executable logic specifications of concurrent objects in Lπ",

abstract = "We present the core- Lπ fragment of Lπ and its program logic. We illustrate the adequacy of Lπ, as a meta-language for jointly defining operational semantics and program logics of languages with concurrent and logic features, considering the case of a specification logic for concurrent objects addressing mobile features like creation of objects and channels in a simple way. Specifications are executable by a translation that assigns to every specification a model in the form of a core-Lπ program. We also illustrate the usefulness of this framework in reasoning about systems and their components.",

keywords = "Semantics, Models, Bigraphical reactive",

author = "Luis Caires and Luis Monteiro",

year = "1998",

month = jan,

day = "1",

language = "English",

isbn = "3540643028",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "42--56",

editor = "Chris Hankin",

booktitle = "Programming Languages and Systems - 7th European Symposium on Programming, ESOP 1998 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 1998, Proceedings",

note = "7th European Symposium on Programming, ESOP 1998 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 1998 ; Conference date: 28-03-1998 Through 04-04-1998",

}

Caires, L & Monteiro, L 1998, Verifiable and executable logic specifications of concurrent objects in L_π. in C Hankin (ed.), Programming Languages and Systems - 7th European Symposium on Programming, ESOP 1998 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 1998, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 1381, Springer Verlag, pp. 42-56, 7th European Symposium on Programming, ESOP 1998 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 1998, Lisbon, Portugal, 28/03/98.

Verifiable and executable logic specifications of concurrent objects in L_π. / Caires, Luis ; Monteiro, Luis.
Programming Languages and Systems - 7th European Symposium on Programming, ESOP 1998 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 1998, Proceedings. ed. / Chris Hankin. Springer Verlag, 1998. p. 42-56 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 1381).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Verifiable and executable logic specifications of concurrent objects in Lπ

AU - Caires, Luis

AU - Monteiro, Luis

PY - 1998/1/1

Y1 - 1998/1/1

N2 - We present the core- Lπ fragment of Lπ and its program logic. We illustrate the adequacy of Lπ, as a meta-language for jointly defining operational semantics and program logics of languages with concurrent and logic features, considering the case of a specification logic for concurrent objects addressing mobile features like creation of objects and channels in a simple way. Specifications are executable by a translation that assigns to every specification a model in the form of a core-Lπ program. We also illustrate the usefulness of this framework in reasoning about systems and their components.

AB - We present the core- Lπ fragment of Lπ and its program logic. We illustrate the adequacy of Lπ, as a meta-language for jointly defining operational semantics and program logics of languages with concurrent and logic features, considering the case of a specification logic for concurrent objects addressing mobile features like creation of objects and channels in a simple way. Specifications are executable by a translation that assigns to every specification a model in the form of a core-Lπ program. We also illustrate the usefulness of this framework in reasoning about systems and their components.

KW - Semantics

KW - Models

KW - Bigraphical reactive

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

M3 - Conference contribution

AN - SCOPUS:84947723862

SN - 3540643028

SN - 9783540643029

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 42

EP - 56

BT - Programming Languages and Systems - 7th European Symposium on Programming, ESOP 1998 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 1998, Proceedings

A2 - Hankin, Chris

PB - Springer Verlag

T2 - 7th European Symposium on Programming, ESOP 1998 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 1998

Y2 - 28 March 1998 through 4 April 1998

ER -

Caires L , Monteiro L. Verifiable and executable logic specifications of concurrent objects in L_π. In Hankin C, editor, Programming Languages and Systems - 7th European Symposium on Programming, ESOP 1998 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 1998, Proceedings. Springer Verlag. 1998. p. 42-56. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).