Implementing the Change of Data Structures with SPECTRUM in the Framework of KORSO Development Graphs

Technical Report TUM-I9511

Author

Abstract

Data structures are algebraically specified with abstract data types in the specification language SPECTRUM. Structures of specifications are depicted in the Development-Graphs like in the BMFT-Project: KORSO. These graphs contain refinement relations, which have to be proved.

In this paper a general method for changing data structures is demonstrated on the example of sets and sequences. The focus lays on proving the involved refinement relations with the theorem prover Isabelle. A simple method is given to support such proofs.

CR classification

D.2.4, F.3.1, F.3.2, G.4

General Keywords of CR classification

Algorithms, Reliability, Theory, Verification

Keywords:

Abstract data types, specification, refinement, quotient, subtype, verification, proof

@TechReport{Slo95,
  author =       "Oscar Slotosch",
  title =        "Implementing the {C}hange of {D}ata {S}tructures with {{\sc {S}pectrum}} in the {F}ramework of {{\sc {K}or{S}o}} {D}evelopment {G}raphs",
  institution =  {Technische Universit{\"a}t M{\"u}nchen. Institut f{\"u}r Informatik},
  year =         "1995",
  number =       {TUM-I9511},
  uri       = {"http://www4.informatik.tu-muenchen.de/proj/korso/papers/dsw.html"}
}