Decision procedures for algebraic data types with abstractions
| Autor: | DottaMirco, SuterPhilippe, KuncakViktor |
|---|---|
| Rok vydání: | 2010 |
| Předmět: |
Catamorphism
Correctness Computer science 0102 computer and information sciences 02 engineering and technology Lambda computer.software_genre 01 natural sciences Data type Term algebra Boolean algebra symbols.namesake 0202 electrical engineering electronic engineering information engineering Abstraction Multiset Recursion Programming language Verification 020207 software engineering Multiplicity (mathematics) Data structure Computer Graphics and Computer-Aided Design Term (time) Decidability Algebra Type theory 010201 computation theory & mathematics Constraints Free variables and bound variables Languages symbols Algebraic data type 020201 artificial intelligence & image processing Homomorphism Abstract syntax tree computer Boolean data type Software Algorithms |
| Zdroj: | POPL |
| DOI: | 10.1145/1706299.1706325 |
| Popis: | We describe a family of decision procedures that extend the decision procedure for quantifier-free constraints on recursive algebraic data types (term algebras) to support recursive abstraction functions. Our abstraction functions are catamorphisms (term algebra homomorphisms) mapping algebraic data type values into values in other decidable theories (e.g. sets, multisets, lists, integers, booleans). Each instance of our decision procedure family is sound; we identify a widely applicable many-to-one condition on abstraction functions that implies the completeness. Complete instances of our decision procedure include the following correctness statements: 1) a functional data structure implementation satisfies a recursively specified invariant, 2) such data structure conforms to a contract given in terms of sets, multisets, lists, sizes, or heights, 3) a transformation of a formula (or lambda term) abstract syntax tree changes the set of free variables in the specified way. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|