From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00,FREEMAIL_FROM
	autolearn=ham autolearn_force=no version=3.4.4
X-Google-Thread: 103376,35bd0e7237228bcd,start
X-Google-NewGroupId: yes
X-Google-Attributes: gida07f3367d7,domainid0,public,usenet
X-Google-Language: ENGLISH,ASCII-7-bit
Path: 
 g2news1.google.com!postnews.google.com!t20g2000yqa.googlegroups.com!not-for-mail
From: Ada novice <ycalleecharan@gmx.com>
Newsgroups: comp.lang.ada
Subject: Spark and the Ada numerics annex
Date: Tue, 10 Aug 2010 01:48:30 -0700 (PDT)
Organization: http://groups.google.com
Message-ID: 
 <064d3276-769c-46f7-9590-77a90af589cb@t20g2000yqa.googlegroups.com>
NNTP-Posting-Host: 193.11.22.91
Mime-Version: 1.0
Content-Type: text/plain; charset=ISO-8859-1
X-Trace: posting.google.com 1281430110 1554 127.0.0.1 (10 Aug 2010 08:48:30
 GMT)
X-Complaints-To: groups-abuse@google.com
NNTP-Posting-Date: Tue, 10 Aug 2010 08:48:30 +0000 (UTC)
Complaints-To: groups-abuse@google.com
Injection-Info: t20g2000yqa.googlegroups.com; posting-host=193.11.22.91;
	posting-account=Rr9I-QoAAACS-nOzpA-mGxtAlZ46Nb6I
User-Agent: G2/1.0
X-HTTP-UserAgent: Mozilla/5.0 (Windows; U; Windows NT 5.1; en-US; rv:1.9.2.8)
	Gecko/20100722 Firefox/3.6.8 (.NET CLR 3.5.30729),gzip(gfe)
Xref: g2news1.google.com comp.lang.ada:13040
Date: 2010-08-10T01:48:30-07:00
List-Id: <comp.lang.ada>

Hi, I became interested in taking a look at SPARK. I've browsed
through the freely available first chapter of Barnes's SPARK book and
I saw that SPARK doesn't seem to cover the Ada specialized annexes
(see Figure 1.1. Relatonship between SPARK and Ada on pp. 11).

My interests are purely in Scientific numerical programming with Ada
and the Ada numerics annex is important to me. Is it true that SPARK.
If I understand correctly, then simple mathematical functions like
SQRT are elementary functions that are part of the language Ada itself
and SPARK will recognize these elementary functions. But the extensive
vector and matrix manipulations as added in Ada 05 won't be recognized
by SPARK. Am I right?

The good things about SPARK is that it helps to make checks and hence
get the programming right. Is it recommended to use SPARK even for
very simple programs?

Thanks
YC