* An: www.ada-ru.org @ 2003-01-27 16:27 Dmitriy Anisimkov 2003-01-27 20:00 ` Larry Kilgallen 2003-01-31 17:57 ` www.ada-ru.org Rodrigo Garcia 0 siblings, 2 replies; 8+ messages in thread From: Dmitriy Anisimkov @ 2003-01-27 16:27 UTC (permalink / raw) [-- 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 ^ permalink raw reply [flat|nested] 8+ messages in thread
* Re: An: www.ada-ru.org 2003-01-27 16:27 An: www.ada-ru.org Dmitriy Anisimkov @ 2003-01-27 20:00 ` Larry Kilgallen 2003-01-28 9:07 ` Dmitriy Anisimkov 2003-01-31 17:57 ` www.ada-ru.org Rodrigo Garcia 1 sibling, 1 reply; 8+ messages in thread From: Larry Kilgallen @ 2003-01-27 20:00 UTC (permalink / raw) [-- 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. ^ permalink raw reply [flat|nested] 8+ messages in thread
* Re: An: www.ada-ru.org 2003-01-27 20:00 ` Larry Kilgallen @ 2003-01-28 9:07 ` Dmitriy Anisimkov 0 siblings, 0 replies; 8+ messages in thread From: Dmitriy Anisimkov @ 2003-01-28 9:07 UTC (permalink / raw) > 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. ^ permalink raw reply [flat|nested] 8+ messages in thread
* Re: www.ada-ru.org 2003-01-27 16:27 An: www.ada-ru.org Dmitriy Anisimkov 2003-01-27 20:00 ` Larry Kilgallen @ 2003-01-31 17:57 ` Rodrigo Garcia 2003-02-04 15:13 ` SPARK or RAVENSCAR (from "Re: www.ada-ru.org") Colin Paul Gloster 1 sibling, 1 reply; 8+ messages in thread From: Rodrigo Garcia @ 2003-01-31 17:57 UTC (permalink / raw) [-- 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 ^ permalink raw reply [flat|nested] 8+ messages in thread
* SPARK or RAVENSCAR (from "Re: www.ada-ru.org") 2003-01-31 17:57 ` www.ada-ru.org Rodrigo Garcia @ 2003-02-04 15:13 ` Colin Paul Gloster 2003-02-04 15:57 ` Vinzent Hoefler 2003-02-05 8:37 ` Phil Thornley 0 siblings, 2 replies; 8+ messages in thread From: Colin Paul Gloster @ 2003-02-04 15:13 UTC (permalink / raw) 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)? ^ permalink raw reply [flat|nested] 8+ messages in thread
* Re: SPARK or RAVENSCAR (from "Re: www.ada-ru.org") 2003-02-04 15:13 ` SPARK or RAVENSCAR (from "Re: www.ada-ru.org") Colin Paul Gloster @ 2003-02-04 15:57 ` Vinzent Hoefler 2003-02-05 12:01 ` Rod Chapman 2003-02-05 8:37 ` Phil Thornley 1 sibling, 1 reply; 8+ messages in thread From: Vinzent Hoefler @ 2003-02-04 15:57 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 8+ messages in thread
* Re: SPARK or RAVENSCAR (from "Re: www.ada-ru.org") 2003-02-04 15:57 ` Vinzent Hoefler @ 2003-02-05 12:01 ` Rod Chapman 0 siblings, 0 replies; 8+ messages in thread From: Rod Chapman @ 2003-02-05 12:01 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 8+ messages in thread
* Re: SPARK or RAVENSCAR (from "Re: www.ada-ru.org") 2003-02-04 15:13 ` SPARK or RAVENSCAR (from "Re: www.ada-ru.org") Colin Paul Gloster 2003-02-04 15:57 ` Vinzent Hoefler @ 2003-02-05 8:37 ` Phil Thornley 1 sibling, 0 replies; 8+ messages in thread From: Phil Thornley @ 2003-02-05 8:37 UTC (permalink / raw) "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 ^ permalink raw reply [flat|nested] 8+ messages in thread
end of thread, other threads:[~2003-02-05 12:01 UTC | newest] Thread overview: 8+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2003-01-27 16:27 An: www.ada-ru.org Dmitriy Anisimkov 2003-01-27 20:00 ` Larry Kilgallen 2003-01-28 9:07 ` Dmitriy Anisimkov 2003-01-31 17:57 ` www.ada-ru.org Rodrigo Garcia 2003-02-04 15:13 ` SPARK or RAVENSCAR (from "Re: www.ada-ru.org") Colin Paul Gloster 2003-02-04 15:57 ` Vinzent Hoefler 2003-02-05 12:01 ` Rod Chapman 2003-02-05 8:37 ` Phil Thornley
This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox