文档介绍：Texts puter Science
Editors
David Gries
Fred B. Schneider
For further volumes:
ies/3 191
pression, OCR, web optimization using a watermarked evaluation copy of CVISION pressor
Krzysztof R. Apt
Frank S. de Boer
Ernst-Rüdiger Olderog
Verification of Sequential
and Concurrent Programs
Third, Extended Edition
ì Springer
pression, OCR, web optimization using a watermarked evaluation copy of CVISION pressor
Krzysztof R. Apt Frank S. de Boer
Centrum Wiskunde Centrum Wiskunde
& Informatica & Informatica
Science Park 123 Science Park 123
1098 XG Amsterdam 1098 XG Amsterdam
herlands
Ernst-Rüdiger Olderog
Department für Informatik
Universität Oldenburg
26111 Oldenburg
Germany
olderog informatilcuni-
Series Editors
David Gries Fred B. Schneider
Department puter Science Department puter Science
Upson Hall Upson Hall
Cornell University Cornell University
Ithaca, NY 14853-750 1, USA Ithaca, NY 14853-7501, USA
ISSN 1868-0941 e-ISSN 1868-095X
ISBN 978-1-84882-744-8 e-ISBN 978-1-84882-745-5
DOl -1-84882-745-5
Springer Dordrecht Heidelberg London New York
British Library Cataloguing in Publication Data
A catalogue record for this book is available from the British Library
Library of Congress Control Number: 2009932111
© Springer-Verlag London Limited 2009, Reprinted with corrections 2010
Apart from any fair dealing for the purposes of research or private study, or criticism or review, as
permitted under the Copyright, Designs and Patents Act 1988, this publication may only be reproduced,
stored or transmitted, in any form or by any means, with the prior permission in writing of the
publishers, or in the case of reprographic reproduction in accordance with the terms of licenses issued by
the Copyright Licensing Agency. Enquiries concerning reproduction outside those terms should be sent
to the publi