Dynamic predicate

We have seen that if we define properly the domain of our problem, we can make the Ada's type system to assist us to avoid bugs. We have seen how we can constrain values, but it isn't all. In fact we can also provide a dynamic predicate for our type (at least in Ada 2012). The dynamic predicate can check for some property of the type which the type system itself doesn't allow.

For example, we want a type which can hold only odd numbers. We do like this:

   subtype Odd_Number is Integer with 
     Dynamic_Predicate => Odd_Number mod 2 /= 0;

We are saying that the subtype Odd_Number stores integers, then we also say to check “dynamically” according to a predicate that must hold true. This can be done using a with clause which introduces an aspect, in this case the Dynamic_Predicate.

Note: if you want the compiler to compile the checks, you must enable asssertions. This is done using the compile time option -gnata. It can be done also using specific pragmas, but I haven't seen the details yet.

You can imagine correctly that all these checks slow down your program, so you surely keep them on during your tests, but likely you'll turn some off (not all…) when you'll release your final product.

The checks on a dynamic predicate are inserted by the compiler in these points:

• assignment
• passing the variable as input
• returning the variable as output (function or out parameters)
• conversion

Static predicate

Dynamic predicates are flexible and, as the name suggests, are checked dynamically, that is, when the program is running. But we can have also another aspect: Static_Predicate. This must be something that can be checked statically, so we are restricted to few kinds of predicates.

   type Animal is (Bear, Cat, Dog, Horse, Wolf);
   subtype Pet is Animal with
     Static_Predicate => Pet in Cat | Dog | Horse;

   My_Pet : Pet := Dog;

-- ...

   My_Pet := Bear;

The compiler can see that now we haven't our dog anymore: now we have a bear, which isn't a pet… The static predicate fails. But it's just a warning:

warning: static expression fails static predicate check on "Pet"

If we want the compilation to fail on warnings, we must use the switch -gnatwe.

The manual goes on discouraging the for given for the static predicate on Pet; this is because if we add another animal to the list, say, a rabbit, it won't be considered a pet if we forget to update the list in the static predicate. Therefore another form is suggested:

   subtype Pet2 is Animal with
     Static_Predicate => (case Pet2 is
                             when Cat | Dog | Horse => True,
                             when Bear | Wolf => False);

Why is this better? Because Ada requires that all the cases are covered. When we add Rabbit to Animal, the case doesn't handle all the possibilities anymore, and compilation fails.

This is another relevant aspect of safe programming. You may say: but I won't forget to add Rabbit to the subtype Pet, so there's no need to use the other form which forces me to exhaustively specify all the values, and I like more the other one, shorter, effective! This is the wrong attitude. There could be many reason why you, or someone on your team, add a Rabbit and forget to update the subtype Pet. With a little bit of discipline, you can make the compiler to help you to catch these glitches.

So, we add Rabbit but forget to update the case in the static predicate? Compilation fails:

missing case value: "Rabbit"

And we don't risk to treat a rabbit like a bear or a wolf. The source code dynamic_test.adb plays with these predicates.

Type invariant

Another interesting aspect we can tie to a type is type invariance. With the aspect Type_Invariant we say, basically, that each time the value is “visible”, the predicate specified in Type_Invariant must be true. That is, the value can be modified as you prefer, but in certain situation the check is performed. I've summarized these situation as “when the value is visible”, but these are my words to explain it briefly.

By analogy, think of a procedure which modify the value: until the value is handled inside the procedure, the type invariance isn't checked and you can do any computation you need. Once you give the value outside the function (using an out parameter), the predicate is checked and it must be true.

But Type_Invariant can be applied only to private type, so we must use it in a package.

   package Internal is
      type Unknown is private with
        Type_Invariant => Isnt_Bad_Luck (Unknown);
      
      function Isnt_Bad_Luck
        (S : Unknown) return Boolean;

      -- ...
      
   private
      type Unknown is new Integer;
      
   end Internal;

Then we can have a procedure which internally can use any value for a variable of type Unknown, but if it must give it outside, then the predicate of the invariant must hold.

A (silly) example in the file t_inv.adb.

Pre and post conditions

Since the first article I've shown Ada 2012 features which help to write contracts, so that you can prove your implementation is right according to a specification.

When we call a subprogram, we expect that the input values and the output values fulfil specific criteria. Types already do a big job so that you can define exactly the domain of your problem. But it is not all, and SPARK (and Ada 2012 alone, too) makes it possible to tell what you expect from a subprogram.

You do it in the specs, like this:

procedure Increment (A : in out Integer)
with 
  Post => A = A'Old + 1;

The attribute Old can be used to refer to the old value of a out variable. While if you have a function, the attribute Result refers to the returned value:

function Sum_Minus_One (A, B : Integer) return Integer
with
  Post => Sum_Minus_One'Result = A + B - 1;

We can use also preconditions, for example we can impose a certain relationship between two parameters:

function Positive_Diff (A, B : Integer) return Integer
with
  Pre => A > B;

According to the rationale on Ada 2012,

A precondition is an obligation on the caller to ensure that it is true before the subprogram is called and it is a guarantee to the implementer of the body that it can be relied upon on entry to the body.

And

A postcondition is an obligation on the implementer of the body to ensure that it is true on return from the subprogram and it is a guarantee to the caller that it can be relied upon on return.

So, in our example Positive_Diff, the implementer of the body of that function can ignore the case when A <= B, because it's the caller's duty to assure that A > B before calling the function.

Example source code: pre_post.adb.

Another very interesting example is this: suppose we have a procedure which sort in place an array. At the end of the procedure, the array must be sorted. We can state this as a postcondition, using for all.

procedure Sort (A : in out Int_Array)
with
  Post => (for all I in A'First .. A'Last - 1 => A (I) <= A (I+1))

The postcondition describes a property which must be true for all I in the given range, and this property is the one you have when an array is sorted, as you can easily see.

There is another “quantificator”, some which can be useful when we want to say that for some, but not necessarily all, values must hold a certain property. For example we could say that, as precondition to call Sort, the array must be unsorted. This is odd, but this is just an example...

procedure Sort (A : in out Int_Array)
with
  Pre => (for some I in A'First .. A'Last - 1 => A (I) > A (I+1)),
  Post => (for all I in A'First .. A'Last - 1 => A (I) <= A (I+1));

The precondition says this: for some I in the given range, the value at that index is greater than the next. It is enough that it is true for just one I, then the precondition is true (the array isn't sorted).

Of course we can't say for all, because in that case we were saying that the array must be in reverse order (greater values first), and also that there can't be two equal values, e.g., 10 9 8 7 would be ok, but 10 9 9 7 wouldn't.

Loop invariant

A loop invariant assertion must hold true at each iteration of a loop. It is specified at the beginning or at the end of a loop, like this:

   for I in 1 .. 10 loop
      for J in I + 1 .. I + 10 loop
         pragma Loop_Invariant (J > I);
         -- ...
      end loop;
   end loop;

This isn't very interesting because we can see that the condition is always true, and in fact the compiler agrees with a warning:

warning: condition is always True

Don't we want exactly that? Yes, but if we are stating the obvious, so that the compiler, at compile time, can see that there can't be cases when the condition isn't true; here, for example, the J loop starts from I+1, that is, there's no point in checking J > I.

A more “interesting” example, even if still nonsense, can be seen in the source file loopinv.adb.

Talking about loops

If you are a C or a C++ programmer, likely you've struggled with nested loops sometimes. The faster and cleaner way to break from a nested loop is using a goto; this is maybe the only case when using a goto is better than the alternatives. Unfortnately in C/C++ nobody accepted the idea to have a break statement which can break not just the enclosing loop, but also an outer loop.

In Ada loops can be labelled, and the keyword to exit from a loop is exit. When you label a loop, you must end it with end loop Name.

Reverse_Loop:
   for I in 1 .. 100 loop
      for J in 2*I .. 4*I loop
         -- ...
         exit Reverse_Loop when Condition (I, J);
         -- ...
      end loop;
   end loop Reverse_Loop;

Records and dynamic predicates

Records are what C/C++ calls structures, but C/C++ structures (not class-like, in the case of C++) have a simply deducible memory layout; the same can't be said for Ada's records.

Predicates can be applied to records too, and all we need is to use the type name as prefix, but they can only be dynamic: static predicates apply only to scalar or string types.

We've already seen examples like Person. We can modify it like this:

type Person is
   record
      Name     : U_String;
      Surname  : U_String;
      Birthday : Time;
      Deathday : Time;
      Alive    : Boolean;
      Married  : Boolean;
   end record
   with Dynamic_Predicate => Person.Alive
                             or else Person.Birthday < Person.Deathday;

If the person isn't alive, the Deathday must be in the future with resspect to the birthday. If the person is alive, the Deathday isn't meaningful and can be anything.

Now, let's populate a variable:

   Aldo : Person := (
                      Name => Us ("Al"),
                      Surname => Us ("Pachinko"),
                      Birthday => Time_Of (2018, 1, 20),
                      Deathday => Time_Of (2017, 1, 20),
                      Alive => True,
                      Married => False
                    );

The deathday comes before the birthday, but Alive is true, so it doesn't matter.

Let us suppose we do

   -- ...
   Aldo.Alive := False;
   -- ...

Nothing happens when we do this assignment, because the dynamic predicate isn't checked everytime, but only in certain circumstances. If we let our block (begin-end) to end when the variable holds values such that the dynamic predicate fails, then we have this error:

raised PROGRAM_ERROR : dynamic_test.adb:6 finalize/adjust raised exception

Behind the curtains, Ada calls special subprograms for a record to manage its memory and other things; this happens when exiting the block where the variable is in scope, and in this case the subprogram is Finalize, or when the record gets assigned, and in this case the subprogam is Adjust.

The error suggests that the dynamic predicate is checked when one of these function is called, but not when one of the value of the members is changed. So,

-- ...
begin
   Aldo.Alive := False;
   Put_Line ("We are here");
end;

When the program hits end, the Finalize subprogram is called for Aldo, and the dynamic predicate is then checked, raising the exception. If we adjust things so that Aldo is ok just before the end, no exception is raised:

-- ...
begin
   Aldo.Alive := False;
   Put_Line ("We are here");
   Aldo.Deathdate := Time_Of (2019, 6, 2);
end;

In both cases we read the string We are here in the console, because the exception isn't raised on the assignment Aldo.Alive := False, even if this makes false the dynamic predicate.

But the same thing happens if we call a subprogram of our own:

-- ...
begin
   Aldo.Alive := False;
   Massage_Person (Aldo);
   Put_Line ("We are here");
   Aldo.Deathdate := Time_Of (2019, 6, 2);
   -- now Aldo is ok, but we don't reach this point!
end;

In this case We are here isn't reached, because the exception is raised when we call Massage_Person.

So, when we enter or leave a subprogram, the dynamic predicates of any record type must be true.

The dynamic predicate must be true also when we copy the variable:

   Copy_Of_Aldo : Person;
-- ...
begin
   Aldo.Alive := False;
   Copy_Of_Aldo := Aldo;
   Aldo.Alive := True;
   Put_Line ("Al's ok!");
end;

The exception is raised on the assignment, hence the Al's ok! string won't be written to the output. The assignment doesn't need to be a copy of an existing variable; it can be also a brand new assignment from a fresh Person type:

   Aldo := (Name => Us ("Aldebaran"),
            Surname => Us ("Pax"),
            Birthday => Aldo.Birthday,
            Deathday => Aldo.Deathday,
            Alive => False,
            Married => True);

All this is consistent with what we've already seen in general on the checkpoints inserted by the compiler, and in particular for

• assignment
• passing the variable as input

With the note that for a record the assignment is considered only for the whole variable and not when you change a member's value (in this case, if the member is of a subtype with a dynamic predicate, this one would be the checked one!)

The source code for these tests is again dynamic_test.adb. A screenshot of my editor while editing that source code follows, just to give an image for this post.