Logics of Specification Languages
By a specification language we understand a formal system of syntax, semantics and proof rules. The syntax and semantics define a language; the proof rules define a proof system. Specifications are expressions in the language, and reasoning over propertie
- PDF / 5,327,293 Bytes
- 635 Pages / 439.368 x 666.139 pts Page_size
- 116 Downloads / 239 Views
Advisory Board: G. Ausiello M. Broy C.S. Calude A. Condon D. Harel J. Hartmanis T. Henzinger T. Leighton M. Nivat C. Papadimitriou D. Scott
Dines Bjørner · Martin C. Henson Editors
Logics of Specification Languages
123
Prof. Emeritus, Dr. Dines Bjørner Informatics and Mathematical Modelling Technical University of Denmark 2800 Kgs. Lyngby Denmark [email protected]
Series Editors Prof. Dr. Wilfried Brauer Institut für Informatik der TUM Boltzmannstr. 3 85748 Garching, Germany [email protected] Prof. Dr. Grzegorz Rozenberg Leiden Institute of Advanced Computer Science University of Leiden Niels Bohrweg 1 2333 CA Leiden, The Netherlands [email protected]
ISBN 978-3-540-74106-0
Prof. Martin C. Henson University of Essex Department of Computer Science Wivenhoe Park CO4 3SQ Colchester United Kingdom [email protected]
Prof. Dr. Juraj Hromkoviˇc ETH Zentrum Department of Computer Science Swiss Federal Institute of Technology 8092 Zürich, Switzerland [email protected] Prof. Dr. Arto Salomaa Turku Centre of Computer Science Lemminkäisenkatu 14 A 20520 Turku, Finland asalomaa@utu.fi
e-ISBN 978-3-540-74107-7
DOI 10.1007/978-3-540-74107-7 ACM Computing Classification (1998): F.4, F.3, D.1, D.2, D.3 Library of Congress Control Number: 2007936401 Monographs in Theoretical Computer Science. An EATCS Series. ISSN 1431-2654 © 2008 Springer-Verlag Berlin Heidelberg 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, reuse of illustrations, recitation, broadcasting, reproduction on microfilm 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. The use of general descriptive names, registered names, trademarks, etc. in this publication does not imply, even in the absence of a specific statement, that such names are exempt from the relevant protective laws and regulations and therefore free for general use. Cover Design: KünkelLopka, Heidelberg Printed on acid-free paper 987654321 springer.com
The editors dedicate this book to: ASM : Yuri Gurevich B : Jean-Raymond Abrial CASL : Peter D. Mosses CafeOBJ : Joseph A. Goguen, 1941–2006 DC : Zhou Chaochen RAISE : Søren Prehn, 1955–2006 VDM : Peter Lucas TLA+ : Leslie Lamport Z : Jean-Raymond Abrial
Preface
1 Specification Languages By a specification language we understand a formal system of syntax, semantics and proof rules. The syntax and semantics define a language; the proof rules a proof system. Specifications are expressions in the language — and reasoning over properties of these specifications is done within the proof system. This book [2] will present nine of the current specification languages (ASM [40], B [5], CafeOBJ [8], CASL [33], Duration Calculus [14],
Data Loading...
