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)
TL;DR
This paper proposes a novel approach to program derivation by focusing on improving correctness first and then ensuring executability, offering an alternative to traditional refinement methods.
Contribution
It introduces the concept of deriving programs through correctness enhancement while maintaining executability, reversing the traditional refinement process.
Findings
Demonstrates the feasibility of correctness-first program derivation
Provides a theoretical framework for correctness enhancement
Suggests new directions for program synthesis methods
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.