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 be prov 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.     «

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 be prov 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 metho...     »