This tutorial talks about a powerful bug trap that was introduced in Ada 2012: the Type_invariant attribute.

Type invariant? What's that?

The idea of type invariant is pretty simple. Sometimes data structure are quite simple, just an aggregation of values, but often they are quite complex with an internal structure that needs to be preserved.

A type invariant associated to a given type is a Boolean expression that is true for every valid value of the type. Ada allows the association of a type invariant to a private type; the compiler — if instructed so — will insert code that checks that the invariant remains satisfied; if not, an exception will be raised.

An example: a table with two keys

Let's do a simple example. Suppose that

• We have a set of users
• Every user has a Serial_ID (a 6 digit number) and a SSN (Social Security Number). We will assume the Italian convention where the SSN is a 16 character string.
• Both the Serial_ID and SSN identify uniquely the user, that is, there are no two users with the same Serial_ID nor two users with the same SSN.
• We want to build a data structure User_Directory that will allow us to get (efficiently) an user both by Serial_ID and SSN

A possible solution is shown in the figure

The data structure is made of two Ordered_Maps: one map is indexed by the Serial_ID, the other one by the SSN and both maps store pointers (access values in Ada jargon) to a User_Record, a record that contains the user information. This structure clearly introduces some (quite obvious) redundancy

• The SSN stored in a User_Record must be equal to the corresponding key in the SSN_Map, the same for the Serial_ID
• The entries of the two maps corresponding to the same user must map to the same record
• The two maps have the same number of entries.

The spec file

This is an excerpt of the public part of the spec file (roughly the *.h of C)

   subtype ID_Char is Character range '0' .. '9';
   type Serial_ID is array (1 .. 6) of ID_Char;

   type User_SSN is new String (1 .. 16);

   type User_Directory is private;

   procedure Add_User (Dir : in out User_Directory;
                       ID  : in Serial_ID;
                       SSN : in User_SSN)
     with
       Pre => not Contains (Dir, Id) and not Contains (Dir, Ssn),
     Post =>  Contains (Dir, Id) and Contains (Dir, Ssn);


   procedure Delete (Dir : in out User_Directory;
                     ID  : in Serial_ID)
     with
       Pre => Contains (Dir, Id),
     Post =>  not Contains (Dir, Id);

Here we define

• The types Serial_ID and User_SSN as fixed lenght strings. Note that Serial_ID can contain only digits.
• User_Directory is the data structure we are defining.
• Add_User and Delete should be quite obvious. Note the use of preconditions (after Pre =>) and postconditions (after Post =>) that document the behavior of Add_User and Delete.

The actual definition (in the private part) of User_Directory is basically the translation in Ada of the scheme shown above

 type User_Record is
      record
         ID  : Serial_ID;
         SSN : User_SSN;
      end record;

   type User_Record_Pt is access User_Record;

   package ID_To_User_Maps is
     new Ada.Containers.Ordered_Maps (Key_Type     => Serial_ID,
                                      Element_Type => User_Record_Pt);

   package SSN_To_User_Maps is
     new Ada.Containers.Ordered_Maps (Key_Type     => User_SSN,
                                      Element_Type => User_Record_Pt);

   type User_Directory is
      record
         ID_To_User  : ID_To_User_Maps.Map;
         SSN_To_User : SSN_To_User_Maps.Map;
      end record;

We have

• The record User_Record holding the user information and its access User_Record_Pt
• A package ID_To_User_Maps (obtained by specializing the generic standard package Ordered_Maps) that implements maps that associate User_ID to access to User_Record
• A similar package SSN_To_User_Maps
• Finally, we have the User_Directory that simply contains the two required maps.

The implementation

Let's look at the implementation of the package. Let's start with Add_User.

 procedure Add_User
     (Dir : in out User_Directory; 
      ID  : in Serial_ID; 
      SSN : in User_SSN)
   is
      New_User : User_Record_Pt;
   begin
      if Dir.ID_To_User.Contains (ID) then
         raise Constraint_Error;
      end if;

      New_User  := new User_Record'(ID, SSN);

      Dir.ID_To_User.Include (Key      => Id,
                              New_Item => New_User);


      Dir.SSN_To_User.Include (Key      => SSN,
                               New_Item => New_User);
   end Add_User;

The implementation of Add_User is quite straightforward: with

New_User  := new User_Record'(ID  => ID, SSN => SSN);

we allocate dynamically a record with the user information and with

   Dir.ID_To_User.Include (Key      => Id,
                           New_Item => New_User);


   Dir.SSN_To_User.Include (Key      => SSN,
                            New_Item => New_User);

we update the two internal tables by associating the given ID and SSN with the address of the newly allocated record.

This is our first tentative to the implementation of Delete.

procedure Delete (Dir : in out User_Directory; ID : in Serial_ID) is
      To_Be_Removed : User_Record_Pt := Dir.ID_To_User (Id);
   begin
      Dir.ID_To_User.Delete (Id);

      Free (To_Be_Removed);
   end Delete;

This implementation has a bug 🐛, as it is clear from this figure that pictures the behavior of Delete.

The dashed line means that the memory area of the user record now has gone back to the heap. It is clear that we forgot to remove the entry from Dir.SSN_To_User and now we have a dangling pointer referring to the old user record.

This is a nasty bug.

Oh, yes, believe me. I have already seen this movie, actually I was the main character. What could go wrong? Well, for example, later you could want to update the entries of Dir.SSN_To_User in some way. However, the memory that was assigned to the user record now belongs to some other structure that will be corrupted by your update.

Depending on your code, the bug can remain dormant for long time, then, suddenly, one day, if you are lucky, you get a SEGFAULT when you try to use the corrupted structure again. If you are unlucky you'll get funny random behaviors, possibly difficult to replicate.

Even if you are lucky (so to say...) you'll get the SEGFAULT in a place totally unrelated with the real bug in Delete. Believe me, finding this bug can take days of stumbling around in the dark. Not even an army of rubber ducks can save you.

Although this is a specific example, this kind of time bomb 💣 (or Sword of Damocles) behavior is typical of bugs that cause a loss of internal coherence in some complex structure. The bug will not manifest itself when the structure is corrupted, but later as a delayed consequence of the loss of coherence, making bug hunting difficult.

Remember: there is one thing worse than a bug that causes a crash: a bug that causes the program to continue as nothing happened.

The solution: type invariant

Fear not, my friends and colleagues. Ada comes to the rescue with the Type_Invariant. It suffices to add it to the type definition as in

type User_Directory is
      record
         ID_To_User  : ID_To_User_Maps.Map;
         SSN_To_User : SSN_To_User_Maps.Map;
      end record
    with Type_Invariant => Is_Coherent (User_Directory);

where Is_Coherent is a function that checks that the whole structure is coherent, that is, that the two maps have the same number of entries and that the data in the user record match the corresponding key in the tables. The source code of the (fairly long) function is included, for reference, at the end of this post.

Now if we run the following test program

with User_Directories;   use User_Directories;

procedure Main is
   Dir : User_Directory;
begin
   Add_User (Dir => dir,
             ID  => "123456",
             SSN => "ABCDEF64X12Q456R");

   Add_User (Dir => dir,
             ID  => "654321",
             SSN => "XBCDEF64X12Q456R");

   Delete (Dir, Id => "123456");
end Main;

we get the following results

Execution of obj/main terminated by unhandled exception
raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : 
  failed invariant from user_directories.ads:65
Call stack traceback locations:
⋯/s-assert.adb:46
⋯/adainclude/a-coorma.adb:1561
⋯/user_directories.adb:52
⋯/user_directories.adb:59
⋯/main.adb:18
⋯

where, for the sake of readability I replaced part of the dump text with ⋯. The line

failed invariant from user_directories.ads:65

refers to the line where type User_Directory is declared. In the stack dump the first two lines refer to some system files, we are interested in the third line

⋯/user_directories.adb:52

that refers to the first line of procedure Delete.
Summarizing,

• Before calling Delete user directory Dir was fine
• After calling Delete it is not fine anymore, who are you gonna blame?

Ghostbusters! No, sorry, wrong citation... 😊😛 (this is also a hint to my age... 😊)

After a brief inspection of Delete we discover the problem and we fix it quite easily

procedure Delete (Dir : in out User_Directory; ID : in Serial_ID) is
      To_Be_Removed : User_Record_Pt := Dir.ID_To_User (Id);
   begin
      Dir.SSN_To_User.Delete (To_Be_Removed.SSN); -- New line
      -- and here???
      Dir.ID_To_User.Delete (Id);

      Free (To_Be_Removed);
   end Delete;

Wait a minute...

Someone maybe could observe that at the line -- and here??? the variable Dir is in a non coherent state since we updated one table, but not the other. The same happen in the Add_User procedure. Wouldn't this raise an exception?

Well, no. The details are a bit complex, but the basic idea is that since Add_User and Delete are declared in the same package of User_Directory, they are able to operate on the internal structure of the type and it is acceptable that during this manipulation the internal structure is not coherent for a moment. The type invariant will be checked only when the procedures end;
see the Reference manual if you want every single, gory, detail...

Appendix

Implementation of Is_Coherent

function Is_Coherent (Dir : User_Directory) return Boolean is
      use Ada.Containers;
      use ID_To_User_Maps;
      use SSN_To_User_Maps;
   begin
      if Dir.ID_To_User.Length /= Dir.SSN_To_User.Length then
         return False;
      end if;

      for Pos in Dir.ID_To_User.Iterate loop
         declare
            Usr_Entry : constant User_Record_Pt := Element (Pos);
         begin 
            if Usr_Entry /= Dir.SSN_To_User (Usr_Entry.Ssn) then
               return False;
            end if;

            if Key (Pos) /= Usr_Entry.Id then
               return False;
            end if;
         end;         
      end loop;

      return True; 
   end Is_Coherent;

Credits

• The image of Gollum is a modified version of the wikipedia image
• The scolopendra image is available with license CC BY 4.0 as figure of this paper

Introduction

SPARK/Ada is a language derived from Ada that allows for a formal checking (i.e., mathematically prove the correctness) of the software. Several types of checks can be done: from the absence of runtime exceptions to no use of uninitialized variables, up to the formal proof that a given procedure/function fulfills its contract.

I like formal checking because it can actually prove that your program is correct (or that, at least, some kind of errors are absent), something that is usually not possible with testing. Of course, formal checking cannot applied to every program, but when it is possible it is a very powerful tool.

SPARK/Ada is definitively on my list of stuff that I want to learn.

Recently I had to write a procedure for a binary search in an ordered array. I thought that it could be an interesting exercise to write it in SPARK/Ada in order to have it formally verified. This is a brief summary of this experience, written with a tutorial spirit.

The requirements

The problem I want to solve is the following

• INPUTS
  • Table: an array of Float sorted in strictly increasing order (that is, Table(n+1) > Table(n) for every n).
  • What : a Float such that
    • it is included between the array extremes, that is, Table(Table'First) ≤ What ≤ Table(Table'Last), but
    • it is not necessarily in Table, that is it is not required that there is n such that Table(n) = What
• OUTPUTS
  • The unique index n such that

Table(n) ≤ What < Table(n+1)

The solution

The spec file

First basic draft of specs

Let's first flesh out the spec file (roughly [very roughly] similar to a *.h file for you C people).

pragma SPARK_Mode (On);

package Searching is
   subtype Element_Type is Float;
   subtype Index_Type is Natural;

   type Array_Type is 
      array (Index_Type range <>) of Element_Type;

   function Find (What  : Element_Type;
                  Table : Array_Type)
                  return Index_Type;
end Searching;

Entering SPARK Mode

The first line we encounter is

pragma SPARK_Mode (On);

This claims that this package will be compatible with SPARK restrictions and conventions. The lines

   subtype Element_Type is Float;
   subtype Index_Type is Natural;

define Element_Type and Index_Type as synominous of Float and Index_Type, respectively. This is not strictly necessary, but it can make it easier to change the types in a future

Function declaration

 function Find (What  : Element_Type;
                Table : Array_Type)
                return Index_Type;

should be clear enough.

Introducing contracts

In order for SPARK to be able to proof that our implementation of Find is correct, we need to describe to SPARK what we expect Find to do. This is done by means of a contract. Like a normal contract between people, a function contract usually has two parts: preconditions and postconditions.

The idea is that if you (the caller) do your part (i.e. you meet the preconditions when you call me), then I, the function, promise to do my part, that is, that the result will satisfy the post-conditions.

If a contract is given, I can ask SPARK to prove that the post-conditions follow from the pre-conditions. If SPARK succeeds, I know that the code I wrote is correct (in the sense that it respects the contract) without doing any test: I have a mathematical proof for it.

BTW, contracts are very useful even if you are not using SPARK. First, they are a wonderful "bug trap." By using the right options, you can ask the compiler to insert code that checks the pre-conditions when the function is called and the post-conditions when the function ends. If pre/post-conditions are not met, an exception is raised.

Moreover, contracts document in a formal and unambiguous way the behavior of the function and, differently from usual comment-based documentation, cannot go out of sync with the code.

OK, so contracts are cool. How do we write the contract for our function? Well, let's start with the precondition and let's check the specs. It is said that (i) Table must be sorted and (ii) What must be between Table extrema; we just translate that in Ada in this way

    function Find (What  : Element_Type;
                  Table : Array_Type)
                  return Index_Type
     with
       Pre =>
          Is_Sorted (Table)
          and Table (Table'Last) >= What
          and What >= Table (Table'First);

where Is_Sorted is a function that checks if its argument is sorted and defined as follows

function Is_Sorted (Table : Array_Type) return Boolean
   is (for all L in Table'Range =>
         (for all M in Table'Range =>
            (if L > M then Table (L) > Table (M))))
   with Ghost;

The body of the function (this form is called expression function) is the translation in Ada of the definition of monotonic array.

Note the with Ghost in the definition. This says that Is_Sorted is a ghost function, that is, a function that can be used only in contracts or assertions; if used in other places ("real code") an error is raised. (I love this kind of protections ♥)

The preconditions look right and they represent the actual specs, but if we try to run SPARK we get an error

medium: array index check might fail

at line

      and What >= Table (Table'First);

This means that Table'First, that is the first index of the array, can be ... outside array bounds? The first index is by definition within the bounds, right?

Go home SPARK, you're drunk...

Well... Actually, SPARK is right. If you ask for a counterexample you get

e.g. when Table'First=1 and Table'Last=0

Now, when in the world can be possible that the last index is smaller than the first one?!? Well, if Table is empty... Empty arrays in Ada have the last index smaller than the first one. Therefore, trying to access Table (Table'First) would cause an error.
Well, SPARK, good catch...

Well, I agree (although it could happen because of an error), but SPARK does not know it. To make SPARK happy it suffices to add Table'Length > 0 to the precondition to get

    function Find (What  : Element_Type;
                  Table : Array_Type)
                  return Index_Type
     with
       Pre => Table'Length > 0
              and then (Is_Sorted (Table)
                        and Table (Table'Last) >= What
                        and What >= Table (Table'First));

Now SPARK is happy and even the casual user sees that you cannot call the function with an empty table.

The postcondition

Also for the post-conditions we translate directly the requirement from English to Ada. It is required that What is between Table(n) and Table(n+1) where n is the value returned by the function. In Ada we get

         (if Find'Result = Table'Last then
             Table (Find'Result) = What
          else
             Table (Find'Result) <= What 
         and What < Table (Find'Result + 1));

Note that Find'Result is the value returned by Find and that we consider as special case Find'Result = Table'Last since in this case there is no "following entry" in Table. Overall, the function declaration with the full contract is

   function Find (What  : Element_Type;
                  Table : Array_Type)
                  return Index_Type
     with
       Pre => 
          Table'Length > 0
          and then (Is_Sorted (Table)
                    and Table (Table'Last) >= What
                    and What >= Table (Table'First)),
       Post =>
         (if Find'Result = Table'Last then
             Table (Find'Result) = What
          else
             Table (Find'Result) <= What 
         and What < Table (Find'Result + 1));

The body file (implementation)

The algorithm

The algorithm for a binary search is well known and exemplified in the following picture

Basically, we keep two "cursors" in the table: Bottom and Top with the condition that it must always be

Table(Bottom) ≤ What < Top(top)

We get the Middle point between Top and Bottom and if Table(Middle) is too large we move Top to Middle, otherwise we move Bottom. We iterate this until on of the following two conditions holds

• Table(Bottom) = What, that is, we actually found What in Table
• Top = Bottom+1 there are no intermediate entries between Top and Bottom

In both cases we return Bottom

The actual code

Let's start with a basic skeleton of the procedure.

function Find (What : Element_Type; Table : Array_Type) return Index_Type
   is
      Bottom : Index_Type;
      Top    : Index_Type;
      Middle : Index_Type;
   begin
      if Table (Table'Last) = What then
         return Table'Last;
      end if;

      Bottom := Table'First;
      Top    := Table'Last;

      pragma Assert (Table (Top) > What and What >= Table(Bottom));

      while Table (Bottom) < What and Top - Bottom > 1 loop
         Middle := (Bottom + Top)/2;

         if Table (Middle) > What then
            Top := Middle;
         else
            Bottom := Middle;
         end if;
      end loop;

      return Bottom;
   end Find;

It is just a translation of the algorithm informally described above. Note how the special case Table (Table'Last) = What is handled separately; in this way we know that

Table (Top) > What and What >= Table(Bottom)

holds (see the pragma Assert).

Now, in order to make it easier for SPARK to prove the correctness of the code we insert in the code some pragma Assert claiming properties that hold true in different points of the code.

Automatic theorem proving is not easy and some hint to the prover can help. Moreover, I love spreading generously my code with assertion since they help understanding what the code does and which properties I expect to be true. They are also formidable "bug traps".

The function body with all the assertions looks like

function Find (What : Element_Type; Table : Array_Type) return Index_Type
   is
      Bottom : Index_Type;
      Top    : Index_Type;
      Middle : Index_Type;
   begin
      if Table (Table'Last) = What then
         return Table'Last;
      end if;

      pragma Assert (Table (Table'Last) > What);

      Bottom := Table'First;
      Top    := Table'Last;

      pragma Assert (Bottom < Top);
      pragma Assert (Table (Bottom) <= What and What < Table (Top));

      while Table (Bottom) < What and Top - Bottom > 1 loop

         pragma Loop_Invariant (Bottom >= Table'First);
         pragma Loop_Invariant (Top <= Table'Last);
         pragma Loop_Invariant (Top > Bottom);
         pragma Loop_Invariant (Table (Bottom) <= What and What < Table (Top));
         pragma Loop_Variant (Decreases => Top - Bottom);

         Middle := (Bottom + Top)/2;
         pragma Assert (Bottom < Middle and Middle < Top);

         if Table (Middle) > What then
            Top := Middle;
         else
            Bottom := Middle;
         end if;
      end loop;

      pragma Assert (Table (Bottom) <= What and Table (Bottom + 1) > What);
      return Bottom;
   end Find;

There are just two points worth describing; the first is this sequence of pragmas inside the loop

pragma Loop_Invariant (Bottom >= Table'First);
pragma Loop_Invariant (Top <= Table'Last);
pragma Loop_Invariant (Top > Bottom);
pragma Loop_Invariant (Table (Bottom) <= What 
                       and What < Table (Top));
pragma Loop_Variant (Decreases => Top - Bottom);

pragmas Loop_Invariant and Loop_Variant are specific to SPARK. A loop invariant is a condition that is true at every iteration and you can see that this loop invariant is a formalization of what we said before: at every iteration What is between Top and Bottom. Loop invariants are important in the proof of correctness of while loops.

A while loop can potentially go on forever; a technique that allows us to prove that the loop will terminate is to search for some value that always increases (or decreases) at every iteration; if we know a bound for this value (e.g., it is always positive and it always decreases) we can deduce that the loop will terminate. The pragma Loop_Variant allows us to declare said value. In this case the distance between Top and Bottom is halved at every iteration, therefore it is a good variant. Since Top-Bottom cannot be smaller than 2 (see condition in the while), we deduce that the loop will terminate.

A second observation is about seemly innocuous line

 Middle := (Top + Bottom) / 2;

Here SPARK complains with

medium: overflow check might fail 
(e.g. when Bottom = Index_Type'Last-4 and Top = Index_Type'Last-2)

Good catch! Here SPARK is observing that although theoretically Middle should be in the range of representable integers if Top and Bottom are, there is a possibility of an overflow while doing the sum. Since on my PC Index_Type'Last = 2^63-1, it is unlikely that one would work with tables so big, nevertheless...

We have two solutions: (i) allow a smaller range of integers (that is, up to Index_Type'Last/2) or (ii) compute the mean with function

function Mean (Lo, Hi : Index_Type) return Index_Type
is (Lo + (Hi - Lo) / 2)
   with
     Pre  => Lo < Index_Type'Last and then Hi > Lo + 1,
     Post => Hi > Mean'Result and Mean'Result > Lo;

that is guaranteed to have no overflow. Note that in the precondition we require that Hi > Lo + 1, this is guaranteed by the loop condition and it is necessary in order to guarantee that the post conditions hold which in turn guarantees that the loop variant decreases at every iteration.

Finally...

OK, now if we run SPARK we get

Summary of SPARK analysis
=========================

-------------------------------------------------------------------------------------------------------
SPARK Analysis results        Total      Flow   Interval   CodePeer      Provers   Justified   Unproved
-------------------------------------------------------------------------------------------------------
Data Dependencies                 .         .          .          .            .           .          .
Flow Dependencies                 .         .          .          .            .           .          .
Initialization                    3         3          .          .            .           .          .
Non-Aliasing                      .         .          .          .            .           .          .
Run-time Checks                  29         .          .          .    29 (CVC4)           .          .
Assertions                       14         .          .          .    14 (CVC4)           .          .
Functional Contracts              3         .          .          .     3 (CVC4)           .          .
LSP Verification                  .         .          .          .            .           .          .
-------------------------------------------------------------------------------------------------------
Total                            49    3 (6%)          .          .     46 (94%)           .          .

Do you see on the extreme right the column Unproved with no entries? That is what I want to see... SPARK was able to prove everything, so now you can kick back, relax and enjoy your binary search function with confidence: you made terra bruciata (scorched earth) around it and no bug can survive.