Identifiers use Mixed_Case_With_Underscores. Acronyms remain upper case:
Variable_Name : Integer;
Variable_With_TLA : Integer;Wherever possible aspects should be used. Pragmas should only be used if there is no equal aspect or if using the aspect would cause a bug in the toolchain. If a pragma is used that could have been an aspect a comment with a justification and a reference to an issue is required.
In the declarative part of both package specifications and bodies all
declarations of types, subprograms, etc. are separated by a single blank line.
This includes a single blank line at the beginning and the end of the package.
The package initialization part after begin in the body should not contain
any blank lines.
package Foo is
<declaration>
<declaration>
end Foo;package Foo with
SPARK_Mode,
Pure
is
<declaration>
<declaration>
end Foo;package body Foo with
SPARK_Mode,
Pure
is
<declaration>
<declaration>
begin
<statements>
end Foo;package body Foo is
<declaration>
<declaration>
begin
<statements>
end Foo;procedure Foo (A : Natural;
B : Natural) with
Pre => True,
Post => True;function Bar (A : Natural;
B : Natural) return Natural with
Pre => True,
Post => True;function "+" (Left, Right : Integer) return Integer with
Pre => True,
Post => True;function "+" (Left : Integer; Right : Boolean) return Integer with
Pre => True,
Post => True;Subprogram bodies should not contain blank lines at all.
procedure Foo is
<declarations>
begin
<statements>
end Foo;procedure Foo (A : Natural;
B : Natural) with
Pre => True,
Post => True
is
<declarations>
begin
<statements>
end Bar;
function Bar return <type_name> is
<declarations>
begin
<statements>
end Bar;function Bar (A : Natural;
B : Natural) return Natural with
Pre => True,
Post => True
is
<declarations>
begin
<statements>
end Bar;function Bar (N : Natural) return Natural is
(N + 1)
with
Pre => N <= 42; type Foo_Record is record
Bar : Natural;
end record with
Convention => C;type Enum is (A, B, C);type Enum_Short is (A, B, C) with Aspect => Condition;type Enum_Long is
(Very_Very_Very_Very_Long_Literal_1,
Very_Very_Very_Very_Long_Literal_2,
Very_Very_Very_Very_Long_Literal_3)
with Aspect => Condition;if <condition> then
<statements>
elsif <condition> then
<statements>
else
<statements>
end if;If any of the <condition>s does not fit onto one line:
if
(((<condition>
and then <condition>)
or else <condition>)
and then <condition>)
then
<statements>
elsif
<condition>
then
<statements>
else
<statements>
end if;(if <condition> then <expression> elsif <condition> then <expression> else <expression>)If the whole expression does not fit onto one line:
(if
(((<condition>
and then <condition>)
or else <condition>)
and then <condition>)
then
<expression>
elsif
<condition>
then
<expression>
else
<expression>)case <selector> is
when <first_alternative> => <statement>;
when <second_alternative> => <statement>;
when others => <statement>;
end case;If at least one <statement> does not fit onto the line or at least one alternative has multiple statements, all lines are wrapped and arrows are not aligned:
case <selector> is
when <first_alternative> =>
<statement>;
<statement>;
when <second_alternative> =>
<statement>;
when others =>
<statement>;
<statement>;
end case;(case <selector> is
when <first_alternative> => <expression>,
when <second_alternative> => <expression>,
when others => <expression>)If at least one <expression> does not fit onto the line, all lines are wrapped and arrows are not aligned:
(case <selector> is
when <first_alternative> =>
<expression>,
when <second_alternative> =>
<expression>,
when others =>
<expression>)Conditions in loops are formatted equally to conditions in if expressions.
while <condition> loop
<statements>
end loop;With multi line conditions:
while
(((<condition>
and then <condition>)
or else <condition>)
and then <condition>)
loop
<statements>
end loop;for <index> in <range> loop
<statements>
end loop;
for <element> of <array> loop
<statements>
end loop;For long ranges and arrays that do not fit on a line:
for <index> in
First .. Last
loop
<statements>
end loop;
for <index> in
Long_First
.. Long_Last
loop
<statements>
end loop;
for <element> of
Array (First .. Last)
loop
<statements>
end loop;
for <element> of
Array (Long_First
.. Long_Last)
loop
<statements>
end loop;loop
<statements>
exit when <condition>;
<statements>
exit when (((<condition>
and then <condition>)
or else <condition>)
and then <condition>);
<statements>
end loop;procedure Foo (Buffer_Address : System.Address;
Buffer_Length : Interfaces.C.Size_T)
is
Buffer : Array_Type (Index_Type'First ..
Index_Type'First + Length_Type (Buffer_Length) - 1) with
Address => Buffer_Address;
begin
<statements>
end Foo;Use clauses for packages are not permitted. Use clauses for types should be as limited in scope as feasible.