Programming without refinement

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

doi:10.4204/EPTCS.282.4

Programming without refinement

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

Research output: Contribution to journal › Conference article › peer-review

1 Scopus citations

Abstract

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 language	English (US)
Pages (from-to)	39-52
Number of pages	14
Journal	Electronic Proceedings in Theoretical Computer Science, EPTCS
Volume	282
DOIs	https://doi.org/10.4204/EPTCS.282.4
State	Published - Oct 24 2018
Event	18th Refinement Workshop, Refine 2018 - Oxford, United Kingdom Duration: Jul 18 2018 → …

All Science Journal Classification (ASJC) codes

Software

Access to Document

10.4204/EPTCS.282.4

Cite this

@article{19c2dc13ae7742db956751ff8a74c65d,

title = "Programming without refinement",

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

author = "Marwa Benabdelali and Jilani, {Lamia Labed} and Wided Ghardallou and Ali Mili",

note = "Publisher Copyright: c M. Benabdelali, L. Labed Jilani, W. Ghardallou & A. Mili This work is licensed under the Creative Commons Attribution License.; 18th Refinement Workshop, Refine 2018 ; Conference date: 18-07-2018",

year = "2018",

month = oct,

day = "24",

doi = "10.4204/EPTCS.282.4",

language = "English (US)",

volume = "282",

pages = "39--52",

journal = "Electronic Proceedings in Theoretical Computer Science, EPTCS",

issn = "2075-2180",

publisher = "Open Publishing Association",

}

TY - JOUR

T1 - Programming without refinement

AU - Benabdelali, Marwa

AU - Jilani, Lamia Labed

AU - Ghardallou, Wided

AU - Mili, Ali

N1 - Publisher Copyright: c M. Benabdelali, L. Labed Jilani, W. Ghardallou & A. Mili This work is licensed under the Creative Commons Attribution License.

PY - 2018/10/24

Y1 - 2018/10/24

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=85060060122&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85060060122&partnerID=8YFLogxK

U2 - 10.4204/EPTCS.282.4

DO - 10.4204/EPTCS.282.4

M3 - Conference article

AN - SCOPUS:85060060122

SN - 2075-2180

VL - 282

SP - 39

EP - 52

JO - Electronic Proceedings in Theoretical Computer Science, EPTCS

JF - Electronic Proceedings in Theoretical Computer Science, EPTCS

T2 - 18th Refinement Workshop, Refine 2018

Y2 - 18 July 2018

ER -

Programming without refinement

Abstract

All Science Journal Classification (ASJC) codes

Access to Document

Other files and links

Fingerprint

Cite this