Type definition mapping for generating SPARK 83 (Ada code)
For each Type Definition, ACS generates a type, array type, enumeration type or subtype:
• If the Type Definition has Array Construction, ACS generates an array type declaration.
• If the Type Definition has Enumeration Construction, ACS generates an enumeration type declaration.
• If the Type Definition has Sequence Construction and is stereotyped by the «Ada Subtype» stereotype, ACS generates a subtype declaration.
The generation of a Type Definition is derived from the properties of the Type Definition and the Stereotypes and Tag Definitions that are applied to it:
• If the Type Definition's Lower Bound and Upper Bound properties are set (Type Definition of Array construction only) and the «Ada Array» stereotype has not been applied, the values are used to derive the range of the array index.
• If the Type Definition's Visibility property set to Public or Package, ACS generates a type within the package specification.
• If the Type Definition's Visibility property is set to Public or Package, and the Type Definition is stereotyped by the «Ada Private» stereotype, ACS generates a type with the 'private' keyword within the private part of the package specification. If the tagged value of the Ada Limited tag definition (applied by the «Ada Private» stereotype) is set to TRUE, ACS generates the type with the 'limited private' keywords.
• If the Type Definition's Visibility property is set to Private, ACS generates a type within the package body.
• If the Type Definition's Visibility property set to Protected, ACS generates a type within the private area of the package specification.
• If the Type Definition is stereotyped by the «Ada Anonymous» stereotype, ACS generates an anonymous type.
• If the Type Definition is stereotyped by the «Ada Array» stereotype, the Lower Bound and Upper Bound properties are ignored. ACS generates the range of the array index from the Ada Array Index or Ada Array Index Type tag definition (both applied by the «Ada Array» stereotype):
◦ If a tagged value is set for the Ada Array Index tag definition, the value is generated as the array index text.
◦ If a tagged value is set for the Ada Array Index tag definition is blank and the tagged value of the Ada Array Index Type tag definition references a Type Definition, the referenced Type Definition is used is generated as the type of the index. This applies only to single dimension arrays with simple range types.
◦ The tagged value of the Ada Unconstrained Range tag definition is ignored.
If the «Ada Array» stereotype is applied to an array Type Definition, ACS ignores the Lower Bound and Upper Bound properties of that Type Definition.
• If the Type Definition is stereotyped by the «Ada Constraint» stereotype, the applied Tag Definitions can apply range, mod, delta and digits constraints:
◦ If a tagged value has been set for the Ada Delta tag definition, ACS generates a delta constraint. The tagged value of the Ada Delta tag definition is used to generate the value of the delta constraint.
◦ If a tagged value has been set for the Ada Digits tag definition, ACS generates a digits constraint. The tagged value of the Ada Digits tag definition is used to generate the value of the digits constraint.
◦ If a tagged value has been set for the Ada Mod tag definition, ACS generates a mod constraint. The tagged value of the Ada Mod tag definition is used to generate the value of the mod constraint.
◦ If a tagged value has been set for the Ada Range tag definition, ACS generates a range constraint. The tagged value of the Ada Range tag definition is used to generate the range expression text.
• If the Type Definition is stereotyped by the «Ada Pragma» stereotype, the tagged value of the Ada Pragma Text tag definition (applied by the «Ada Pragma» stereotype) is used to generate the pragmas.
• If the Type Definition is stereotyped by the «Ada Representation» stereotype, the generated type declaration includes a representation clause. The tagged value of the Ada Representation Text tag definition is used to generate the representation clauses.
• If the Type Definition is stereotyped by the «Ada Type Binding» stereotype, the tagged value of the Ada Type Parameters tag definition (applied by the «Ada Type Binding» stereotype) is used to generate the parameters of the type.
• Aliases are not generated.
• The Pointer property is ignored.
• The «Ada Access» stereotype does not apply to the SPARK 83 Code Generator DLL.
• The «Ada Attribute Designator» stereotype is ignored.
