Aspect programming

Aspect programming

[Anh Vo]

If I understand the ARM 2012 and Ada 2012 Rationale correctly, the
following test code should raise Ada.Assertions.Assertion_Error.
However, Stack_Error is raised instead. I am using GNAT-GPL-2011. Is
it my bug or compiler's bug?


pragma Assertion_Policy (Check);
--  pragma Check_Policy (Postconditions, On);
--  pragma Check_Policy (Preconditions, On);

with Ada.Assertions;
with Ada.Text_Io;
with Ada.Exceptions;
with Stacks;

procedure Aspect_Programming_Test is

   use Ada;
   use Text_Io;

   package Int_Stacks is new Stacks (Integer);
   My_Int_Stack : Int_Stacks.Stack;
   My_Int : Integer := -1;

begin
   Put_Line ("Learning Aspect-Oriented Software Programming");

   for Index in 1 .. 10 loop
      My_Int_Stack.Push (Index);
   end loop;

   Put_Line ("Next Push operation will trigger Stack Full problem /
exception");
   My_Int_Stack.Push (1);

   for Index in 1 .. 10 loop
      My_Int_Stack.Pop (My_Int);
   end loop;

   Put_Line ("Next Pop operation will trigger Stack Empty problem /
exception");
   My_Int_Stack.Pop (My_Int);

exception
   when Ada.Assertions.Assertion_Error =>
      Put_Line ("Pragma Assertion_Policy is in effect");

   when Error : Int_Stacks.Stack_Error =>
      Put_Line ("Pragma Assertion_Policy is ignored");
      Put_Line (Exceptions.Exception_Information (Error));

   when Error : others =>
      Put_Line ("Let's see what is going on => ");
      Put_Line (Exceptions.Exception_Information (Error));

end Aspect_Programming_Test;

generic
   type Item is private;
   Size : Positive := 10;
package Stacks is

   type Stack is tagged private;

   function Is_Empty (S : Stack) return Boolean;

   function Is_Full (S : Stack) return Boolean;

   procedure Push (S : in out Stack;
                   X : in     Item)
      with Pre => not Is_Full (S),
           Post => not Is_Empty (S);

   procedure Pop (S : in out Stack;
                  X :    out Item)
      with Pre => not Is_Empty (S),
           Post => not Is_Full (S);

   Stack_Error: exception;

private

   type Data_Array is array (Natural Range 1 .. Size) of Item;

   type Stack is tagged record
      Data : Data_Array;
      Index : Positive := 1;
   end record;

   function Current_Items (S : Stack) return Natural;

end Stacks;

pragma Assertion_Policy (Check);

package body Stacks is

   protected Mutex is -- Mutex object section starts
      entry Take;
      procedure Release;
   private
      Resource_Available : Boolean := True;
   end Mutex;
   protected body Mutex is
      entry Take when Resource_Available is
      begin
         Resource_Available := False;
      end Take;

      procedure Release is
      begin
         Resource_Available := True;
      end Release;
   end Mutex;  -- Mutex object section ends

   function Is_Empty (S : Stack) return Boolean is
      Condition : Boolean := True;
   begin
      Mutex.Take;
      Condition := S.Index = 1;
      Mutex.Release;
      return Condition;
   end Is_Empty;

   function Is_Full (S : Stack) return Boolean is
      Condition : Boolean := True;
   begin
      Mutex.Take;
      Condition := S.Index = Size + 1;
      Mutex.Release;
      return Condition;
   end Is_Full;

   procedure Push (S : in out Stack;
                   X : in     Item)  is
   begin
      Mutex.Take;
      if S.Index = Size + 1 then
         Mutex.Release;
         raise Stack_Error with "Stack is full!!!";
      end if;
      S.Data(S.Index) := X;
      S.Index := S.Index + 1;
      Mutex.Release;
   end Push;

   procedure Pop (S : in out Stack;
                  X :    out Item)  is
   begin
      Mutex.Take;
      if S.Index = 1 then
         Mutex.Release;
         raise Stack_Error with "Stack is empty!!!";
      end if;
      S.Index := S.Index - 1;
      X := S.Data(S.Index);
      Mutex.Release;
   end Pop;

   function Current_Items (S : Stack) return Natural is
      Items_Count : Natural := 0;
   begin
      Mutex.Take;
      Items_Count := S.Index - 1;
      Mutex.Release;
      return Items_Count;
   end Current_Items;

end Stacks;

Re: Aspect programming

[AdaMagica]

You're using GNAT, which requires one compilation unit per file.
Thus your pragma Assertion_Policy applies only to the unit where it is
in the context clause.

If you want it to apply to all units, you have to use it as a
configuration pragma.

Re: Aspect programming

[Robert A Duff]

AdaMagica <christ-usch.grein@t-online.de> writes:

> You're using GNAT, which requires one compilation unit per file.

By default.  There are ways to get around that, but the easiest
thing is to follow GNAT's default convention.

> Thus your pragma Assertion_Policy applies only to the unit where it is
> in the context clause.
>
> If you want it to apply to all units, you have to use it as a
> configuration pragma.

Right, or use the -gnata switch.

- Bob

Re: Aspect programming

[Adam Beneschan]

On 7/27/2011 9:56 PM, AdaMagica wrote:
> You're using GNAT, which requires one compilation unit per file.
> Thus your pragma Assertion_Policy applies only to the unit where it is
> in the context clause.
>
> If you want it to apply to all units, you have to use it as a
> configuration pragma.

I don't think this is entirely accurate.  The RM says (10.1.5(8)) that 
configuration pragmas appear before the first compilation unit of a 
"compilation", and "The pragma applies to all compilation_units 
appearing in the compilation, unless there are none, in which case it 
applies to all future compilation_units compiled in the same environment."

It's not clear which one applies in the original poster's case.  If GNAT 
does disallow more than one compilation unit per file, then clearly the 
source in the original post must actually be multiple files (or else it 
wouldn't have worked), and we weren't really told where the dividing 
lines between the files are.  For all we know, the first 
Assertion_Policy pragma could have been in its own file.

But even if the first Assertion_Policy was in the same file as the
Aspect_Programming_Test procedure, it's still a configuration pragma. 
The difference here is that it's a configuration pragma that applies 
only to Aspect_Programming_Test and not to any of the other compilation 
units (it appears that there's another Assertion_Policy that applies to 
the body of Stacks).  But it's still a configuration pragma, so I think 
you really wanted to say something like "you have to use it as an 
environment-wide configuration pragma" or whatever the correct term is.

Even so, I still don't think this is the right answer.  Regarding 
preconditions, 6.1.1(20) says, "If the assertion policy in effect at the 
point of a subprogram or entry declaration is Check, then upon a call of 
the subprogram ... precondition checks are performed ...".  So where is 
the subprogram declaration?  Since Stacks is a generic, I think that the 
declarations of Int_Stacks.Push and Int_Stacks.Pop occur at the point 
the Stacks generic is instantiated, which where the instance Int_Stacks 
is declared, which is inside Aspect_Programming_Test; thus, even if the 
first Assertion_Policy is a configuration pragma that applies only to 
Aspect_Programming_Test, it still should apply here, and the 
precondition checks should be performed.  However, I haven't researched 
all the relevant language rules carefully, and there may be some rules 
that affect when assertion policies apply to declarations (or Assert 
pragmas) created by instantiation.

				-- Adam

Re: Aspect programming

[Adam Beneschan]

On 7/28/2011 11:13 AM, Adam Beneschan wrote:

>However, I haven't researched
> all the relevant language rules carefully, and there may be some rules
> that affect when assertion policies apply to declarations (or Assert
> pragmas) created by instantiation.

OK, I just ran across 11.4.2(17), which says "The assertion policy that 
applies to a generic unit also applies to all its instances".  11.4.2 
also talks about a default assertion policy that applies when there's no 
explicit Assertion_Policy that applies to a compilation unit; this 
policy is implementation-defined, and I don't know how GNAT defines it, 
and I don't feel like looking it up, but I assume that GNAT's default is 
that assertions aren't checked... is that right?

I assume that "an assertion policy applying to its instances" means that 
this policy supersedes anything that might be in effect elsewhere in the 
compilation unit; although the RM doesn't say this explicitly, it looks 
like this is the intent, and I haven't yet found any corner cases where 
the RM doesn't provide a clear answer about what's supposed to happen.

So I guess you can ignore the last paragraph of my previous post.

				-- Adam

Re: Aspect programming

[Martin]

On Jul 28, 5:56 am, AdaMagica <christ-usch.gr...@t-online.de> wrote:
> You're using GNAT, which requires one compilation unit per file.
> Thus your pragma Assertion_Policy applies only to the unit where it is
> in the context clause.
>
> If you want it to apply to all units, you have to use it as a
> configuration pragma.

Behaviour doesn't change even if you provide the configuration
pragma's in a file and specify the Global_Configuration_Pragmas in
the .gpr file...

-- Martin

Re: Aspect programming

[Anh Vo]

On Jul 28, 11:13 am, Adam Beneschan <a...@irvine.com> wrote:
> On 7/27/2011 9:56 PM, AdaMagica wrote:
>
> > You're using GNAT, which requires one compilation unit per file.
> > Thus your pragma Assertion_Policy applies only to the unit where it is
> > in the context clause.
>
> > If you want it to apply to all units, you have to use it as a
> > configuration pragma.
>
> It's not clear which one applies in the original poster's case.  If GNAT
> does disallow more than one compilation unit per file, then clearly the
> source in the original post must actually be multiple files (or else it
> wouldn't have worked), and we weren't really told where the dividing
> lines between the files are.  For all we know, the first
> Assertion_Policy pragma could have been in its own file.

Actually, each program unit is in a separate file per GNAT convention.
While posting, I just copy and past their contents one after the
other.

When using switch -gnata, GNAT crashes with a bug box. Harry Tucker
already submitted a bug reported.

Anh Vo

Re: Aspect programming

[Adam Beneschan]

On 7/29/2011 9:09 AM, Anh Vo wrote:

>>> If you want it to apply to all units, you have to use it as a
>>> configuration pragma.
>>
>> It's not clear which one applies in the original poster's case.  If GNAT
>> does disallow more than one compilation unit per file, then clearly the
>> source in the original post must actually be multiple files (or else it
>> wouldn't have worked), and we weren't really told where the dividing
>> lines between the files are.  For all we know, the first
>> Assertion_Policy pragma could have been in its own file.
>
> Actually, each program unit is in a separate file per GNAT convention.
> While posting, I just copy and past their contents one after the
> other.

In that case, where was the Assertion_Policy pragma that you included at 
the top of your source?  In the same file as Aspect_Programming_Test, or 
in its own file?  If "file" == "compilation" on GNAT, then according to 
the language rules, if you included it in the same file (compilation) as 
the procedure, it would have applied only to the procedure.

However it's done, I believe that Assertion_Policy(Check) has to be 
applied to the specification of the Stacks generic package in order for 
you to get the checks to happen.  I don't know what works on GNAT or 
what doesn't.  But adding the pragma to the top of stacks.ads should 
work.  Compiling it as a configuration pragma that applies to "all 
future compilation_units compiled into the same environment" (10.1.5(8)) 
should work too, according to the language rules, but Martin's earlier 
comment seems to imply that it doesn't.

				-- Adam

Re: Aspect programming

[Harry Tucker]

But then when the compiler outputs the below when compiling his code I
think that something else is going on.

+===========================GNAT BUG
DETECTED==============================+
| GPL 2011 (20110428) (i686-pc-mingw32) GCC
error:                         |
| in gnat_to_gnu_entity, at ada/gcc-interface/decl.c:
329                   |
| Error detected at stacks.ads:28:23 [aspect_programming_test.adb:
26:4]    |
| Please submit a bug report by email to
report@adacore.com.               |
| GAP members can alternatively use GNAT
Tracker:                          |
| http://www.adacore.com/ section 'send a
report'.                         |
| See gnatinfo.txt for full info on procedure for submitting
bugs.         |
| Use a subject line meaningful to you and us to track the
bug.            |
| Include the entire contents of this bug box in the
report.               |
| Include the exact gcc or gnatmake command that you
entered.              |
| Also include sources listed below in gnatchop
format                     |
| (concatenated together with no headers between
files).                   |
| Use plain ASCII or MIME
attachment.                                      |
+==========================================================================
+

And from the GNAT RM, Sec 13:

"AI-0183 Aspect specifications (2010-08-16)
Aspect specifications have been fully implemented except for pre and
post- conditions, and type invariants, which have their own separate
AI's. All forms of declarations listed in the AI are supported..."

So I would expect some issues to arise.

In my own play with aspects I haven't seen this bug-box.

Harry

Re: Aspect programming

[Anh Vo]

On Jul 27, 9:56 pm, AdaMagica <christ-usch.gr...@t-online.de> wrote:
> You're using GNAT, which requires one compilation unit per file.
> Thus your pragma Assertion_Policy applies only to the unit where it is
> in the context clause.
>
> If you want it to apply to all units, you have to use it as a
> configuration pragma.

Actually, each program unit is contained in a separate file per GNAT
file / unit convention. Interestingly enough GNAT crashes with a bug
box when -gnata switch is used. In fact, Harry Tucker submitted a bug
report already. In addition, based on Adam's comments, I am convinced
that this is a compiler's bug. By the way, thank you for all replies.

Anh Vo

Re: Aspect programming

[Yannick Duchêne (Hibou57)]

Unfortunately, the thread's content did not match so much the thread's  
title (cheese).

If anyone know any good on-line materials about aspect-programming in Ada  
and the best ways to get equivalent of the LISP's “:before”, “:after” and  
“:around” inserted methods (with or without the help of auxiliary tools),  
I would welcome any material (just for personal study matters).

With thanks

-- 
“Syntactic sugar causes cancer of the semi-colons.”  [Epigrams on  
Programming — Alan J. — P. Yale University]
“Structured Programming supports the law of the excluded muddle.” [Idem]
Java: Write once, Never revisit