* Presentations on-line - Ada&SPARK for Education&Research
@ 2010-03-02 21:22 Dirk Craeynest
2010-03-05 8:03 ` Georg Bauhaus
2010-03-06 12:40 ` Marco
0 siblings, 2 replies; 9+ messages in thread
From: Dirk Craeynest @ 2010-03-02 21:22 UTC (permalink / raw)
Cc: dirk
[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: Type: text/plain, Size: 2729 bytes --]
-----------------------------------------------------------------------
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
-----------------------------------------------------------------------
All presentations at this half-day Seminar, held at the university in
Leuven last week, are available now on the web sites of Ada-Belgium
and the Distrinet research group: see URLs above.
For each presentation a PDF version can be downloaded; some are also
available in other formats (ODP or PPTX):
- "What's New in the World of Ada"
Robert Dewar, AdaCore, New York, USA
- "Ada in Industry, an Experience Report"
Philippe Waroquiers, EUROCONTROL/CFMU, Brussels, Belgium
- "Ada in Research and Education, an Experience Report"
Erhard Pl�dereder, University Stuttgart, Germany
- "SPARK - The Libre Language and Toolset for High-Assurance Software"
Rod Chapman, Altran Praxis, Bath, UK
The seminar went very well, with a good mix of people from academia,
research and industry, not only from Belgium, but also from the U.K.,
the Netherlands, Germany and France. Many participants told us they
really appreciated the event; some of the feedback we received:
"... was really interesting being there."
"... a most interesting Ada meeting at the K.U.Leuven."
"I did find all the presentations very interesting as well as
the informal discussions with the people present."
Thanks again to all presenters for their collaboration, to AdaCore
for the many Ada books we handed out, to the participants for their
interest, as well as for all the efforts many speakers and participants
went through to come to Leuven at a time when both European high speed
rail and air travel was disrupted.
Enjoy the on-line presentations!
Dirk Craeynest, Ada-Belgium, Dirk.Craeynest@cs.kuleuven.be
-----------------------------------------------------------------------
(V20100302.1)
^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: Presentations on-line - Ada&SPARK for Education&Research
2010-03-02 21:22 Presentations on-line - Ada&SPARK for Education&Research Dirk Craeynest
@ 2010-03-05 8:03 ` Georg Bauhaus
2010-03-05 9:14 ` J-P. Rosen
` (2 more replies)
2010-03-06 12:40 ` Marco
1 sibling, 3 replies; 9+ messages in thread
From: Georg Bauhaus @ 2010-03-05 8:03 UTC (permalink / raw)
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;
^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: Presentations on-line - Ada&SPARK for Education&Research
2010-03-05 8:03 ` Georg Bauhaus
@ 2010-03-05 9:14 ` J-P. Rosen
2010-03-05 10:46 ` Georg Bauhaus
2010-03-06 8:43 ` Jerry van Dijk
2010-03-05 9:19 ` Dmitry A. Kazakov
2010-03-05 12:11 ` Peter Hermann
2 siblings, 2 replies; 9+ messages in thread
From: J-P. Rosen @ 2010-03-05 9:14 UTC (permalink / raw)
Georg Bauhaus a écrit :
> True? With some effort, it seems possible to break an Ada
> monitor implemented as a protected object.
>
With enough pointers, you can make anything unreliable ;-), but the
important point in your remark is "with some effort". If you make a
special effort to publicly export something that is meant to be
protected, it ceases to be protected. But this can happen only if the
author of the PO provides facility for doing that; it cannot happen due
to misuse on the client side.
--
---------------------------------------------------------
J-P. Rosen (rosen@adalog.fr)
Visit Adalog's web site at http://www.adalog.fr
^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: Presentations on-line - Ada&SPARK for Education&Research
2010-03-05 8:03 ` Georg Bauhaus
2010-03-05 9:14 ` J-P. Rosen
@ 2010-03-05 9:19 ` Dmitry A. Kazakov
2010-03-05 12:11 ` Peter Hermann
2 siblings, 0 replies; 9+ messages in thread
From: Dmitry A. Kazakov @ 2010-03-05 9:19 UTC (permalink / raw)
On Fri, 05 Mar 2010 09:03:08 +0100, Georg Bauhaus wrote:
> 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;
monitor.adb:13:25: warning: possible unprotected access to protected data
Which pins down broken design.
> end expose;
> end SynchNode;
>
> end Monitor;
With even less efforts you can break anything:
X : SynchNode;
Y : Float;
for Y'Address use X'Address;
begin
Y := sqrt (Y);
----------------------------------
1. Do not use pointers
2. Do not use global variables
--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de
^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: Presentations on-line - Ada&SPARK for Education&Research
2010-03-05 9:14 ` J-P. Rosen
@ 2010-03-05 10:46 ` Georg Bauhaus
2010-03-06 8:43 ` Jerry van Dijk
1 sibling, 0 replies; 9+ messages in thread
From: Georg Bauhaus @ 2010-03-05 10:46 UTC (permalink / raw)
J-P. Rosen schrieb:
> Georg Bauhaus a écrit :
>> True? With some effort, it seems possible to break an Ada
>> monitor implemented as a protected object.
>>
> With enough pointers, you can make anything unreliable ;-), but the
> important point in your remark is "with some effort". If you make a
> special effort to publicly export something that is meant to be
> protected, it ceases to be protected. But this can happen only if the
> author of the PO provides facility for doing that; it cannot happen due
> to misuse on the client side.
Thanks, this is wording I had been looking for.
^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: Presentations on-line - Ada&SPARK for Education&Research
2010-03-05 8:03 ` Georg Bauhaus
2010-03-05 9:14 ` J-P. Rosen
2010-03-05 9:19 ` Dmitry A. Kazakov
@ 2010-03-05 12:11 ` Peter Hermann
2 siblings, 0 replies; 9+ messages in thread
From: Peter Hermann @ 2010-03-05 12:11 UTC (permalink / raw)
Georg Bauhaus <rm-host.bauhaus@maps.futureapps.de> wrote:
> 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;
monitor.adb:69:24: warning: possible unprotected access to protected data
> end expose;
> end SynchNode;
>
> end Monitor;
^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: Presentations on-line - Ada&SPARK for Education&Research
2010-03-05 9:14 ` J-P. Rosen
2010-03-05 10:46 ` Georg Bauhaus
@ 2010-03-06 8:43 ` Jerry van Dijk
2010-03-08 5:54 ` AdaMagica
1 sibling, 1 reply; 9+ messages in thread
From: Jerry van Dijk @ 2010-03-06 8:43 UTC (permalink / raw)
"J-P. Rosen" <rosen@adalog.fr> writes:
> With enough pointers, you can make anything unreliable ;-)
That just went into my signature file :-)
--
-- Jerry van Dijk
-- Leiden, Holland
--
-- The early bird may get the worm, but the second mouse gets the cheese!!
^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: Presentations on-line - Ada&SPARK for Education&Research
2010-03-02 21:22 Presentations on-line - Ada&SPARK for Education&Research Dirk Craeynest
2010-03-05 8:03 ` Georg Bauhaus
@ 2010-03-06 12:40 ` Marco
1 sibling, 0 replies; 9+ messages in thread
From: Marco @ 2010-03-06 12:40 UTC (permalink / raw)
thank you
^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: Presentations on-line - Ada&SPARK for Education&Research
2010-03-06 8:43 ` Jerry van Dijk
@ 2010-03-08 5:54 ` AdaMagica
0 siblings, 0 replies; 9+ messages in thread
From: AdaMagica @ 2010-03-08 5:54 UTC (permalink / raw)
On 6 Mrz., 09:43, Jerry van Dijk <je...@jerryware.nl> wrote:
> "J-P. Rosen" <ro...@adalog.fr> writes:
> > With enough pointers, you can make anything unreliable ;-)
>
> That just went into my signature file :-)
>
> --
> -- Jerry van Dijk
> -- Leiden, Holland
> --
> -- The early bird may get the worm, but the second mouse gets the cheese!!
So why don't worms get it - early is shit?
^ permalink raw reply [flat|nested] 9+ messages in thread
end of thread, other threads:[~2010-03-08 5:54 UTC | newest]
Thread overview: 9+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2010-03-02 21:22 Presentations on-line - Ada&SPARK for Education&Research Dirk Craeynest
2010-03-05 8:03 ` Georg Bauhaus
2010-03-05 9:14 ` J-P. Rosen
2010-03-05 10:46 ` Georg Bauhaus
2010-03-06 8:43 ` Jerry van Dijk
2010-03-08 5:54 ` AdaMagica
2010-03-05 9:19 ` Dmitry A. Kazakov
2010-03-05 12:11 ` Peter Hermann
2010-03-06 12:40 ` Marco
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox