Projecting programs on specifications: Definition and implications

Jules Desharnais; Nafi Diallo; Wided Ghardallou; Ali Mili

doi:10.1016/j.scico.2016.11.006

Projecting programs on specifications: Definition and implications

Jules Desharnais, Nafi Diallo, Wided Ghardallou, Ali Mili

Research output: Contribution to journal › Article › peer-review

3 Scopus citations

Abstract

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.

Original language	English (US)
Pages (from-to)	26-48
Number of pages	23
Journal	Science of Computer Programming
Volume	138
DOIs	https://doi.org/10.1016/j.scico.2016.11.006
State	Published - May 1 2017

All Science Journal Classification (ASJC) codes

Software
Information Systems
Modeling and Simulation
Computational Theory and Mathematics

Keywords

Absolute correctness
Lattices
Projection
Refinement
Relative correctness

Access to Document

10.1016/j.scico.2016.11.006

Cite this

@article{197ee68c7f934c62bdd3f4082ccd91e5,

title = "Projecting programs on specifications: Definition and implications",

abstract = "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.",

keywords = "Absolute correctness, Lattices, Projection, Refinement, Relative correctness",

author = "Jules Desharnais and Nafi Diallo and Wided Ghardallou and Ali Mili",

note = "Publisher Copyright: {\textcopyright} 2017 Elsevier B.V.",

year = "2017",

month = may,

day = "1",

doi = "10.1016/j.scico.2016.11.006",

language = "English (US)",

volume = "138",

pages = "26--48",

journal = "Science of Computer Programming",

issn = "0167-6423",

publisher = "Elsevier",

}

TY - JOUR

T1 - Projecting programs on specifications

T2 - Definition and implications

AU - Desharnais, Jules

AU - Diallo, Nafi

AU - Ghardallou, Wided

AU - Mili, Ali

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 -

Projecting programs on specifications: Definition and implications

Abstract

All Science Journal Classification (ASJC) codes

Keywords

Access to Document

Other files and links

Fingerprint

Cite this