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: [email protected].
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
SN - 0304-3975
VL - 149
SP - 333
EP - 360
JO - Theoretical Computer Science
JF - Theoretical Computer Science
IS - 2
ER -