TY - JOUR
T1 - Projecting programs on specifications
T2 - Definition and implications
AU - Desharnais, Jules
AU - Diallo, Nafi
AU - Ghardallou, Wided
AU - Mili, Ali
N1 - Publisher Copyright:
© 2017 Elsevier B.V.
PY - 2017/5/1
Y1 - 2017/5/1
N2 - Given a specification R, it is common for a candidate program P to be doing more than R requires; this is not necessarily bad, and is often unavoidable, due to programming language constraints or to otherwise sensible design decisions. In this paper, we introduce a relational operator that captures, for a given specification R and candidate program P, the functionality delivered by P that is relevant to R. This operator, which we call the projection of P over R (for reasons we explain), has a number of interesting properties, which we explore in this paper.
AB - Given a specification R, it is common for a candidate program P to be doing more than R requires; this is not necessarily bad, and is often unavoidable, due to programming language constraints or to otherwise sensible design decisions. In this paper, we introduce a relational operator that captures, for a given specification R and candidate program P, the functionality delivered by P that is relevant to R. This operator, which we call the projection of P over R (for reasons we explain), has a number of interesting properties, which we explore in this paper.
KW - Absolute correctness
KW - Lattices
KW - Projection
KW - Refinement
KW - Relative correctness
UR - http://www.scopus.com/inward/record.url?scp=85011912130&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85011912130&partnerID=8YFLogxK
U2 - 10.1016/j.scico.2016.11.006
DO - 10.1016/j.scico.2016.11.006
M3 - Article
AN - SCOPUS:85011912130
SN - 0167-6423
VL - 138
SP - 26
EP - 48
JO - Science of Computer Programming
JF - Science of Computer Programming
ER -