Derivation and Verification of Array Sorting by Merging, and its Certification in Dafny

Juan Pablo Carbonell, José E. Solsona, Nora Szasz +1

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…