主要观点：

• 以 Ada/SPARK 编写后缀表达式计算器，探讨 Ada/SPARK 的优势、“验证”含义、操作等。
• 介绍编写过程中的各种步骤、困难及应对方法，如设置工具链、证明代码、处理浮点简化等。
• 强调验证的重要性及注意事项，如遵循预条件、使用足够的证明器等。

关键信息：

• Ada/SPARK 可用于正式验证，工具链安装方便，如使用 Alire 安装 GNATprove。
• “验证”意味着无溢出、无运行时错误、遵守预条件和后条件等。
• 后缀表达式计算器操作方式，如通过栈进行计算。
• 编写过程中遇到的问题，如浮点计算简化、证明器运行设置等。

重要细节：

• SPARK 是 Ada 的子集，可与 Ada 代码共存，通过 SPARK_Mode 控制。
• 编写代码时先验证核心部分，如机器和词法分析器，再添加输入输出层。
• 浮点计算中 Value 和 Bounded_Value 的分离及相关简化。
• 不同证明器级别和选项的使用，如 --level=2 和 -j12 。
• 各种验证机制，如 Assume 、Additional Asserts 、Contract_Cases 等的使用。
• 处理循环不变量、私有子程序和不变量等问题。
• 算术操作结果的检查及对代码的影响。

总结：通过以 Ada/SPARK 编写后缀表达式计算器，展示了 Ada/SPARK 在正式验证方面的应用及过程中遇到的各种问题和解决方法，强调了验证的重要性和细节。