Reasons for loving Ada: Type invariants (because bugs shouldn't sleep...)
Tags: typeinvariant, strongtyping, tutorial, ada
Published: 2020-07-19 14:30:05

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

![Two table pointing to the same record](https://dev-to-uploads.s3.amazonaws.com/i/em3jf1qtr6cx0ob0ddgl.png)

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)

```ada
   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

```ada
 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`. 

```ada
 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 

```ada
New_User  := new User_Record'(ID  => ID, SSN => SSN);
```
we allocate dynamically a record with the user information and with 

```ada
   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`. 

```ada
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`.

![Entry deleted from only one table](https://dev-to-uploads.s3.amazonaws.com/i/sptmeiwy5hm6lu0dwv6w.png)

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.

![Gollum with a scolopendra saying it is a nasty bug](https://dev-to-uploads.s3.amazonaws.com/i/zcvhxxe0s92eya0272n2.png)
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](https://en.wikipedia.org/wiki/Segmentation_fault) 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.

![Army of rubber ducks](https://dev-to-uploads.s3.amazonaws.com/i/jphkmppxi00vc0099mxg.png)

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](https://blog.codinghorror.com/whats-worse-than-crashing/). 

## 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 

```ada
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

```ada
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

```text
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 

```term
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
```term
⋯/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... 😊)

![Judge finds Delete guilty of data structure damage](https://dev-to-uploads.s3.amazonaws.com/i/ejlmpd17zfnc9j6yzigw.png)

After a brief inspection of `Delete` we discover the problem and we fix it quite easily
 
```ada
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](https://www.adaic.org/resources/add_content/standards/12rm/html/RM-7-3-2.html#I3612) if you want every single, gory, detail...

# Appendix 

## Implementation of `Is_Coherent`

```ada
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](https://commons.wikimedia.org/wiki/File:Gollum_at_Wellington_Airport.jpg)
* The scolopendra image is available with license CC BY 4.0 [as figure of this paper](https://www.researchgate.net/publication/266085751_The_Evolutionary_History_of_the_Rediscovered_Austrian_Population_of_the_Giant_Centipede_Scolopendra_cingulata_Latreille_1829_Chilopoda_Scolopendromorpha/figures?lo=1)