Learning Ada 1: Hello world, basic greeter package, citing contract based programming, aspects, SPARK…

in #ada-lang6 years ago

The Ada's Hello World is as simple as this:

with Ada.Text_IO; use Ada.Text_IO;

procedure Hello is
begin
   Put_Line ("Hello world");
end Hello;

Which with a proper syntax highlight looks better:

ada_hello.png

You put it into a file named hello.adb. If you name it differently, a warning will be written when you build it (with gnatmake hello.adb in my case):

warning: file name does not match unit name, should be "hello.adb"

Without the

use Ada.Text_IO;

we have to write the full name, Ada.Text_IO.Put_Line. Ada tends to be a little bit verbose, and this is something that can annoy, but with use and renames we can make life easier.

with Ada.Text_IO;

procedure Hello 
is
   package T renames Ada.Text_IO;
begin
   T.Put_Line ("Hello world");
end Hello;

Instead of using a string literal, we can put the string “into” a variable. We can also concatenate two or more strings using the operator &, and we can modify the string, which are array of characters.

with Ada.Text_IO; use Ada.Text_IO;

procedure Hello
is
   Hello : String := "Hello";
   World : String := "world";
begin
   Put_Line (Hello & " " & World & "!"); -- Hello world!
   World (1) := 'W';
   Put_Line (World); -- World
end Hello;

Arrays aren't zero-based; we can make zero-based arrays, though:

   A_String : array (0 .. 4) of Character;

Ada is “very” strongly typed, so A_String must keep five character, no more, no less:

procedure Hello
is
   A_String : array (0 .. 4) of Character;
   -- ...
begin
   -- ...
   A_String := "kayak";
   -- we can also specify them like this:
   A_String := ('k', 'a', 'y', 'a', 'k');
end Hello;

This is ok, but if we use "hi!" or "hello world" instead of "kayak", the compiler complains:

hello.adb:13:16: warning: wrong length for array of type of A_String declared at line 5
hello.adb:13:16: warning: "Constraint_Error" will be raised at run time

but we have our executable… and we already know it will raise:

Hello world!
World

raised CONSTRAINT_ERROR : hello.adb:13 length check failed

If we think of Ada as a mean towards writing robust software, it's better we tell the compiler to turn the warning into an error. (I'm surprised it uses such a default.) We can add more warnings (-gnatwa), and tell the compiler to fails if there are warnings (-gnatwe). Anyway, it can become frustrating and soon or later you'll relax few warnings (e.g., those about unused variables and alike — maybe you have them just because you are still developing!)

Default strings in Ada are fixed-length strings. In this line:

   Hello : String := "Hello";

the length is “deduced”: luckly we aren't forced to write this:

   Hello : String (1 .. 5) := "Hello";

If we are not going to modify the strings, we can say they are constant:

   Hello : constant String := "Hello";
   World : constant String := "world";

Then, if we try to modify them, compilation fails.

Because we are dealing with fixed-length strings and a strongly typed language, we can assign to each other only if they have the same length:

   World := Hello;
   Put_Line (World);   

This will write Hello. We don't have to overwrite the whole string: we can slice it:

   World (1 .. 3) := Hello (3 .. 5);
   Put_Line (World); -- output: llold

It works as long as the slices have the same length, of course.

A string is a one-based array of characters, but A_String is zero-based. This is why the following doesn't work:

procedure Hello
is
   A_String : array (0 .. 4) of Character;
begin
   -- ...
   Put_Line (String (A_String));
end Hello;

The type conversion String (xxx), which is needed because Put_Line wants a String, fails (value out of range), but if we change A_String into:

   A_String : array (1 .. 5) of Character;

The conversion works, Put_Line is happy and we read kayak as output.

We can do other things even with fixed-length strings, but we'll see them in a future article.

Now let's see how to write a greeter.

Packages

We can write our own package to use with the with statement. Let's do a simple greeter.

We put our greeter (a procedure, i.e. a subprogram, accepting one parameter) into a file. Each package is made of a specification, something which tells what's inside and how to use it, and an implementation, its body.

Specifications are put in files ending with .ads, bodies go into .adb files.

The specification of our greeter is this:

package Greeter is
   
   procedure Greet (S : String) 
     with Pre => S'Length > 0;
   
end Greeter;

Out package Greeter contains a procedure which has a string as input parameter, and this string must have length greater than 0.

The with Pre ... is an aspect, available since Ada 2012. Before Ada 2012, the precondition that must hold before entering the procedure couldn't be specified, unless you used SPARK. SPARK is a language which is a subset of the whole Ada, but had other features to make it possible to prove the correctness of a program. Many of those features are now part of the standard Ada 2012.

The precondition tells how to use correctly the procedure: we don't want to greet a null space, right?

The implementation is in the file greeter.adb, which is:

with Ada.Text_IO; use Ada.Text_IO;

package body Greeter is
   
   procedure Greet (S : String) is
   begin
      Put_Line ("Hello " & S & "!");
   end Greet;
   
end Greeter;

And our hello.adb (which isn't a package) becomes:

with Greeter;

procedure Hello is
begin
   Greeter.Greet ("world");
end Hello;

Now let's try to break the precondition:

   Greeter.Greet ("");

The program compiles ok and also run ok!

First, the aspects are there so that they can be used to check the correctness of a program. Maybe this isn't a task for the compiler alone, is it?

Secondly, we can in fact tell the compiler we want to do something if the precondition is broken. When the Pre is broken, what should it happen?

Ada has exceptions, as seen already (Constraint_Error), so we expect that greeting the null will raise an exception. We need to enable the runtime check, which is disabled by default: we must compile with the -gnata option.

Now we see an error:

raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : failed precondition from greeter.ads:4

We can also use a pragma to instruct the compiler to actually do the checks.

package Greeter is   
   pragma Assertion_Policy (Check);
   -- ...   
end Greeter;

Ada 2012 has many features useful for the so called contract based programming, which helps to prove the correctness of a program and in general to build better software which complies with the expectations.

Compiling

Now we have three files:

greeter.ads
greeter.adb
hello.adb

But the compilation is always done just with

gnatmake -gnat12 -gnatwa hello.adb

In GNAT there are conventions so that when the compiler read with Greeter, it knows it must find a greeter.ads, and automatically compiles that units too.

For more complex “layout”, though, a build tool like gprbuild will be useful. I will show something in a future article.

Uppercase, lowercase and style

Ada isn't case sensitive, but there are pretty conventions to be used, and of course consistency is always a good idea: if we write Greeter now, we'll write Greeter everywhere, even if we can write greeter or gReeTer.

Checks about style can be activated with -gnatyX option; with -gnatyy we activate all the checks. For example, in my files there were trailing spaces, and GNAT told me:

greeter.adb:4:01: (style) trailing spaces not permitted
greeter.adb:9:01: (style) trailing spaces not permitted
greeter.ads:2:01: (style) trailing spaces not permitted
greeter.ads:4:01: (style) trailing spaces not permitted
greeter.ads:5:32: (style) trailing spaces not permitted
greeter.ads:7:01: (style) trailing spaces not permitted

This is a minor violation of a style guide, but it's anyway a violation. Available checks can be found in the GNAT page for the style checking. Your editor or IDE of choice should be able to remove the trailing spaces.

Main?

In C we have a special function called main, which is the one called when we run our program from the command line. (Ok, it hasn't to be always so, but that's what it is most of the time.)

In Java we define a static method, also called main, inside the class. Sometimes we need to tell the compiler which class has the main method which must be called.

In the Ada example, we have just a file, hello.adb, which isn't part of a package and contains a single procedure. The compiler calls that procedure.

Can we add more procedure like we would do in, say, C? In fact in C we can write:

void do_something(void)
{
  /* ... */
}

int main(void)
{
   do_something();
   return 0;
}

Can we do something similar in Ada?

with Greeter;

procedure Do_It is
begin
   Greeter.Greet ("hello");
end Do_It;

procedure Hello
is
begin
   Do_It;
end Hello;

The compiler gives the answer: no, because in a file there must be only a compilation unit, and a “bare” (not in a package) procedure accounts for that. Then how can we put our “logic” into the procedure Do_It?

The answer is this:

with Greeter;

procedure Hello is
   
   procedure Do_It is
   begin
      Greeter.Greet ("hello");
   end Do_It;
   
begin
   Do_It;
end Hello;

The “declarative” part of a procedure can be rather thick; we can nest other procedures, define types and subtypes, and other things like package renaming — we've already seen that — and, well, of course that's the place where we put our variables and constants which are used inside our procedure!

The style check says that code above has a style problem: the procedure Do_It hasn't a specification. We can add it:

with Greeter;

procedure Hello is
   procedure Do_It;
   -- ...
begin
   Do_It;
end Hello;

Scope

In the example using the procedure Do_It, this procedure sees the other variables declared in the “host” procedure. E.g.

with Greeter;
procedure Hello is
   X : Integer := 2;
   procedure Do_It;
   
   procedure Do_It is
   begin
      if X > 20 then
         Greeter.Greet ("Hello");
      end if;
   end Do_It;
   
begin
   for I in Integer range 0 .. 30
   loop
      X := X + I;
      Do_It;
   end loop;
end Hello;

This example shows also for loop with integer ranges.

The procedure Do_It hasn't input parameters, but indeed it's like it has one. Usually this is bad programming, but if it is legitimated by a reason, then let's use an aspect to state that our procedure in fact uses a “global” as input.

with Greeter;

procedure Hello is
   X : Integer := 2;
   
   procedure Do_It
     with Global => (Input => X);

   -- ...
begin
   -- ...
end Hello;

This is useful to prove correctness.

Of course in this case we'd rather change the procedure from parameterless to taking a single parameter.

See also SPARK documentation.

Both Hello and Do_It of course also see variables of the packages specified in with, provided they are used with the full name, Greeter.A_Variable or alone in case we add use Greeter.

For example, in greeter.ads we add:

package Greeter is
   
   Y : Integer;
   
   -- ...

end Greeter;

The variable Y is a package global variable. It is seen by all other units having with Greeter. Let's use it in hello.adb:

with Greeter;

procedure Hello is
   -- ...
begin
   Greeter.Y := 10;
   for I in Integer range 0 .. Greeter.Y
   loop
      X := X + I;
      Do_It;
   end loop;
end Hello;

What if in stead of Greeter.Y we have Greeter.X and then we add use Greeter? The “local” symbols win and any conflicting symbol must be qualified. So we must write Greeter.X for the variable in the package, and we can still use X for the variable X of Hello.

Writing integers to standard output

If you want to play with X, Y, Greeter.X, … you have to know a gear to print them. You will use Integer'Image. The ' is a way to access attributes. In this case, the type Integer, as other types, has an attribute Image which gives a string representation of the value held by the variable.

   Put_Line (Integer'Image (Greeter.X));
   Put_Line (Integer'Image (Y));

There's another way which give more control on the output; I cite it here, but I will explore it in a future article. (Note: here I'm assuming you renamed Greeter.Y into Greeter.X).

-- ...
procedure Hello is
   package Int_IO is new Ada.Text_IO.Integer_IO (Integer);
   
   X : Integer := 2;
   -- ...
begin
   -- ...
   Put_Line (Integer'Image (Greeter.X)); -- X in pkg Greeter
   Put_Line (Integer'Image (X));         -- X in Hello
   Int_IO.Put (X); New_Line;
end Hello;

The package Ada.Text_IO.Integer_IO is “parametrized”; more correctly, it is a generic package, but to use it you must specify what is the type which was “generic”. It is like templates in C++ when you must specify a type to instantiate the template; e.g. using the vector in STL:

std::vector<int> x;

Indeed it is more like doing this:

typedef std::vector<int> int_vec;

And then using int_vec. In Ada you “instantiate” the package with the concrete type you need and assign a name to this instance.

Uninitialized variable?!

The Greeter.Y (or Greeter.X if you tried to rename it to X to check if it clashes with the X inside Hello) doesn't seem to be initialized. In Ada it takes a default value, so you don't need to be worried: its value is well defined.

But in case you don't want it to be 0, you can say:

package Greeter is
   
   X : Integer := 1000;

   -- ...
end Greeter;

Package private variables

If we want our Greeter.Y to be accessible from the code which uses it, we must put into the public package specification as we in fact did. But if it's something that the package uses internally and it shouldn't be exposed, then we put it into the package body.

with Ada.Text_IO; use Ada.Text_IO;

package body Greeter is
   
   Hello_Text : constant String := "Hello ";

   procedure Greet (S : String) is
   begin
      Put_Line (Hello_Text & S & "!");
   end Greet;

end Greeter;

The variable Hello_Text can't be accessed from outside, not even with Greeter.Hello_Text: it's private to the package. If we try

   Put_Line (Greeter.Hello_Text);

the compilation fails with "Hello_Text" not declared in "Greeter".

A specification can contain a private part, though. In this case it is private from the point of view of code, but can be read by anybody who has access to the specification file.

package Greeter is
   -- ...
private
   
   Hi_Text : constant String := "Hi ";
   
end Greeter;

Specification files are what the users of your package will read, in case you don't want to give them all the sources.

Read Building a library, a more advanced topic but in case you are curious…

Sources

These sources can be a mix of what I've used in the text. I am not using hastebin because it thinks this code is Pascal, not Ada, and currently it doesn't seem there's a way to tell it which syntax highlighter to use.

Conclusion and remarks

As first article, or lesson since I'm trying to teach (myself and readers) something, I think it's enough. If there are questions or suggestions, please comment — but first be sure the answer isn't in the article already.

Criticism is “welcome” if and only if it addresses real, actual, and solvable problems in the scope of the approach of these articles. I will try to ignore pointless and annoying criticism like there are many more things to say about package, or alike! Of course, there's more about package to be said, and I don't know if I will unroll everything (and correctly) in other articles. Though, the implicit answer is: really? I will be glad to read your article about that! And I really mean it, no sarcasm: currently I am eager about learning material on Ada!

(I am mentioning package because I am planning to tell more about them in the next article, by the way.)

Sort:  

It's good to see a bit of interest in Ada. I really think it has some nice features to it that disappeared from languages that came after it (aside from some functional languages). I am mainly thinking of the type system when I say that.

I will be interested to see what you think of it once you get there.

Based on what I've already seen, I can say the Ada's type system is some kind of central part of the design to give tools for writing more reliable and safe software. I don't know of other languages which allow for so detailed “domain” definition through types!

Coin Marketplace

STEEM 0.35
TRX 0.12
JST 0.040
BTC 70797.92
ETH 3553.00
USDT 1.00
SBD 4.76