Automatic Refinement to Efficient Data Structures: A Comparison of Two Approaches
| Autor: | Peter Lammich, Andreas Lochbihler |
|---|---|
| Rok vydání: | 2018 |
| Předmět: |
Correctness
business.industry Computer science Programming language Proof assistant HOL 020207 software engineering Usability Context (language use) 0102 computer and information sciences 02 engineering and technology Data structure computer.software_genre 01 natural sciences Computational Theory and Mathematics 010201 computation theory & mathematics Artificial Intelligence 0202 electrical engineering electronic engineering information engineering Code (cryptography) Data refinement Algorithm verification Code generation business computer Software |
| Zdroj: | Journal of Automated Reasoning, 63 (1) |
| ISSN: | 1573-0670 0168-7433 |
| Popis: | We consider the problem of formally verifying an algorithm in a proof assistant and generating efficient code. Reasoning about correctness is best done at an abstract level, but efficiency of the generated code often requires complicated data structures. Data refinement has been successfully used to reconcile these conflicting requirements, but usability calls for automatic tool support. In the context of Isabelle/HOL, two frameworks for automating data refinement have been proposed (Lammich, in: Blazy, Paulin-Mohring, Pichardie (eds) ITP 2013, LNCS, vol 7998, Springer, Heidelberg, pp 84–99, 2013; Lochbihler, in: Blazy, Paulin-Mohring, Pichardie (eds) ITP 2013, LNCS, vol 7998, Springer, Heidelberg, pp 116–132, 2013). In this paper, we present and compare the two frameworks and their underlying ideas in depth. Thereby, we identify the challenges of automating data refinement, highlight the similarities and differences of the two approaches, and show their strengths and limitations both from the implementer’s and the user’s perspectives. A case study demonstrates how to combine both frameworks, benefiting from the strengths of each. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full text from SpringerLink