Re: Presentations on-line - Ada&SPARK for Education&Research

[Georg Bauhaus <rm-host.bauhaus@maps.futureapps.de>]

On 3/2/10 10:22 PM, Dirk Craeynest wrote:
> -----------------------------------------------------------------------
>
>                    All presentations available on-line
>
>                    T e c h n o l o g y   U p d a t e :
>                         A d a   a n d   S P A R K
>            f o r   e d u c a t i o n   a n d   r e s e a r c h
>
>         State-of-the-art programming language technology with Ada
>              Formal specifications made practical with SPARK
>
>                            Seminar organized by
>             the Computer Science Department of the K.U.Leuven
>                      and the Ada-Belgium organization
>                with support from AdaCore and Altran Praxis
>
>                  Tuesday, February 23, 2010, 14:00-18:00
>                 K.U.Leuven, Department of Computer Science
>          Celestijnenlaan 200A, B-3001 Leuven (Heverlee), Belgium
>
> http://www.cs.kuleuven.be/~dirk/ada-belgium/events/10/100223-ab-adaspark.html
>       http://distrinet.cs.kuleuven.be/events/AdaEvent/abstracts.html

> - "Ada in Research and Education, an Experience Report"
>    Erhard Pl�dereder, University Stuttgart, Germany


I'm reading a few presentation pages that advertise  the strengths
of Ada. One sheet compares monitor functionalities as present
in Java and Ada.  Java needs much care not to break
a monitor.  Ada is shown not to have this problem.

True?  With some effort, it seems possible to break an Ada
monitor implemented as a protected object.

package Monitor is

    type SynchNode;
    type Linkage is access all synchnode;
    type data is access all integer;

    protected type synchnode is
       procedure Link (x : Linkage);
       procedure Expose (N : out Data);
    private
       Outgoing : aliased Integer := 0;
    end SynchNode;

end Monitor;

package body monitor is

    protected body synchnode is
       procedure link (X : Linkage) is
          View : Data; -- X's data
       begin
          X.Expose(View);
          View.all := View.all + 1;  -- <-- unprotected
       end link;

       procedure Expose (N : out Data) is
       begin
          N := Outgoing'unchecked_access;
       end expose;
    end SynchNode;

end Monitor;