Аннотированный язык Ада (Анна)

Я новичок в языке Ада и хотел бы знать, что означают обозначения. Я прочитал в документе о повторном использовании программного обеспечения Kreuger, что Анна - это язык аннотаций для описания Ады. Считается ли это формальным комментарием к коду Ады?

Например:

subtype EVEN is INTEGER;

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

2-я строка — это аннотация Анны для первой строки, которая представляет собой код Ады. Является ли вторая строка просто комментарием, позволяющим пользователю понять первую строку, или это ограничение, которое «обязательно» для упоминания, а не просто необязательная строка?

я действительно в замешательстве


ada
person Joe Brown    schedule 04.08.2012    source источник

Ответы (2)


arrow_upward
3
arrow_downward

Анна древняя, не тратьте на это время.

Есть несколько мест, с которых можно начать работу с Адой. Среди них Викикнига по Аде, а Информационный центр по Ада (AdaIC) поддерживает список рекомендуемых ресурсов.

Если вас интересует формальная логика применительно к Аде, вам следует изучить SPARK («SPARK — это язык программирования, набор инструментов для анализа исходного кода (статическая проверка) и метод проектирования для разработки высокопроизводительных систем). программное обеспечение для обеспечения безопасности"). Ниже приведен краткий обзор и руководство, хотя вы, возможно, не захотите займитесь этим, пока у вас не будет практики с Адой за плечами.

Вы, вероятно, уже знаете о компиляторе GNAT, но на всякий случай: GNAT GPL 2012 — это компилятор с открытым исходным кодом, доступный для Linux, Windows и некоторые другие платформы. (GNATPro доступен для многих платформ.)

Удачи, задавайте вопросы здесь, другие ресурсы включают comp.lang.ada и подраздел Ады.

person Marc C    schedule 04.08.2012
comment
Большое спасибо, на самом деле я прошу Анну, потому что я хотел бы представить ее в качестве примера для аннотации в моей диссертации. Я хотел бы понять эти 2 строки, чтобы я мог привести пример, потому что я занимаюсь исследованием повторного использования программного обеспечения, а Анна является примером для указания компонентов, написанных на Аде. - person Joe Brown; 04.08.2012
comment
Посмотрите материал СПАРК. Он делает такие же аннотации, и, поскольку он актуален, намного легче найти пояснительный материал о нем. (Короче говоря, ANNA давно нет, так что достоверных материалов о ней мало.) - person Marc C; 04.08.2012

arrow_upward
3
arrow_downward

  1. EVEN является целым числом с ограничением быть, ну, четным. Таким образом, 2-я строка является ограничением. Но это не будет проверяться компилятором — и, насколько мне известно, набор инструментов Anna никогда не мог проверять такие ограничения.

  2. Анна древняя и давно ушла, но недавний стандарт Ады (Ада 2012) поддерживает такие аннотации (которые даже могут быть проверены компилятором). Таким образом, ваше выражение Ада/Анна может быть записано на языке Ада 2012 как

    подтип Even является целым числом с Dynamic_Predicate => Even mod 2 = 0;

На самом деле это пример из обоснования Ada 2012, см. Ada 2012.

person Stefan    schedule 21.08.2012