Jos Bacelar Almeida - Rigorous Software Development÷ An Introduction to Program Verification (Undergraduate Topics in Computer Science).pdf

Undergraduate Topics puter Science
Undergraduate Topics puter Science (UTiCS) delivers high-quality instructional content for un-
dergraduates studying in all areas puting and information science. From core foundational and
theoretical material to final-year topics and applications, UTiCS books take a fresh, concise, and mod-
ern approach and are ideal for self-study or for a one- or two-semester course. The texts are all authored
by established experts in their fields, reviewed by an international advisory board, and contain numer-
ous examples and problems. Many include fully worked solutions.
For further volumes:
ies/7592
José Bacelar Almeida  Maria João Frade 
Jorge Sousa Pinto  Simão Melo de Sousa
Rigorous
Software
Development
An Introduction to
Program Verification
Dr. José Bacelar Almeida Dr. Jorge Sousa Pinto
Depto. Informática Depto. Informática
Universidade do Minho Universidade do Minho
Campus de Gualtar Campus de Gualtar
Braga 4710-057 Braga 4710-057
Portugal Portugal
******@ ******@
Dr. Maria João Frade Dr. Simão Melo de Sousa
Depto. Informática Depto. Informática
Universidade do Minho Universidade Beira Interior
Campus de Gualtar rua Marques d’Avila e Bolama
Braga 4710-057 Covilhã 6201-001
Portugal Portugal
******@ ******@
Series editor
Ian Mackie
Advisory board
Samson Abramsky, University of Oxford, Oxford, UK
Chris Hankin, Imperial College London, London, UK
Dexter Kozen, Cornell University, Ithaca, USA
Andrew Pitts, University of Cambridge, Cambridge, UK
Hanne Riis Nielson, Technical University of Denmark, Lungby, Denmark
Steven Skiena, Stony Brook University, Stony Brooks, USA
Iain Stewart, University of Durham, Durham, UK
ISSN 1863-7310
ISBN 978-0-85729-017-5 e-ISBN 978-0-85729-018-2
DOI -0-85729-018-2
Springer London Dordrecht Heidelberg New York
British Library Cataloguing in Publication Data
A catalogue record for this book is available from the British