序曲 软件无处不在 全世界有超过10亿辆汽车在行驶，每辆新汽车上 都有20~80个微处理器，有多达3000万行的代码 在运行 全世界每年有多达23亿次手术，在每个现代医疗 设备上往往会有超过30万行的代码在运行 全世界有超过3000辆高速列车在行驶，每辆列车 上会有多达6000万行的代码在运行 -全世界有超过300万架飞机，新型飞机上会有多达 2000万行代码在运行 如何保证这些代码没有错误？序 曲 • 软件无处不在 – 全世界有超过10亿辆汽车在行驶，每辆新汽车上 都有20～80个微处理器，有多达3000万行的代码 在运行 – 全世界每年有多达23亿次手术，在每个现代医疗 设备上往往会有超过30万行的代码在运行 – 全世界有超过3000辆高速列车在行驶，每辆列车 上会有多达6000万行的代码在运行 – 全世界有超过300万架飞机，新型飞机上会有多达 2000万行代码在运行 如何保证这些代码没有错误？ 6