ada - 带注释的 Ada 语言(Anna)

Question

我是 Ada 语言的初学者，我想知道符号是什么意思。我在 Kreuger 软件重用论文中读到 Anna 是一种描述 Ada 的注释语言。这被认为是对 Ada 代码的正式评论吗？

例如:

subtype EVEN is INTEGER;

--| where X : EVEN = ) X mod 2 = 0;

第二行是对第一行 Ada 代码的 Anna 注释。第二行只是一个让用户理解第一行的注释，还是一个“必须”提及的约束，而不仅仅是一个可选行？

我真的很迷茫

Answer 1

Anna 古老，不要浪费你的时间。

有很多地方可以开始使用 Ada。其中有Ada Wikibook ，Ada 信息交换所 (AdaIC) 维护着一个 list of suggested resources .

如果您对适用于 Ada 的形式逻辑感兴趣，您将需要研究 SPARK(“SPARK 是一种编程语言，一组源代码分析(静态验证)工具，以及一种设计方法开发高保证软件。”)这是一个 quick overview and tutorial ，尽管在您对 Ada 进行一些练习之前，您可能不想解决这个问题。

您可能已经了解 GNAT 编译器，但为了以防万一，GNAT GPL 2012是可用于 Linux、Windows 和其他一些平台的开源编译器。 (GNATPro 适用于许多平台。)

祝你好运，在这里提问，其他资源包括comp.lang.ada和 Ada sub-reddit .