Coverset induction with partiality and subsorts: A powerlist case study

Many inductive theorem provers generate induction schemes from the recursive calls appearing in terminating functions defined recursively in the specification. This strategy is called coverset induction in the context of algebraic specifications, and has been shown to be quite useful in a wide variety of applications. One challenge is that coverset induction typically requires using a total recursive function, while many operations are only meaningful on a subset of their inputs. A generalization of coverset induction method that supports partial constructors and operations specified in membership equational logic is proposed. The generalization has been implemented in the Maude ITP, and used to perform an extensive case study involving powerlists - a data structure introduced by J. Misra to elegantly formalize parallel algorithms based on divide and conquer strategy. Powerlists are constructed by partial operations, and it has been a challenge to naturally reason about powerlists using a formal logic that only supports total operations. We show how theorems about powerlists can be elegantly proven using the generalized coverset induction scheme implemented in the Maude ITP.