Team-Ada folks,

Several recent messages have given the impression that the HRG Guide
imposes restrictions and/or defines a subset:

from Bill Pritchett:
"The tool, called AdaSTAT, also enforces the language restrictions
recommended by the Annex H Rapporteur Group."

from Currie Colket:
"AdaSTAT is built upon ASIS and 1) flags violations of safety-critical
language
restrictions,..."

from SY Wong (referring to the AdaSTAT tool):
"I want to ask them
the question why they think SIGAda members will be interested in safety
restrictions when I have to battle the group for many years to define
a subset without the restricted constructs."

In fact the Guide does neither of these.

The basis of the HRG Guide is that any development of high-integrity
software will make systematic use of several verification techniques
("systematic" should be understood as meaning that the techniques are to
be applied to all the delivered software). The Guide identifies 15 such
techniques (10 analysis and 5 testing).

However some language features are not compatible with some verification
techniques - the Guide identifies these incompatibilities.

So, the user of the Guide first defines their software process then
determines the restrictions that are necessary to ensure that process is
not defeated by inappropriate code.

There are therefore as many sets of restrictions, or subsets, as there
are combinations of the verification techniques. For a tool to "[enforce]
the language restrictions recommended" by the Guide it must allow the
user to define the set of verification techniques to be applied.

I would be grateful if someone attending the DCS demonstration could post
a summary of what the tool actually does.

Phil Thornley