Preface

Writing programs is fun and rewarding. Programming is an activity that many people would do for fun, and yet are paid for. In this sense, a programmer is a bit like an actor, a musician, or a professional football player. It seems like a dream until you, as a programmer, begin to have real responsibilities. Writing games or office applications isn’t really a big deal from this point of view. If your application has a bug, you simply fix it and release a new version. But if you write applications that people depend on, and if you can’t simply release a new version and have your users install it themselves, it’s another story. Of course, Java isn’t meant for writing applications for monitoring nuclear plants or flying airplanes, or any system in which a simple bug could put human life at risk. But if your application is used to manage internet backbones, you wouldn’t like a nasty bug to be discovered one day before the Olympic Games open, causing a TV transmission failure for a whole country. For such applications, you want to be sure that your program can be proven correct.