skip to main content
research-article

Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant

Published: 14 January 2015 Publication History

Abstract

We present Fiat, a library for the Coq proof assistant supporting refinement of declarative specifications into efficient functional programs with a high degree of automation. Each refinement process leaves a proof trail, checkable by the normal Coq kernel, justifying its soundness. We focus on the synthesis of abstract data types that package methods with private data. We demonstrate the utility of our framework by applying it to the synthesis of query structures -- abstract data types with SQL-like query and insert operations. Fiat includes a library for writing specifications of query structures in SQL-inspired notation, expressing operations over relations (tables) in terms of mathematical sets. This library includes a suite of tactics for automating the refinement of specifications into efficient, correct-by-construction OCaml code. Using these tactics, a programmer can generate such an implementation completely automatically by only specifying the equivalent of SQL indexes, data structures capturing useful views of the abstract data. Throughout we speculate on the new programming modularity possibilities enabled by an automated refinement system with proved-correct rules.

Supplementary Material

MPG File (p689-sidebyside.mpg)

References

[1]
Don Batory, Vivek Singhal, Marty Sirkin, and Jeff Thomas. Scalable software libraries. In Proceedings of the 1st ACM SIGSOFT Symposium on Foundations of Software Engineering. ACM, 1993.
[2]
Lee Blaine and Allen Goldberg. DTRE -- a semi-automatic transformation system. In Constructing Programs from Specifications, pages 165--204. Elsevier, 1991.
[3]
Peter Buneman, Leonid Libkin, Dan Suciu, Val Tannen, and Limsoon Wong. Comprehension syntax. SIGMOD Rec., 23(1), March 1994.
[4]
Swarat Chaudhuri, Martin Clochard, and Armando Solar-Lezama. Bridging boolean and quantitative synthesis using smoothed proof search. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM, 2014.
[5]
Cyril Cohen, Maxime Dénès, and Anders Mörtberg. Refinements for free! In Certified Programs and Proofs. Springer International Publishing, 2013.
[6]
http://coq.inria.fr/distrib/current/refman/Reference-Manual029.html.
[7]
Edsger W. Dijkstra. A constructive approach to the problem of program correctness. Circulated privately, August 1967.
[8]
Peter Hawkins, Alex Aiken, Kathleen Fisher, Martin Rinard, and Mooly Sagiv. Data representation synthesis. In Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM, 2011.
[9]
J. He, C.A.R. Hoare, and J.W. Sanders. Data refinement refined. In Bernard Robinet and Reinhard Wilhelm, editors, ESOP 86, volume 213 of Lecture Notes in Computer Science, pages 187--196. Springer Berlin Heidelberg, 1986.
[10]
C.A.R. Hoare. Proof of correctness of data representations. Acta Informatica, 1(4):271--281, 1972.
[11]
Barbara Liskov and Stephen Zilles. Programming with abstract data types. In Symposium on Very High Level Languages, New York, NY, USA, 1974. ACM.
[12]
Robert Paige and Fritz Henglein. Mechanical translation of set theoretic problem specifications into efficient RAM code -- a case study. J. Symb. Comput., 4(2):207--232, October 1987.
[13]
Robert Paige and Shaye Koenig. Finite differencing of computable expressions. ACM Trans. Program. Lang. Syst., 4(3), July 1982.
[14]
Dusko Pavlovic, Peter Pepper, and Douglas R. Smith. Formal derivation of concurrent garbage collectors. In Mathematics of Program Construction, pages 353--376. Springer Berlin Heidelberg, 2010.
[15]
Rishabh Singh and Armando Solar-Lezama. Synthesizing data structure manipulations from storyboards. In Proceedings of the 19th ACM SIGSOFT Symposium and the 13th European Conference on Foundations of Software Engineering. ACM, 2011.
[16]
Douglas R. Smith. KIDS: A semi-automatic program development system. In Client Resources on the Internet, IEEE Multimedia Systems'99, pages 302--307, 1990.
[17]
Douglas R. Smith and Stephen J. Westfold. Synthesis of propositional satisfiability solvers, 2008.
[18]
Armando Solar-Lezama. Program Synthesis by Sketching. PhD thesis, University of California, Berkeley, 2008.
[19]
Armando Solar-Lezama, Christopher Grant Jones, and Rastislav Bodik. Sketching concurrent data structures. In Proceedings of the 2008 ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM, 2008.
[20]
http://www.kestrel.edu/home/prototypes/specware.html.
[21]
Philip Wadler. Comprehending monads. In Mathematical Structures in Computer Science, pages 61--78, 1992.

Cited By

View all
  • (2024)UTC Time, Formally VerifiedProceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3636501.3636958(2-13)Online publication date: 9-Jan-2024
  • (2024)Symbolic metaprogram search improves learning efficiency and explains rule learning in humansNature Communications10.1038/s41467-024-50966-x15:1Online publication date: 10-Aug-2024
  • (2021)Cyclic program synthesisProceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3453483.3454087(944-959)Online publication date: 19-Jun-2021
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices
ACM SIGPLAN Notices  Volume 50, Issue 1
POPL '15
January 2015
682 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/2775051
  • Editor:
  • Andy Gill
Issue’s Table of Contents
  • cover image ACM Conferences
    POPL '15: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
    January 2015
    716 pages
    ISBN:9781450333009
    DOI:10.1145/2676726
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 14 January 2015
Published in SIGPLAN Volume 50, Issue 1

Check for updates

Author Tags

  1. deductive synthesis
  2. mechanized derivation of abstract data types

Qualifiers

  • Research-article

Funding Sources

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)62
  • Downloads (Last 6 weeks)4
Reflects downloads up to 19 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2024)UTC Time, Formally VerifiedProceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3636501.3636958(2-13)Online publication date: 9-Jan-2024
  • (2024)Symbolic metaprogram search improves learning efficiency and explains rule learning in humansNature Communications10.1038/s41467-024-50966-x15:1Online publication date: 10-Aug-2024
  • (2021)Cyclic program synthesisProceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3453483.3454087(944-959)Online publication date: 19-Jun-2021
  • (2020)Concise Read-Only Specifications for Better Synthesis of Programs with PointersProgramming Languages and Systems10.1007/978-3-030-44914-8_6(141-168)Online publication date: 27-Apr-2020
  • (2019)Refinement to Imperative HOLJournal of Automated Reasoning10.1007/s10817-017-9437-162:4(481-503)Online publication date: 1-Apr-2019
  • (2018)Correct-by-Construction Implementation of Runtime Monitors Using Stepwise RefinementDependable Software Engineering. Theories, Tools, and Applications10.1007/978-3-319-99933-3_3(31-49)Online publication date: 26-Aug-2018
  • (2018)A Coq Formalisation of SQL’s Execution EnginesInteractive Theorem Proving10.1007/978-3-319-94821-8_6(88-107)Online publication date: 4-Jul-2018
  • (2016)Extensible and Efficient Automation Through Reflective TacticsProgramming Languages and Systems10.1007/978-3-662-49498-1_21(532-559)Online publication date: 2016
  • (2016)Proof–Based Synthesis of Sorting Algorithms for TreesLanguage and Automata Theory and Applications10.1007/978-3-319-30000-9_43(562-575)Online publication date: 26-Feb-2016
  • (2016)From Sets to Bits in CoqFunctional and Logic Programming10.1007/978-3-319-29604-3_2(12-28)Online publication date: 21-Feb-2016
  • Show More Cited By

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media