我是 Ada 语言的初学者，我想知道符号的含义。我在 Kreuger 软件重用论文中读到 Anna 是一种用于描述 Ada 的注释语言。这是否被认为是对 Ada 代码的正式评论？
例如：
subtype EVEN is INTEGER;
--| where X : EVEN = ) X mod 2 = 0;
第二行是 Anna 注释，第一行是 Ada 代码。第二行只是让用户理解第一行的注释，还是“必须”提及的约束，而不仅仅是可选行？
我真的很困惑
问问题
539 次
2 回答
3
安娜是古老的，不要浪费你的时间。
有很多地方可以从 Ada 开始。其中包括Ada Wikibook，Ada Information Clearinghouse (AdaIC) 维护着一个建议资源列表。
如果你对适用于 Ada 的形式逻辑感兴趣，你会想研究一下 SPARK（“SPARK 是一种编程语言，一套源代码分析（静态验证）工具，以及一种用于开发高性能的设计方法）保证软件。”）这里有一个快速概述和教程，尽管在您对 Ada 进行了一些练习之前，您可能不想解决这个问题。
您可能已经了解 GNAT 编译器，但以防万一，GNAT GPL 2012是一个可用于 Linux、Windows 和其他一些平台的开源编译器。（GNATPro 可用于许多平台。）
祝你好运，在这里提问，其他资源包括comp.lang.ada和Ada sub-reddit。
于 2012-08-04T15:22:24.453 回答
3
EVEN 是整数，其约束是，嗯，偶数。所以第二行是一个约束。但是编译器不会检查它——而且，据我所知，Anna 工具集从未能够检查这些约束。
Anna 很古老，早已不复存在——但最近的 Ada 标准 (Ada 2012) 支持此类注释（甚至可以由编译器检查）。所以你的 Ada/Anna 表达式可以在 Ada 2012 中写成
子类型 Even 是带有 Dynamic_Predicate => Even mod 2 = 0 的整数；
这实际上是 Ada 2012 基本原理中的一个示例，请参见Ada 2012。
于 2012-08-21T10:19:33.473 回答