Sciweavers

ATVA
2008
Springer

Automating Algebraic Specifications of Non-freely Generated Data Types

13 years 5 months ago
Automating Algebraic Specifications of Non-freely Generated Data Types
Abstract. Non-freely generated data types are widely used in case studies carried out in the theorem prover KIV. The most common examples are stores, sets and arrays. We present an automatic method that generates finite counterexamples for wrong conjectures and therewith offers a valuable support for proof engineers saving their time otherwise spent on unsuccessful proof attempts. The approach is based on the finite model finding and uses Alloy Analyzer [1] to generate finite instances of theories in KIV [6]. Most definitions of functions or predicates on infinite structures do not preserve the semantics if a transition to arbitrary finite substructures is made. We propose the constraints which should be satisfied by the finite substructures, identify a class of amenable definitions and present a practical realization using Alloy. The technique is evaluated on the library of basic data types as well as on some examples from case studies in KIV.
Andriy Dunets, Gerhard Schellhorn, Wolfgang Reif
Added 12 Oct 2010
Updated 12 Oct 2010
Type Conference
Year 2008
Where ATVA
Authors Andriy Dunets, Gerhard Schellhorn, Wolfgang Reif
Comments (0)