Specifying exception raised at pre/postcondition failures

General
1

Hi, how do you specify the exception raised by a pre/post-condition failures, as well as other contracts ?
It seems to me it should be useful, but I can’t find it.
I’m just trying to get into the habit of specifying every logical property I can think of.

2

I usually do it in the pre/post condition itself:

with Ada.Text_IO; use Ada.Text_IO;
with Ada.Assertions; use Ada.Assertions;

procedure jdoodle is
    pragma Assertion_Policy(Check);
    
    Condition : constant Boolean := False;
    Custom_Exception : exception;
    
    procedure Do_Something
        with Pre => 
            (if Condition then 
                True 
             else 
                raise Custom_Exception with "Failed Pre check" );
                        
    Procedure Do_Something is
    begin
        Put_Line("In Do_Something");
    end;
    
begin
    Do_Something;
exception
    when Assertion_Error  => Put("Assertion - ");  raise;
    when Custom_Exception => Put("Custom - ");     raise;
end jdoodle;

Output:

Custom - 
raised JDOODLE.CUSTOM_EXCEPTION : Failed Pre check
3

but if Custom_Exception is raised, isn’t the precondition still validated though, in the eyes of automated tools ?

4

I’m not a spark expert but my understanding is the precondition is checked by the solver and would alert you. Should be easy to test.

Plus raising an exception there is valid ada so any tools should properly handle it. If not you should let the tool vendor know.

5

The normal way:

procedure P with Pre => C or else raise E;
4 Likes
6

Okay I read specifically that reaching those branches of the expression with raise is considered a failure of the post/precondition, so the tools will try to prove they are never reached.
This is what I supposed.

7

The item you’re probably looking for is the Predicate_Failure aspect.

Type Serial_Number is new String(1..7)
  with Dynamic_Predicate => (for all C of Serial_Number => C in '0'..'9'),
       Predicate_Failure => raise Constraint_Error 
         with "Invalid character in string: '" & String(Serial_Number) & "'.;
3 Likes
8

it is specific to subtype predicates though.