形式化规范：超越程序指令的软件行为描述

本文探讨了形式化规范与传统程序的区别。传统程序是指令列表，而形式化规范是行为集合。作者以计数器为例，说明规范如何定义所有正确行为，并利用集合论的思想，通过生成器（Init和Next）描述无限行为集。这与程序中非确定性的概念有所不同，形式化规范中的非确定性指行为的多种扩展方式，而程序中的非确定性则指代码路径的不确定性。文章强调了理解形式化规范作为行为集合的重要性，这有助于调试和理解模型检查器的错误。