Egon Börger and Dean Rosenzweig generously shared with me their ideas and rich application experience. Discussions with Andreas Blass were indispensable in clarifying things. Numerous working walks with Jim Huggins through the woods of Ann Arbor were very helpful. Raghu Mani raised important implementation issues. Numerous ealgebraists commented on earlier drafts of the guide. I am very thankful to all of them. To an extent, this chapter is a result of a collective effort, though I am responsible for possible blunders.
A preliminary version of the guide has been tried out during the 1993 summer school on Specification and Validation Methods for Programming Languages and Systems on the beautiful island of Lipari in Italy. I use this opportunity to thank the organizers, Egon Börger and Alfredo Ferro, and all participants.