It's a directive that happens to be placed at the tail end of a comment. Reading the documentation the doc comment stops being a comment-proper with the first @

It's a directive that happens to be placed at the tail end of a comment. Reading the documentation the doc comment stops being a comment-proper with the first @-directive, after that it's a list of directives. SPARK started in comments, ACSL is placed in specially marked comments. SPARK 2014 moved into Ada proper using Ada 2012 features (aspects). The difference between SPARK 2014's annotation and this is basically, are the annotations above the function or after the function declaration?