Implementing the Change of Data Structures with SPECTRUM in the Framework of KORSO Development Graphs
Oscar Slotosch · 1995
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."