精化演算

精化演算是一种从规范逐步推导实现的形式化开发方法。

基本思想

从抽象规范出发，通过一系列精化步骤，逐步得到具体实现。

精化步骤

1. 数据精化：抽象数据类型 → 具体数据结构
2. 算法精化：非确定性规范 → 确定性算法
3. 代码精化：伪代码 → 目标语言

代表工具

• B方法
• Event-B
• Z notation