Verifiable and executable logic specifications of concurrent objects in Lπ

Research output: Chapter in Book/Report/Conference proceedingConference contribution

13 Citations (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 languageEnglish
Title of host publicationProgramming 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
EditorsChris Hankin
PublisherSpringer Verlag
Pages42-56
Number of pages15
ISBN (Print)3540643028, 9783540643029
Publication statusPublished - 1 Jan 1998
Event7th 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 19984 Apr 1998

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
PublisherSpringer Verlag
Volume1381
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference7th European Symposium on Programming, ESOP 1998 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 1998
CountryPortugal
CityLisbon
Period28/03/984/04/98

Keywords

  • Semantics
  • Models
  • Bigraphical reactive

Fingerprint Dive into the research topics of 'Verifiable and executable logic specifications of concurrent objects in L<sub>π</sub>'. Together they form a unique fingerprint.

Cite this