Embedding a demonic semilattice in a relation algebra

Jules Desharnais, Nadir Belkhiter, Salah Ben Mohamed Sghaier, Fairouz Tchier, Ali Jaoua, Ali Mili, Nejib Zaguia

Research output: Contribution to journalArticlepeer-review

40 Scopus citations

Abstract

We present a refinement ordering between binary relations, viewed as programs or specifications. This ordering induces a complete join semilattice that can be embedded in a relation algebra. This embedding then allows an easy proof of many properties of the refinement semilattice, by making use of the well-known corresponding properties of relation algebras. The operations of the refinement semilattice corresponding to join and composition in the embedding algebra are, respectively, demonic join and demonic composition. The weakest prespecification and postspecification operators of Hoare and He, defined over a relation algebra, also have corresponding operators in the semilattice.

Original languageEnglish (US)
Pages (from-to)333-360
Number of pages28
JournalTheoretical Computer Science
Volume149
Issue number2
DOIs
StatePublished - Oct 2 1995
Externally publishedYes

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Embedding a demonic semilattice in a relation algebra'. Together they form a unique fingerprint.

Cite this