Formal Verification of Recursive Predicates
Richard Bubel · Repository KITopen (Karlsruhe Institute of Technology) · 2007
data types are a well-known and explored area in computer sciences. Of interest for this section are generated abstract data types as they enable reasoning by structural induction. Generated abstract data types are axiomatised with help of a set of function symbols. A selected subset of them is marked as constructors. Their semantics is that all elements of the abstract datatype can be written as ground terms consisting only of constructors. In particular any element of the domain has a syntactical representation. The remaining functions can be divided into observers, which do not manipulate the structure, and operations mapping an ADT element to another one. The semantics of the queries and operations is usually given in terms of a rewrite system and/or general axioms in a (fragment) sorted first order logic. Some characteristics of the algebraic data type are strongly tied to the allowed rewrite system resp. logic. Abstract data types are a useful tool to model linked data structures. To some extend they allow to (re-)use methodologies invented for their analysis for verifying object-oriented programs. 5.1.1 Abstraction of Linked Data Structures This section demonstrates how to abstract a linked data structure using abstract data types. The found abstraction can then be used instead of the linked data structure itself when verifying programs using the data structure. An elaborated example is given in Sect. 6 modelling the JAVA String data type in KeY. An abstract data type is traditionally described using an algebraic specification. An algebraic specification defines a signature algebra consisting at least of • a set of sorts (sort names) TADT with one distinguished S ∈ TADT often called the sort or type of interest. • a set of functions FADT • a set of axioms AxADT The intent of the axioms set is to give the functions a meaning. The axioms are usually given as (conditional) equations. The concrete used framework is