细化微积分

细化微积分是一种用于逐步细化程序构造的正式方法。最终可执行程序的预期行为被指定为一个抽象的，也许是不可执行的程序，然后通过一系列保持正确性的转换被细化为一个有效的可执行程序。支持者包括Ralph-JohanBack，他在1978年的博士论文《论程序开发中细化步骤的正确性》中提出了这种方法，还有CarrollMorgan，特别是他的《从规范中编程》（PrenticeHall，第二版，1994，ISBN0-13-123274-6）。

在后一种情况下，其动机是将Abrial的规范符号Z，通过严格的行为保全程序细化，与基于Dijkstra的命令保全语言的可执行编程符号联系起来。在这种情况下，行为保全意味着一个程序所满足的任何Hoare三元组也应该被它的任何细化所满足，这个概念直接导致了作为前条件和后条件的典型语句，这些语句本身对任何可以合理地放在它们之间的程序都有条件。