软件工程方法

TLA+ 追踪：先说清要验证什么，形式化方法才能给出有效结论

据 Hillel Wayne 的技术文章，TLA+ 教育者 Hillel Wayne 讨论了这种方法能直接表达哪些系统性质，以及哪些需求需要额外建模或其他工具。