{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,27]],"date-time":"2026-03-27T09:02:16Z","timestamp":1774602136487,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":51,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540605898","type":"print"},{"value":"9783540478027","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/bfb0015454","type":"book-chapter","created":{"date-parts":[[2005,11,13]],"date-time":"2005-11-13T06:32:11Z","timestamp":1131863531000},"page":"25-57","source":"Crossref","is-referenced-by-count":6,"title":["A method for the development of correct software"],"prefix":"10.1007","author":[{"given":"Peter","family":"Pepper","sequence":"first","affiliation":[]},{"given":"Martin","family":"Wirsing","sequence":"additional","affiliation":[]},{"given":"Ralph","family":"Betschko","sequence":"additional","affiliation":[]},{"given":"Manfred","family":"Broy","sequence":"additional","affiliation":[]},{"given":"Sabine","family":"Dick","sequence":"additional","affiliation":[]},{"given":"Klaus","family":"Didrich","sequence":"additional","affiliation":[]},{"given":"Joachim","family":"Faulhaber","sequence":"additional","affiliation":[]},{"given":"Wolfgang","family":"Grieskamp","sequence":"additional","affiliation":[]},{"given":"Heinrich","family":"Hu\u00dfmann","sequence":"additional","affiliation":[]},{"given":"Michael","family":"Mehlich","sequence":"additional","affiliation":[]},{"given":"Wolfgang","family":"Reif","sequence":"additional","affiliation":[]},{"given":"Martin","family":"Beyer","sequence":"additional","affiliation":[]},{"given":"Stefan","family":"Gastinger","sequence":"additional","affiliation":[]},{"given":"Maritta","family":"Heisel","sequence":"additional","affiliation":[]},{"given":"Friedrich","family":"von Henke","sequence":"additional","affiliation":[]},{"given":"Liu","family":"Junbo","sequence":"additional","affiliation":[]},{"given":"Bernd","family":"Krieg-Br\u00fcckner","sequence":"additional","affiliation":[]},{"given":"Thomas","family":"Santen","sequence":"additional","affiliation":[]},{"given":"Gerhard","family":"Schellhorn","sequence":"additional","affiliation":[]},{"given":"Oscar","family":"Slotosch","sequence":"additional","affiliation":[]},{"given":"Kurt","family":"Stenzel","sequence":"additional","affiliation":[]},{"given":"Martin","family":"Strecker","sequence":"additional","affiliation":[]},{"given":"Nikolas","family":"Vlachantonis","sequence":"additional","affiliation":[]},{"given":"Burkhart","family":"Wolff","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,9]]},"reference":[{"key":"2_CR1","unstructured":"Abdelwaheb Ayari, Stefan Friedrich, Ramses A. Heckler, and Jacques Loeckx. Das Fallbeispiel LEX. Working Paper WP92\/39, Universit\u00e4t Saarbr\u00fccken, Dezember 1992."},{"key":"2_CR2","unstructured":"C. Ashworth and M. Goodland. SSADM \u2014 A Practical Approach. McGraw Hill, 1990."},{"key":"2_CR3","unstructured":"Ralph Betschko, Sabine Dick, Klaus Didrich, and Wolfgang Grieskamp. Formal Development of an Efficient Implementation of a Lexical Scanner within the Korso methodology framework. Technical Report 93-30, TU Berlin, October 1993."},{"key":"2_CR4","doi-asserted-by":"crossref","unstructured":"F.L. Bauer, B. M\u00f6ller, H. Partsch, and P. Pepper. Formal Program Construction By Transformations-Computer-Aided, Intuition Guided Programming. Technische Universit\u00e4t M\u00fcnchen, 1988.","DOI":"10.1109\/32.21743"},{"key":"2_CR5","volume-title":"Software Reusability, volume 1 & 2","year":"1989","unstructured":"T.D. Biggerstaff and A.J. Perlis, editors. Software Reusability, volume 1 & 2. New York: ACM Press, 1989."},{"key":"2_CR6","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-61807-9","volume-title":"Algorithmic Language and Program Development","author":"F.L. Bauer","year":"1982","unstructured":"F.L. Bauer and H. W\u00f6ssner. Algorithmic Language and Program Development, Springer-Verlag, Berlin, 1982."},{"key":"2_CR7","unstructured":"M. Broy and M. Wirsing. Correct Software: From Experiments to Applications. in this volume."},{"key":"2_CR8","unstructured":"A. Camilleri, M. Gordon, and T. Melham. Hardware Verification Using Higher-Order Logic. In D. Borrione, editor, From HDL Descriptions to Guaranteed Correct Circuit Designs, North-Holland, pages 43\u201371, 1987."},{"key":"2_CR9","unstructured":"F. Cornelius, H. Hu\u00dfmann, and M. L\u00f6we. The Korso Case Study for Software Engineering with Formal Methods: A Medical Information System. in this volume."},{"key":"2_CR10","doi-asserted-by":"crossref","unstructured":"I. Cla\u00dfen, M. L\u00f6we, S. Wa\u00dferroth, and J. Wortmann. Static and dynamic semantics of entity-relationship models based on algebraic methods. In B. Wolfinger, editor, Innovationen bei Rechen-und Kommunikationssystemen, Informatik aktuell, pages 2\u20139. Springer-Verlag, 1994.","DOI":"10.1007\/978-3-642-51136-3_1"},{"key":"2_CR11","doi-asserted-by":"crossref","unstructured":"J. Darlington and R.M. Burstall. A System which automatically Improves Programs. ACTA Informatica, 6(1), 1973.","DOI":"10.1007\/BF00263742"},{"key":"2_CR12","first-page":"228","volume-title":"LNCS 782","author":"K. Didrich","year":"1994","unstructured":"Klaus Didrich, Andreas Fett, Carola Gerke, Wolfgang Grieskamp, and Peter Pepper. OPAL: Design and Implementation of an Algebraic Programming Language. In J\u00fcrg Gutknecht, editor, Programming Languages and System Architectures, International Conference, Zurich, Switzerland, March 1994, LNCS 782, pages 228\u2013244. Springer, 1994."},{"key":"2_CR13","unstructured":"E. Dubois, J. Hagelstein, E. Lahou, F. Ponsaert, A. Rifout, E. Stephens, and F. Williams. Model Components for Requirements Engineering. Final report, ESPRIT1 METEOR project, Task1, 1986."},{"key":"2_CR14","unstructured":"E. W. Dijkstra. A Discipline of Programming. Prentice-Hall, Inc., 1976."},{"key":"2_CR15","unstructured":"Axel Dold and Martin Strecker. Program development with specification operators \u2014 illustrated by a specification of the LEX scanner. Technical report, Universit\u00e4t Ulm, January 1993."},{"key":"2_CR16","volume-title":"EATCS Monographs on Theoretical Computer Science","author":"H. Ehrig","year":"1985","unstructured":"H. Ehrig and B. Mahr. Fundamentals of Algebraic Specifications 1: Equations and Initial Semantics, volume 6 of EATCS Monographs on Theoretical Computer Science. Springer-Verlag, Berlin, 1985."},{"key":"2_CR17","first-page":"748","volume-title":"LP: The Larch Prover","author":"S. J. Garland","year":"1988","unstructured":"S. J. Garland and J. V. Guttag. LP: The Larch Prover. In E. Lusk and R. Overbeek, editors, 9th International Conference on Automated Deduction (Argonne, Illinois), pages 748\u2013750. Springer Verlag, 1988."},{"issue":"1","key":"2_CR18","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1007\/BF00260922","volume":"10","author":"J. V. Guttag","year":"1978","unstructured":"J. V. Guttag and J. J. Horning. The Algebraic Specification of Abstract Data Types. ACTA Informatica, 10(1):27\u201352, 1978.","journal-title":"ACTA Informatica"},{"key":"2_CR19","first-page":"28","volume-title":"LCNS 552","author":"J. V. Guttag","year":"1991","unstructured":"J. V. Guttag and J. J. Horning. Introduction to LCL \u2014 A Larch\/C Interface Language. In S. Prehn, W. J. Toetenel, G. Goos, and J. Hartmanis, editors, VDM '91 Formal Software Development Methods 4th international Symp. (Noordwijerhout, Nov. 1991) LCNS 552, pages 28\u201378. Springer Verlag, 1991."},{"key":"2_CR20","unstructured":"S. Gastinger, R. Hennicker, and R. Stabl. Design of modular software systems with reuse. in this volume."},{"key":"2_CR21","first-page":"153","volume-title":"Formal Aspects of VLSI Design","author":"M. Gordon","year":"1986","unstructured":"M. Gordon. Why Higher-Order Logic is a good Formalism for Specifying and Verifying Hardware. In G. J. Milne and P. A. Subrahmanyam, editors, Formal Aspects of VLSI Design (Edinburgh Jan. 1985), pages 153\u2013179. North-Holland, 1986."},{"key":"2_CR22","doi-asserted-by":"crossref","unstructured":"D. Gries. The Science of Programming. Springer Verlag, 1981.","DOI":"10.1007\/978-1-4612-5983-1"},{"key":"2_CR23","volume-title":"LNCS 551","author":"J. V. Guttag","year":"1991","unstructured":"J. V. Guttag. The Larch Approach to Specification. In S. Prehn, W. J. Toetenel, G. Goos, and J. Hartmanis, editors, VDM '91 Formal Software Development Methods 4th Intern. Sympos. (Noordwijkerhout, Oct. 1991) LNCS 551. Springer Verlag, 1991."},{"key":"2_CR24","unstructured":"F.W. von Henke, J.S. Crow, R. Lee, J.M. Rushby, and R.A. Whitehurst. The EHDM verification environment: an overview. In 11th National Computer Security Conference, Baltimore, NBS\/NCSC, 1988."},{"key":"2_CR25","unstructured":"R. Hettler. Zur \u00dcbersetzung von E\/R-Schemata nach SPECTRUM. Technischer Bericht TUM-I9333, TU M\u00fcnchen, 1993."},{"key":"2_CR26","unstructured":"R. Hettler. A Requirement Specification for a Lexical Analyzer. Technical Report TUM-I9409, TU M\u00fcnchen, 1994."},{"key":"2_CR27","doi-asserted-by":"crossref","unstructured":"J. He, C. A. R. Hoare, and J.W.Sanders. Data Refinement refined. In G Goos and J. Hartmanis, editors, European Symposium on Programming, LNCS 213, pages 187\u2013196. ESOP 86, 1986.","DOI":"10.1007\/3-540-16442-1_14"},{"key":"2_CR28","unstructured":"C. A. R. Hoare. Developments in Concurrency and Communication. Addison-Wesley Publishing Company, 1990."},{"key":"2_CR29","unstructured":"H. Hu\u00dfmann. Zur formalen Beschreibung der funktionalen Anforderungen an ein Informationssystem. Technical Report TUMI-9332, Technische Universit\u00e4t M\u00fcnchen, 1993."},{"key":"2_CR30","doi-asserted-by":"crossref","unstructured":"H. Hu\u00dfmann. Formal foundations for pragmatic software engineering methods. In B. Wolfinger, editor, Innovationen bei Rechen-und Kommunikationssystemen, Informatik aktuell, pages 27\u201334. Springer-Verlag, 1994.","DOI":"10.1007\/978-3-642-51136-3_4"},{"key":"2_CR31","unstructured":"C. B. Jones. Systematic Software Development Using VDM. Prentice-Hall, 1986."},{"key":"2_CR32","doi-asserted-by":"crossref","first-page":"110","DOI":"10.1007\/3-540-17654-3_9","volume-title":"VDM '87 \u2014 VDM \u2014 A Formal Method at Work","author":"K. D. Jones","year":"1987","unstructured":"K. D. Jones. Support Environments for VDM. In D. Bjorner, C. B. Jones, M. Mac An Airchinnigh, and E. J. Neuhold, editors, VDM '87 \u2014 VDM \u2014 A Formal Method at Work (Bruessel March 1987), pages 110\u2013118. Springer Verlag, 1987."},{"key":"2_CR33","doi-asserted-by":"crossref","unstructured":"B. Krieg-Br\u00fcckner. Algebraic formalisation of program development by transformation. In H. Ganzinger, editor, European Symposium on Programming 1988, LNCS 300, pages 34\u201348. Springer, 1988.","DOI":"10.1007\/3-540-19027-9_3"},{"key":"2_CR34","unstructured":"L. J. Kolyang and B. Wolff. Transformational Development of the LEX Example. In B. Krieg-Br\u00fcckner, editor, Programmentwicklung durch Spezifikation und Transformation \u2014 Bremer Beitr\u00e4ge zum Verbundprojekt Korso, volume 2 of Informatik Bericht. Universit\u00e4t Bremen, 1994."},{"key":"2_CR35","doi-asserted-by":"crossref","unstructured":"C. Lewerentz and T. Lindner. Case Study Production Cell: A Comparative Study in Formal Specification and Verification. FZI Publication, FZI Karlsruhe, January 1994.","DOI":"10.1007\/3-540-58867-1_47"},{"key":"2_CR36","unstructured":"E. Mayger, B. Harris, S. Fin, M. Fourman, and M. Francis. Version 4.2 LAMBDA documentation. Technical report, Abstract Hardware Limited, 1992."},{"issue":"3","key":"2_CR37","first-page":"199","volume":"27","author":"Z. Manna","year":"1979","unstructured":"Z. Manna and R. Waldinger. The Logic of Computer Programming. IEEE Transactions on Computers, 27(3):199\u2013229, 1979.","journal-title":"IEEE Transactions on Computers"},{"key":"2_CR38","doi-asserted-by":"crossref","unstructured":"F. Nicki. Ablaufspezifikation durch Datenflu\u00dfdiagramme und Axiome. In B. Wolfinger, editor, Innovationen bei Rechen-und Kommunikationssystemen, Informatik aktuell, pages 10\u201318. Springer-Verlag, 1994.","DOI":"10.1007\/978-3-642-51136-3_2"},{"key":"2_CR39","doi-asserted-by":"crossref","unstructured":"Tobias Nipkow and Lawrence C. Paulson. Isabelle-91. In Deepak Kapur, editor, Proc. 11th Int. Conf. Automated Deduction, pages 673\u2013676. LNCS 607, 1992.","DOI":"10.1007\/3-540-55602-8_201"},{"key":"2_CR40","unstructured":"E. R. Olderog, S. R\u00f6ssig, V. Sander, and M. Schenke. ProCoS at Oldenburg: The Interface between Specification Language and occam-like Programming Language. Technical Report 3\/92, Universit\u00e4t Oldenburg, 1992."},{"key":"2_CR41","doi-asserted-by":"crossref","unstructured":"R. Paige. Transformational programming \u2014 applications to algorithms and systems. In 10th ACM POPL Symposium, Austin, Texas, 1983.","DOI":"10.1145\/567067.567076"},{"key":"2_CR42","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-61512-2","volume-title":"Specification and Transformation of Programs \u2014 A Formal Approach to Software Development","author":"H. Partsch","year":"1990","unstructured":"H. Partsch. Specification and Transformation of Programs \u2014 A Formal Approach to Software Development. Springer-Verlag, Berlin, 1990."},{"key":"2_CR43","doi-asserted-by":"crossref","unstructured":"L. C. Paulson. Logic and Computation: Interactive Proof with Cambridge LCF. Computing Reviews, 1987.","DOI":"10.1017\/CBO9780511526602"},{"key":"2_CR44","unstructured":"P. Pepper, R. Betschko, S. Dick, and K. Didrich. Realizing Sets by Hash Tables. in this volume."},{"key":"2_CR45","unstructured":"W. Reif. The KIV-Approach to Software Verification. in this volume."},{"key":"2_CR46","volume-title":"LNCS 761","author":"W. Reif","year":"1993","unstructured":"W. Reif and K. Stenzel. Reuse of Proofs in Software Verification. In Shyamasundar, editor, Conference on Foundations of Software Technology and Theoretical Computer Science, LNCS 761, Bombay, India, 1993. Springer."},{"key":"2_CR47","unstructured":"Wolfgang Reif, Gerhard Schellhorn, and Kurt Stenzel. Developing a verified lexical scanner \u2014 a methodological case-study with the KIV System. Technical report, Universit\u00e4t Karlsruhe, 1993."},{"key":"2_CR48","unstructured":"D. R. Smith. KIDS A Knowledge-Based Software Development System. In M. R. Lowry and R. D. McCartney, editors, Automating Software Design, pages 483\u2013514, 1991."},{"key":"2_CR49","volume-title":"Software Engineering","author":"I. Sommerville","year":"1992","unstructured":"I. Sommerville. Software Engineering. Addison-Wesley, Mass., 3rd edition, 1992.","edition":"3rd edition"},{"key":"2_CR50","unstructured":"N. Wirth. Algorithmen und Datenstrukturen. Teubner, 1983."},{"key":"2_CR51","volume-title":"Handbook of Theoretical Computer Science","author":"M. Wirsing","year":"1990","unstructured":"Martin Wirsing. Algebraic Specification. In J. van Leeuven, editor, Handbook of Theoretical Computer Science, Amsterdam, 1990. North-Holland."}],"container-title":["Lecture Notes in Computer Science","KORSO: Methods, Languages, and Tools for the Construction of Correct Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0015454","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,10]],"date-time":"2020-04-10T20:48:20Z","timestamp":1586551700000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0015454"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540605898","9783540478027"],"references-count":51,"URL":"https:\/\/doi.org\/10.1007\/bfb0015454","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1995]]}}}