Verification of Object-Oriented Software. The KeY Approach Foreword
Long gone are the days when program veri?cation was a task carried out merely by hand with paper and pen. For one, we are increasingly interested in proving actual program artifacts, not just abstractions thereof or core algorithms. The programs we want t
- PDF / 7,165,550 Bytes
- 669 Pages / 430 x 660 pts Page_size
- 106 Downloads / 211 Views
Subseries of Lecture Notes in Computer Science
4334
Bernhard Beckert Reiner Hähnle Peter H. Schmitt (Eds.)
Verification of Object-Oriented Software The KeY Approach Foreword by K. Rustan M. Leino
13
Series Editors Jaime G. Carbonell, Carnegie Mellon University, Pittsburgh, PA, USA Jörg Siekmann, University of Saarland, Saarbrücken, Germany Volume Editors Bernhard Beckert University of Koblenz Department of Computer Science, AI Research Group Universitätsstr. 1, 56070 Koblenz, Germany E-mail: [email protected] Reiner Hähnle Chalmers University of Technology Department Computer Science and Engineering 41296 Göteborg, Sweden E-mail: [email protected] Peter H. Schmitt Universität Karlsruhe Institut für Theoretische Informatik Am Fasanengarten 5, 76131 Karlsruhe, Germany E-mail: [email protected]
Library of Congress Control Number: 2006939067
CR Subject Classification (1998): I.2.2, I.2, D.2.4, F.3.1, F.4.1 LNCS Sublibrary: SL 7 – Artificial Intelligence ISSN ISBN-10 ISBN-13
0302-9743 3-540-68977-X Springer Berlin Heidelberg New York 978-3-540-68977-5 Springer Berlin Heidelberg New York
This work is subject to copyright. All rights are reserved, whether the whole or part of the material is concerned, specifically the rights of translation, reprinting, re-use of illustrations, recitation, broadcasting, reproduction on microfilms or in any other way, and storage in data banks. Duplication of this publication or parts thereof is permitted only under the provisions of the German Copyright Law of September 9, 1965, in its current version, and permission for use must always be obtained from Springer. Violations are liable to prosecution under the German Copyright Law. Springer is a part of Springer Science+Business Media springer.com © Springer-Verlag Berlin Heidelberg 2007 Printed in Germany Typesetting: Camera-ready by author, data conversion by Markus Richter, Heidelberg Printed on acid-free paper SPIN: 11960881 06/3142 543210
Books must follow sciences, and not sciences books — Francis Bacon, Proposition touching Amendment of Laws
Foreword
Long gone are the days when program verification was a task carried out merely by hand with paper and pen. For one, we are increasingly interested in proving actual program artifacts, not just abstractions thereof or core algorithms. The programs we want to verify today are thus longer, including whole classes and modules. As we consider larger programs, the number of cases to be considered in a proof increases. The creative and insightful parts of a proof can easily be lost in scores of mundane cases. Another problem with paper-and-pen proofs is that the features of the programming languages we employ in these programs are plentiful, including object-oriented organizations of data, facilities for specifying different control flow for rare situations, constructs for iterating over the elements of a collection, and the grouping together of operations into atomic transactions. These language features were designed to facilitate simpler and more natural encodings of
Data Loading...
