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

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...     »