Preservation and reflection in specification

Antónia Lopes, José Luiz Fiadeiro

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

7 Citations (Scopus)


We extend the traditional notion of specification based on theories and interpretations between theories to model situations, typical of open, reactive systems, in which properties exhibited locally by an object no longer hold when that object is interconnected as a component of a larger system. The proposed notion of specification is based on the observation, due to Winskel, that while some assertions are preserved across morphisms of labelled transition systems, other are reflected. The distinction between these two classes of assertions leads us to the definition of two categories of specifications, one that supports horizontal structuring and another that supports vertical structuring, for which compositionality is proved.
Original languageEnglish
Title of host publicationAMAST 1997
Subtitle of host publicationAlgebraic Methodology and Software Technology
EditorsM. Johnson
Place of PublicationBerlin
PublisherSpringer Verlag
Number of pages15
ISBN (Electronic)9783540696612
ISBN (Print)9783540638889
Publication statusPublished - 1997
EventAMAST '97: Algebraic Methodology and Software Technology.: 6th International Conference - Sydney, Australia
Duration: 12 Dec 199717 Dec 1997

Publication series

Name Lecture Notes in Computer Science


ConferenceAMAST '97: Algebraic Methodology and Software Technology.


  • Temporal Logic
  • Label Transition System
  • State Proposition
  • Synchronisation Point
  • Local Logic


Dive into the research topics of 'Preservation and reflection in specification'. Together they form a unique fingerprint.

Cite this