So indeed it's a good time to get your hands dirty and write some code,
play with the containers, Ada 2012, contracts ...
The "lighter introduction to hi-lite" is a good start, but it shouldn't
take you too long. By the way, you can find the code in
testsuite/gnatprove/tests/intro
After that, here is a homework assignment to get you started with contracts.
1) Write a stack package whose spec (stacks.ads) looks a bit like that:
package Stacks is
-- A stack package that holds integers
Max_Size : constant Integer := 1000;
-- the maximal number of elements in the stack
type Content_Type is array (1 .. Max_Size) of Integer;
-- the array that holds the elements
type Stack is record
Content : Content_Type;
Index : Integer;
end record;
function Create return Stack;
function Is_Empty (S : Stack) return Boolean;
function Is_Full (S : Stack) return Boolean;
procedure Push (S : in out Stack; X : Integer);
-- push a new element on the stack
procedure Pop (S : in out Stack; X : out Integer);
-- remove the topmost element from the stack, and return it in X
function Pop (S : in out Stack) return Integer;
-- same as the above procedure, but return the topmost element,
-- instead of having an out parameter
-- note that only in Ada 2012 functions can have in out parameters.
end Stacks;
2) Write an implementation for this package (stacks.adb). The Stack is
an array, together with an index that points to the first empty cell, or
to last used cell, as you wish.
3) Write a main program that tests your stack implementation. It could
look as follows (main.adb):
with Stacks; use Stacks;
procedure Main is
S : Stack := Create;
X : Integer;
begin
pragma Assert (Is_Empty (S));
Push (S, 1);
pragma Assert (not (Is_Empty (S)));
Pop (S, X);
pragma Assert (X = 1);
pragma Assert (Is_Empty (S));
Push (S, 2);
Push (S, 3);
Push (S, 4);
X := Pop (S);
pragma Assert (X = 4);
X := Pop (S);
pragma Assert (X = 3);
X := Pop (S);
pragma Assert (X = 2);
pragma Assert (Is_Empty (S));
end Main;
Obviously, when you run your program, none of the assertions should
fail! Be sure to compile with option "-gnata".
Best is to write a project file, such as "test.gpr", with the following
contents:
project Test is
for Object_Dir use "obj";
for Exec_Dir use ".";
for Main use ("main.adb");
package Compiler is
for Default_Switches ("ada") use ("-gnat12", "-gnata");
end Compiler;
end Test;
You can now compile your project with
$ gnatmake -P test.gpr
4) What happens when you add the following line at the end of the Main
procedure:
X := Pop (S);
5) You can protect yourself against what happens in (4) if you add a
precondition to Pop:
procedure Pop (S : in out Stack; X : out Integer)
with Pre => (not Is_Empty (S));
What happens now if you run the main program of (4)? In what way is that
better than what happened in (4)?
6) Write more preconditions, so that any runtime error in your stacks
package is impossible. Write a few tests in main.adb to check that.
7) Write postconditions that you know are true after executing a
subprogram. For example, you know that after a "push", the stack is not
empty, and after a "pop", it is not full.
8) Pre/ and Postconditions should never have side effects. There is a
problem with that, because it means you cannot use Push and Pop in
pre/post. A way to solve this is to write functions without side
effects, that do something similar to push and pop, but without changing
the stack. For example, you can write a function Peek that returns the
topmost element of the stack without removing it. You can then write in
the postcondition of push:
Peek (S) = X
to express that the topmost element is the one we just pushed.
Write the function Peek and use it in the pre/post.
9) The proposed solution in (8) solves only half of the problem, it
gives an alternative to Pop, but not to Push. For Push, what we need is
a *function* Push that leaves the current Stack alone and returns a new
stack with the new element on top:
function Push (S : Stack; X : Integer) return Stack;
Note that "S" is an "in" parameter and is not modified. So Push must
make a copy of S, modify the copy, and then return that modified copy.
10) Use the function of (9) in your pre/post. For example, a complete
contract of the procedure Push is now the following:
procedure Push (S : in out Stack; X : Integer)
with Pre => (not Is_Full (S)),
with Post => (S = Push(S'Old, X));
we have used S'Old to refer to the previous value of S, ie the stack S
before pushing.
11) With the package, one can only create stacks that all have the same
fixed size. How can you change it to create stacks that have a different
maximal size? You need to change the type definition, and the function
Create, which now has an argument for the maximal size.
Hint: use discriminant records.
Change your tests and run them to see if all assertions and
pre/postconditions still hold.
12) Write a version of stacks that can hold any number of integers. This
means that at some point you need to reallocate memory. It also means
that you probably need to use pointers (access).
Change your tests and run them to see if all assertions and
pre/postconditions still hold.
13) Write a version of stacks that can hold any definite object (whose
size is statically known), not just Integer. Use the Ada feature of
generic packages for that.
Change your tests and run them to see if all assertions and
pre/postconditions still hold.
14) Write a version of stacks that can hold any object, even objects of
mixed size. You probably need to use pointers again.
Change your tests and run them to see if all assertions and
pre/postconditions still hold.
15) Feel free to write an Ada program that uses your stack, and does
something useful, add pre/post to your own program ...
16) I forgot another aspect of the example. Make the type Stack private.
Does this change anything for the implementation of the stack, and for
the clients of the stack?
I'm not sure how long this may take you, this assignment is really just
to get you started, feel free to abandon this whenever you think you
have understood the point. You can then look at the code of the Ada 2005
containers, to see how things are done "in real code". You can start
thinking what kinds of pre/post you would write for the Ada 2005
containers. You can also start writing functions without side effects
that correspond to the procedures that modify a container, as in
exercise 9 and 10.
