Projecting programs on specifications: Definition and implications

Jules Desharnais, Nafi Diallo, Wided Ghardallou, Ali Mili

Research output: Contribution to journalArticlepeer-review

2 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 languageEnglish (US)
Pages (from-to)26-48
Number of pages23
JournalScience of Computer Programming
Volume138
DOIs
StatePublished - May 1 2017

All Science Journal Classification (ASJC) codes

  • Software

Keywords

  • Absolute correctness
  • Lattices
  • Projection
  • Refinement
  • Relative correctness

Fingerprint Dive into the research topics of 'Projecting programs on specifications: Definition and implications'. Together they form a unique fingerprint.

Cite this