TY - JOUR

T1 - Embedding a demonic semilattice in a relation algebra

AU - Desharnais, Jules

AU - Belkhiter, Nadir

AU - Sghaier, Salah Ben Mohamed

AU - Tchier, Fairouz

AU - Jaoua, Ali

AU - Mili, Ali

AU - Zaguia, Nejib

N1 - Funding Information:
*This research is supported by grants from FCAR (Qutbec), NSERC (Canada), Mink&e de I’Enseigne-ment Suptrieur et de la Science (Qukbec), Faculty of Sciences and School of Graduate Studies and Research (University of Ottawa) and Fondation de la Recherche Scientifique (Tunis). *Corresponding author. E-mail: Jules.Desharnais@ift.ulaval.ca.

PY - 1995/10/2

Y1 - 1995/10/2

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

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

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

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

U2 - 10.1016/0304-3975(94)00271-J

DO - 10.1016/0304-3975(94)00271-J

M3 - Article

AN - SCOPUS:0001108878

VL - 149

SP - 333

EP - 360

JO - Theoretical Computer Science

JF - Theoretical Computer Science

SN - 0304-3975

IS - 2

ER -