Derivation and Verification of Array Sorting by Merging, and its Certification in Dafny
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2025
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866911133410000896 |
|---|---|
| author | Carbonell, Juan Pablo Solsona, José E. Szasz, Nora Tasistro, Álvaro |
| author_facet | Carbonell, Juan Pablo Solsona, José E. Szasz, Nora Tasistro, Álvaro |
| contents | We provide full certifications of two versions of merge sort of arrays in the verification-aware programming language Dafny. We start by considering schemas for applying the divide-and-conquer or partition method of solution to specifications given by pre- and post-conditions involving linear arrays. We then derive the merge sort and merging algorithms as instances of these schemas, thereby arriving at a fully recursive formulation. Further, the analysis of the tree of subproblems arising from the partition facilitates the design of loop invariants that allow to derive a fully iterative version (sometimes called bottom-up merge sort) that does not employ a stack. We show how the use of the provided schemas conveniently conducts the formalization and actual verification in Dafny. The whole method is also applicable to deriving variants of quicksort, which we sketch. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2509_01758 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Derivation and Verification of Array Sorting by Merging, and its Certification in Dafny Carbonell, Juan Pablo Solsona, José E. Szasz, Nora Tasistro, Álvaro Logic in Computer Science Data Structures and Algorithms We provide full certifications of two versions of merge sort of arrays in the verification-aware programming language Dafny. We start by considering schemas for applying the divide-and-conquer or partition method of solution to specifications given by pre- and post-conditions involving linear arrays. We then derive the merge sort and merging algorithms as instances of these schemas, thereby arriving at a fully recursive formulation. Further, the analysis of the tree of subproblems arising from the partition facilitates the design of loop invariants that allow to derive a fully iterative version (sometimes called bottom-up merge sort) that does not employ a stack. We show how the use of the provided schemas conveniently conducts the formalization and actual verification in Dafny. The whole method is also applicable to deriving variants of quicksort, which we sketch. |
| title | Derivation and Verification of Array Sorting by Merging, and its Certification in Dafny |
| topic | Logic in Computer Science Data Structures and Algorithms |
| url | https://arxiv.org/abs/2509.01758 |