Re: Instantiating package problems

[Bob Duff <bobduff@theworld.com>]

Anh Vo <anhvofrcaus@gmail.com> writes:

> On Tuesday, January 5, 2016 at 7:31:00 PM UTC-8, Andrew Shvets wrote:
>> On Monday, January 4, 2016 at 3:49:32 PM UTC-5, Anh Vo wrote:
>> > On Sunday, January 3, 2016 at 4:07:30 PM UTC-8, Andrew Shvets wrote:
>> > > Hi Bob,
>> > > 
>> > > Thanks for writing back.  This is the entire example:
>> > > http://pastebin.com/GEJT3WzL
>> >  
>> > Just recommend to add a precondition to function Division as shown below. By the way, this feature is part of latest Ada (Ada 2012). In addition, you should think about adding precondition to other operations such as Addition where Input1 + Input2 <= Integer'Last and Input1 + Input2 >= Integer'Last. 
>> > 
>> >   function Division(
>> >     Input1 : in Integer;
>> >     Input2 : in Integer)
>> >       return Integer
>> >    with pre => Input2 /= 0;

I prefer predicates in a case like that:

    subtype Nonzero is Integer with Predicate => Nonzero /= 0;

And then Input2 can be of subtype Nonzero.  (Predicate is specific to
GNAT; use Static_Predicate if you want to conform to the Ada standard.)

>> I'm not sure that that worked.  I added it to my ads file and after
>> compilation and then re-running the application, this is what I got:
>> 
>> ....
>> 
>>  Division:        4
>> 
>> 
>> raised CONSTRAINT_ERROR : calculator.adb:33 divide by zero
>> 
>> Shouldn't the division function been prevented from running the actual division operation beforehand?
>
> The preconditions and postconditions are controlled by pragma
> Assertion_Policy. Thus, pragma Assertion_Policy(Check) must be added at the top
> of the package specification. Absent of this pragma is equivalent to pragma
> Assertion_Policy (Ignore). That means these conditions are ignored. By the way,
> ASSERTION_ERROR exception would be raised instead of CONSTRAINT_ERROR.

I wouldn't bother fooling about with Assertion_Policy.
Just use the -gnata switch.

If you do use Assertion_Policy, you probably want it in a global
configuration file, so it applies to all of your code.

- Bob