Published online by Cambridge University Press: 02 March 2010
The concepts presented in this book are based on ideas from mathematics and theoretical computer science. Readers certainly do not need to understand these theoretical aspects in order to use the techniques we present. However, some may be interested in pursuing these topics in further detail, and for these readers we can point to the following sources of information.
The central idea of a model program that we present throughout the book is based on the theory of abstract state machines (ASMs) conceived by Yuri Gurevich in 1980s. An ASM is a formal way to describe the steps of an algorithm. It gives a mathematical view of program state (including the state of object-oriented systems and systems with complex structure). There is a well-developed body of scientific literature on the topic. Readers interested in ASMs may wish to see the ASM Web page maintained at the University of Michigan (ASM, 2006). Of particular interest is the “Lipari guide” (Gurevich, 1995).
We also use ideas taken from finite automata, mathematical logic, and set theory. The composition of automata for language intersection is a core concept. A classic text that describes finite automata and their properties is Hopcroft and Ullman (1979). A useful and practical introduction to logic and set theory is found in Lipschutz (1998).
A mathematically rigorous survey of assurance methods including modeling, testing, and static analysis appears in the book by Peled (2001).
The ideas in this book were developed and made practical at Microsoft Research from 1999 through 2006 in the Foundations of Software Engineering group (FSE, 2006).
To save this book to your Kindle, first ensure [email protected] is added to your Approved Personal Document E-mail List under your Personal Document Settings on the Manage Your Content and Devices page of your Amazon account. Then enter the ‘name’ part of your Kindle email address below. Find out more about saving to your Kindle.
Note you can select to save to either the @free.kindle.com or @kindle.com variations. ‘@free.kindle.com’ emails are free but can only be saved to your device when it is connected to wi-fi. ‘@kindle.com’ emails can be delivered even when you are not connected to wi-fi, but note that service fees apply.
Find out more about the Kindle Personal Document Service.
To save content items to your account, please confirm that you agree to abide by our usage policies. If this is the first time you use this feature, you will be asked to authorise Cambridge Core to connect with your account. Find out more about saving content to Dropbox.
To save content items to your account, please confirm that you agree to abide by our usage policies. If this is the first time you use this feature, you will be asked to authorise Cambridge Core to connect with your account. Find out more about saving content to Google Drive.