AVL Trees Revisited: A Case Study in SPECTRUM

The goal of this paper is to present a way of developing software within the axiomatic specification language SPECTRUM. We advocate a development approach which is organized in four stages: requirement specification, design specification, executable specification and functional program. The concept of AVL trees serves as example for presenting this approach.

Specification, development, method, refinement, verification

@techreport{HNRS94,
author = {R. Hettler and D. Nazareth and F. Regensburger and O. Slotosch},
institution = {Technische Universit{\"a}t M{\"u}nchen. Institut f{\"u}r Informatik},
number = {TUM-I9428},
title = {{AVL} Trees Revisited: A Case Study in {{\sc{}Spectrum}}},
year = {1994},
uri = {"http://www4.informatik.tu-muenchen.de/proj/korso/papers/avl.html" }
}
also in
@BOOK{KORSO-LNCS,
        EDITOR  = {Manfred Broy and Stefan J\"ahnichen},
        TITLE   = {{KORSO}: {M}ethods, {L}anguages, and {T}ools for the
                {C}onstruction of {C}orrect {S}oftware -- {F}inal {R}eport},
        ADDRESS = {Heidelberg},
        PUBLISHER       = {Springer},
        SERIES  = {LNCS},
        VOLUME  = {1009},
        MONTH   = {Nov},
        YEAR    = {1995}
        }