An: www.ada-ru.org

An: www.ada-ru.org

[Dmitriy Anisimkov]

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: Type: text/plain, Size: 492 bytes --]

http://www.ada-ru.org

Welcome to new site about Ada in russian.

There is no content in english for now, be�ause our main goal is to
represent Ada for the russian programmers.
There are enought Ada sites in english in the world and
http://www.ada-ru.org
has links over there.

We invite russian speaking people to intent our site.
We appreciate any comments and new russian stuff to populate this site.

Note,
this site is powered by the Ada Web Server. http://libre.act-europe.fr/aws

Re: An: www.ada-ru.org

[Larry Kilgallen]

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: Type: text/plain, Size: 781 bytes --]

In article <b13mii$bmg$1@ns.omskelecom.ru>, "Dmitriy Anisimkov" <anisimkov@yahoo.com> writes:
> http://www.ada-ru.org
> 
> Welcome to new site about Ada in russian.

Congratulations !

> There is no content in english for now, be�ause our main goal is to
> represent Ada for the russian programmers.
> There are enought Ada sites in english in the world and
> http://www.ada-ru.org
> has links over there.

That sounds reasonable.  It would be a good idea if you sent your
announcement to the people who run each of:

	http://www.adaic.org
	http://www.adapower.com

so they will put a link to your site on their sites.  I can imagine
someone who would prefer their information in Russian might first find
one of those English language sites, and be grateful for the reference.

Re: An: www.ada-ru.org

[Dmitriy Anisimkov]

> That sounds reasonable.  It would be a good idea if you sent your
> announcement to the people who run each of:
>
> http://www.adaic.org
> http://www.adapower.com

Good idea. I sent a request to the webmasters of the sites.

Re: www.ada-ru.org

[Rodrigo Garcia]

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: Type: text/plain, Size: 1013 bytes --]

"Dmitriy Anisimkov" <anisimkov@yahoo.com> wrote in message
news:b13mii$bmg$1@ns.omskelecom.ru...
> http://www.ada-ru.org
>
> Welcome to new site about Ada in russian.
>
> There is no content in english for now, be�ause our main goal is to
> represent Ada for the russian programmers.
> There are enought Ada sites in english in the world and
> http://www.ada-ru.org
> has links over there.
>
> We invite russian speaking people to intent our site.
> We appreciate any comments and new russian stuff to populate this site.
>
> Note,
> this site is powered by the Ada Web Server. http://libre.act-europe.fr/aws
>


Great!

    I have seen that, among the links you have added, you have included the
ORK page. As one of the project developers of ORK, I am very proud of it.
However, in the the text of the link, you can read SPARK (the High-Integrity
version of Ada) instead of SPARC (the processor achitecture) as one of the
possible targets. Please, correct it as it can lead to misunderstandings.

Rodrigo

SPARK or RAVENSCAR (from "Re: www.ada-ru.org")

[Colin Paul Gloster]

In article news:3e3ab8ff$1@epflnews.epfl.ch , Rodrigo Garcia wrote
in response to a post by Dmitriy Anisimkov:
  
"    I have seen that, among the links you have added, you have included the
ORK page. As one of the project developers of ORK, I am very proud of it.
[..] you can read SPARK (the High-Integrity version of Ada) [..]"

Hello Rodrigo.

SPARK typically involves more dedication to proofs but Ravenscar is not
intended to be low integrity I would think. Do you think that SPARK is
typically safer (for space work)?

Re: SPARK or RAVENSCAR (from "Re: www.ada-ru.org")

[Vinzent Hoefler]

Colin Paul Gloster wrote:

> SPARK typically involves more dedication to proofs but Ravenscar is
> not intended to be low integrity I would think. Do you think that
> SPARK is typically safer (for space work)?

Well, probably you cannot really compare these two.

Ravenscar ist just a profile on what Ada features to use and what not to 
use. In this sense the concept (subset of existing language) might be 
seen similar to SPARK. But SPARK is a Ada-subset language with 
additional annotations for automatic proof and in some terms it is far 
more restricted than plain Ravenscar.

So, from what I know, I'd say most if not all SPARK programs would 
conform to Ravenscar, but a Ravenscar conforming program is not 
necessarily written in SPARK.

So, in this view SPARK programs look safer, yes. ;)


Vinzent.

-- 
I think every good Christian ought to kick Falwell right in the ass.
                -- Barry Goldwater

Re: SPARK or RAVENSCAR (from "Re: www.ada-ru.org")

[Phil Thornley]

"Colin Paul Gloster" <Colin_Paul_Gloster@ACM.org> wrote in message
news:slrnb3vm4q.eb3.Colin_Paul_Gloster@camac.dcu.ie...
> In article news:3e3ab8ff$1@epflnews.epfl.ch , Rodrigo Garcia wrote
> in response to a post by Dmitriy Anisimkov:
>
> "    I have seen that, among the links you have added, you have
included the
> ORK page. As one of the project developers of ORK, I am very proud of
it.
> [..] you can read SPARK (the High-Integrity version of Ada) [..]"
>
> Hello Rodrigo.
>
> SPARK typically involves more dedication to proofs but Ravenscar is
not
> intended to be low integrity I would think. Do you think that SPARK is
> typically safer (for space work)?

SPARK and Ravenscar can't be compared because they address different
aspects of the language.

- The Ravenscar profile is explicitly silent on the sequential part of
the language.
- The SPARK language is (currently) limited to sequential programs.

So there is an excellent case for using them both - restrict the tasking
features used to conform to Ravenscar and analyse each task as a
separate SPARK program.

In fact this is such a good idea that the SPARK developers are planning
to add Ravenscar compliant features to the next version of SPARK. :-)


The guide to Ravenscar has recently been completed by the HRG. It is
published initially as a University of York report:

ftp://ftp.cs.york.ac.uk/reports and click on YCS-2003-348.pdf

and will be offered to WG9 as a potential ISO technical report.

Cheers,

Phil

--
Phil Thornley
BAE SYSTEMS

Re: SPARK or RAVENSCAR (from "Re: www.ada-ru.org")

[Rod Chapman]

Vinzent Hoefler <ada.rocks@jlfencey.com> wrote in message news:
> So, from what I know, I'd say most if not all SPARK programs would 
> conform to Ravenscar, but a Ravenscar conforming program is not 
> necessarily written in SPARK.

I'm pleased to say that the next release of the SPARK language and
toolkit will incorporate the Ravenscar Profile as a core part of
the SPARK language.  Simply put, SPARK will be a strict subset of the
Ravenscar Profile incorporating library level tasks, protected objects,
suspension objects, Ada.Real_Time and so on.

The language will, of course, be amenable to all the existing forms
of static analysis implemented by the Examiner, but will add:

1) Analysis to show that programs are free from Ravenscar-defined
erroneous behaviour, exceptions, bounded errors and so on.  For example,
SPARK will be statically free from priority ceiling violations,
entry queue length violations, and so on.

2) Information flow analysis at the partition-level.

3) and much more...

We will be presenting a tutorial on the combined "RavenSPARK" language
and its analysis at Ada Europe in Toulouse in June.

 - Rod Chapman, SPARK Team, Praxis Critical Systems