Programming without refinement

Marwa Benabdelali, Lamia Labed Jilani, Wided Ghardallou, Ali Mili

Research output: Contribution to journalConference articlepeer-review

1 Scopus citations


To derive a program for a given specification R means to find an artifact P that satisfies two conditions: P is executable in some programming language; and P is correct with respect to R. Refinement-based program derivation achieves this goal in a stepwise manner by enhancing executability while preserving correctness until we achieve complete executability. In this paper, we argue that it is possible to invert these properties, and to derive a program by enhancing correctness while preserving executability (proceeding from one executable program to another) until we achieve absolute correctness. Of course, this latter process is possible only if we know how to enhance correctness.

Original languageEnglish (US)
Pages (from-to)39-52
Number of pages14
JournalElectronic Proceedings in Theoretical Computer Science, EPTCS
StatePublished - Oct 24 2018
Event18th Refinement Workshop, Refine 2018 - Oxford, United Kingdom
Duration: Jul 18 2018 → …

All Science Journal Classification (ASJC) codes

  • Software


Dive into the research topics of 'Programming without refinement'. Together they form a unique fingerprint.

Cite this