Name
Abstract | ||
|---|---|---|
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. |
Year | DOI | Venue |
|---|---|---|
2010 | 10.1007/978-3-642-14052-5_20 | ITP |
Keywords | Field | DocType |
powerlist case study,total operation,generalized coverset induction scheme,coverset induction,formal logic,coverset induction method,partial constructor,maude itp,membership equational logic,induction scheme,partial operation,data structure,parallel algorithm,theorem prover,divide and conquer | Algebraic number,Programming language,Computer science,Theoretical computer science,Divide and conquer algorithms,Recursive functions,Recursion,Theorem provers,Discrete mathematics,Data structure,Parallel algorithm,Algorithm,Equational logic | Conference |
ISBN | Citations | PageRank |
3-642-14051-3 | 3 | 0.38 |
References | Authors | |
18 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Joe Hendrix | 1 | 98 | 5.71 |
| Deepak Kapur | 2 | 2282 | 235.00 |
| José Meseguer | 3 | 9533 | 805.39 |