Spark and the Ada numerics annex

[Ada novice <ycalleecharan@gmx.com>]

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