Programming Without Refining

Marwa Benabdelali
(ISG Management Institute Bardo, Tunisia)
Lamia Labed Jilani
(ISG Management Institute Bardo, Tunisia)
Wided Ghardallou
(University of Kairouan Kairouan, Tunisia)
Ali Mili
(New Jersey Institute of Technology Newark, NJ, USA)

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.

In John Derrick, Brijesh Dongol and Steve Reeves: Proceedings 18th Refinement Workshop (Refine 2018), Oxford, UK, 18th July 2018, Electronic Proceedings in Theoretical Computer Science 282, pp. 39–52.
Published: 24th October 2018.

ArXived at: http://dx.doi.org/10.4204/EPTCS.282.4 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org