FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
Programming Without Refinement

Authors: Marwa Ben Abdelali, Lamia Labed Jilani, Wided Ghardallou and Ali Mili

Paper Information

Title:Programming Without Refinement
Authors:Marwa Ben Abdelali, Lamia Labed Jilani, Wided Ghardallou and Ali Mili
Proceedings:REFINE REFINE proceedings
Editors: Brijesh Dongol, John Derrick and Steve Reeves
Keywords:Relative Correctness, Absolute Correctness, Correctness Enhancement, Program Derivation, Program Projection, Deriving Reliable Programs
Abstract:

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 (i.e. proceeding from one executable program to another) until we achieve absolute correctness. Of course, this latter process is possible only if we know what it means to enhance correctness.

Pages:16
Talk:Jul 18 11:30 (Session 126J)
Paper: