Search code examples
adadesign-by-contract

How can I have more information in a Predicate_Failure?


I want to be able to include information about my type in the Predicate_Failure message. Here's what I have that works:

subtype Norm is Float range 0.0..1.0;
type Component is (Red, Green, Blue, Yellow, White);

type Proto_Color is array(Component'Range) of Norm;

function Is_Valid(This : Proto_Color) return Boolean is
    Positive_Count : Natural := 0;
    Sum : Norm := 0.0;
begin
    for I in Component'Range loop
        if This(I) > 0.001 then 
            Positive_Count := Positive_Count + 1;
            Sum := Sum + This(I);
        end if;
    end loop;
    if Positive_Count = 0 or Positive_Count > 2 then
        return False;
    end if;
    if This(Red) > 0.001 and then This(Green) > 0.001 then
        return False;
    end if;
    if This(Yellow) > 0.001 and then This(Blue) > 0.001 then
        return False;
    end if;
    return Sum > 0.999 and then Sum < 1.001;
end Is_Valid;

Invalid_Color : exception;

type Color is new Proto_Color with Dynamic_Predicate => Is_Valid(Proto_Color(Color)), 
    Predicate_Failure => raise Invalid_Color;

Note that the Proto_Color type only exists so I can add that Dynamic_Predicate. I couldn't find a way to declare that Is_Valid function on a type that wasn't complete yet.

What I want to do, because all this tells me is that it failed, is have some more information about the type displayed along with the exception. But I can't get it to accept a function call on the Predicate_Failure:

function To_String(This : Proto_Color) return String is
begin
    return "Red => " & Norm'Image(This(Red)) 
        & ", Green => " & Norm'Image(This(Green)) 
        & ", Blue => " & Norm'Image(This(Blue)) 
        & ", Yellow => " & Norm'Image(This(Yellow)) 
        & ", White => " & Norm'Image(This(White));
end To_String;

type Color is new Proto_Color with Dynamic_Predicate => Is_Valid(Proto_Color(Color)), 
    Predicate_Failure => raise Invalid_Color with To_String(Proto_Color'(Color));

The error I get with this is:

expected type "Proto_Color" defined at line [line number]
found type "Color" defined at line [line number]

Without the tick that makes it a qualified expression, it tells me:

the argument of conversion cannot be aggregate
use a qualified expression instead

Solution

  • What’s needed is judicious use of subtypes, and realisation that you can call a function in a predicate before writing the spec (can’t immediately see where this is discussed in the ARM).

    This works (GCC 13.2.0, 14.0.1):

    procedure Devsman is
    
       package Colors is
          subtype Norm is Float range 0.0 .. 1.0;
          type Component is (Red, Green, Blue, Yellow, White);
    
          type Proto_Color is array (Component'Range) of Norm;
    
          Invalid_Color : exception;
    
          subtype Color is Proto_Color with
            Dynamic_Predicate => Is_Valid (Color),
            Predicate_Failure => raise Invalid_Color with To_String (Color);
    
          function Is_Valid (This : Proto_Color) return Boolean;
          function To_String (This : Proto_Color) return String;
    
        end Colors;
    
       package body Colors is
    
          function Is_Valid (This : Proto_Color) return Boolean is
             Positive_Count : Natural := 0;
             Sum            : Norm    := 0.0;
          begin
             for I in Component'Range loop
                if This (I) > 0.001 then
                   Positive_Count := Positive_Count + 1;
                   Sum            := Sum + This (I);
                end if;
             end loop;
             if Positive_Count = 0 or Positive_Count > 2 then
                return False;
             end if;
             if This (Red) > 0.001 and then This (Green) > 0.001 then
                return False;
             end if;
             if This (Yellow) > 0.001 and then This (Blue) > 0.001 then
                return False;
             end if;
             return Sum > 0.999 and then Sum < 1.001;
          end Is_Valid;
    
          function To_String (This : Proto_Color) return String is
          begin
             return
               "Red => " & Norm'Image (This (Red)) & ", Green => " &
               Norm'Image (This (Green)) & ", Blue => " &
               Norm'Image (This (Blue)) & ", Yellow => " &
               Norm'Image (This (Yellow)) & ", White => " &
               Norm'Image (This (White));
          end To_String;
    
       end Colors;
    
       C : Colors.Color;
    begin
       C := (0.0, 0.0, 0.0, 0.0, 0.0);
    end Devsman;
    

    I have to admit to a certain amount of hacking to arrive at this :-(