Sorting Without Sorts

EasyChair Preprint no. 10632, version 2

Abstract

We present an integrated formal methods framework in support of automatically establishing the functional correctness of programs with recursive data structures, including functional programs implementing sorting algorithms. We formalize program semantics in many-sorted first order logic while introducing sortedness/permutation properties as part of our first-order formalization.

Rather than focusing on specific first-order theories such as lists of integer arithmetic, our formalization relies on a parameterized sort abstracting (arithmetic) theories. We further adjust recent efforts for automating inductive reasoning in saturation-based first-order theorem proving. Importantly, we advocate a compositional reasoning approach for fully automating the verification of functional programs implementing and preserving sorting and permutation properties over parameterized list structures.

We showcase the applicability of our framework over recursive sorting algorithms, including Mergesort and Quicksort; to this end, we turn first-order theorem proving into a fully automated verification engine to discharge verification conditions, without requiring manually proven and/or a priori given loop invariants.

Keyphrases: automated software verification, automated theorem proving, automating induction, first-order theorem proving, function calls, induction in first-order logic, software correctness, sorting algorithms, superposition-based theorem proving

@Booklet{EasyChair:10632,
  author = {Pamina Georgiou and Marton Hajdu and Laura Kovacs},
  title = {Sorting Without Sorts},
  howpublished = {EasyChair Preprint no. 10632},

  year = {EasyChair, 2023}}