4. Names and Expressions

The term assertion expression denotes an expression that appears inside an assertion, which can be a pragma Assert, a precondition or postcondition, a type invariant or (subtype) predicate, or other assertions introduced in SPARK 2014.

4.1. Names

Legality Rules

  1. Neither explicit_dereference nor implicit_dereference are in SPARK 2014.

4.1.1. Indexed Components

No extensions or restrictions.

4.1.2. Slices

No extensions or restrictions.

4.1.3. Selected Components

Some constructs which would unconditionally raise an exception at run time in Ada are rejected as illegal in SPARK 2014 if this property can be determined prior to formal program verification.

Legality Rules

  1. If the prefix of a record component selection is known statically to be constrained so that the selected component is not present, then the component selection (which, in Ada, would raise Constraint_Error if it were to be evaluated) is illegal.

4.1.4. Attributes

Many of the Ada language defined attributes are in SPARK 2014 but there are exclusions. For a full list of attributes supported by SPARK 2014 see Language-Defined Attributes.

A SPARK 2014 implementation is permitted to support other attributes which are not Ada or SPARK 2014 language defined attributes and these should be documented in the User Guide for the tool.

Legality Rules

  1. The prefix of a ‘Access attribute_reference shall be a constant without variable input. [This ensures that information flows through such access values only depend on assignments to the access objects, not assignments to the accessed objects. See Object Declarations.]

4.1.5. User-Defined References

Legality Rules

  1. User-defined references are not allowed.
  1. The aspect Implicit_Dereference is not permitted.

4.1.6. User-Defined Indexing

Legality Rules

  1. User-defined indexing is not allowed.
  1. The aspects Constant_Indexing and Variable_Indexing are not permitted.

4.2. Literals

Legality Rules

  1. The literal null representing an access value is not allowed.

4.3. Aggregates

Legality Rules

  1. The box symbol, <>, shall not be used in an aggregate unless the type(s) of the corresponding component(s) define full default initialization.
  1. If the ancestor_part of an extension_aggregate is a subtype_mark, then the type of the denoted subtype shall define full default initialization.

[The box symbol cannot be used in an aggregate to produce an uninitialized scalar value or a composite value having an uninitialized scalar value as a subcomponent. Similarly for an ancestor subtype in an extension aggregate.]

4.4. Expressions

An expression is said to be side-effect free if the evaluation of the expression does not update any object. The evaluation of an expression free from side-effects only retrieves or computes a value.

Legality Rules

  1. An expression shall be side-effect free. [Strictly speaking, this “rule” is a consequence of other rules, most notably the rule that a function cannot have outputs other than its result.]
  1. An expression (or range) in SPARK 2014 occurring in certain contexts (listed below) shall not have a variable input. This means that such an expression shall not read a variable, nor shall it call a function which (directly or indirectly) reads a variable. These contexts include:

    • a constraint other than the range of a loop parameter specification (see Subtype Declarations);

    • the default_expression of a component declaration (see Record Types);

    • the default_expression of a discriminant_specification (see Discriminants);

    • a Dynamic_Predicate aspect specification (see Subtype Predicates);

    • a Type_Invariant aspect specification (see Type Invariants);

    • an indexing expression of an indexed_component or the discrete_range of a slice in an object renaming declaration which renames part of that index or slice (see Object Renaming Declarations);

    • a generic actual parameter corresponding to a generic formal object having mode in (see Generic Instantiation);

    • the declaration and body of a user-defined equality operation on a record type (see Overloading of Operators).

      [This avoids the case where such a record type is a component of another composite type, whose predefined equality operation now depends on variables through the primitive equality operation on its component.]

[An expression in one of these contexts may read a constant which is initialized with the value of a variable.]

[These rules simplify analysis by eliminating the need to deal with implicitly created anonymous constants. An expression which does not have a variable input will always yield the same result if it is (conceptually, for purposes of static analysis) reevaluated later. This is not true of an expression that has a variable input because the value of the variable might have changed.]

[For purposes of these rules, the current instance of a type or subtype is not considered to be a variable input in the case of a Dynamic_Predicate or Type_Invariant condition, but is considered to be a variable input in the case of the default_expression of a component declaration.]

4.4.1. Update Expressions

The Update attribute provides a way of overwriting specified components of a copy of a given composite value.

For a prefix X that denotes an object of a nonlimited record type or record extension T, the attribute

X'Update ( record_component_association_list )

is defined and yields a value of type T and is a record update expression.

For a prefix X that denotes an object of a nonlimited one dimensional array type T, the attribute

X'Update ( array_component_association {, array_component_association} )

is defined and yields a value of type T and is an array update expression.

For a prefix X that denotes an object of a nonlimited multidimensional array type T, the attribute

X'Update ( multidimensional_array_component_association
        {, multidimensional_array_component_association} )

is defined and yields a value of type T and is a multi-dimensional array update. Where multidimensional_array_component_association has the following syntax:

Syntax

multidimensional_array_component_association ::=
  index_expression_list_list => expression
index_expression_list_list ::=
  index_expression_list { | index_expression_list }
index_expression_list ::=
  ( expression {, expression} )

Legality Rules

  1. The box symbol, <>, may not appear in any expression appearing in an update expression.

Dynamic Semantics

  1. In all cases (i.e., whether T is a record type, a record extension type, or an array type - see below), evaluation of X'Update begins with the creation of an anonymous object of type T which is initialized to the value of X in the same way as for an occurrence of X'Old (except that the object is constrained by its initial value but not constant).
  1. Next, components of this object are updated as described in the following subsections. The attribute reference then denotes a constant view of this updated object. The master and accessibility level of this object are defined as for the anonymous object of an aggregate.
  1. The assignments to components of the result object described in the following subsections are assignment operations and include performance of any checks associated with evaluation of the target component name or with implicit conversion of the source value to the component subtype.

4.4.1.1. Record Update Expressions

For a record update expression of type T the following are required.

Legality Rules

  1. The record_component_association_list shall have one or more record_component_associations, each of which shall have a non-others component_choice_list and an expression.
  1. Each selector_name of each record_component_name shall denote a distinct non discriminant component of T.
  1. Each record_component_association‘s associated components shall all be of the same type. The expected type and applicable index constraint of the expression is defined as for a record_component_association occurring within a record aggregate.
  1. Each selector of all component_choice_lists of a record update expression shall denote a distinct component.

Dynamic Semantics

  1. For each component for which an expression is provided, the expression value is assigned to the corresponding component of the result object. The order in which the components are updated is unspecified.

[Components in a record update expression must be distinct. The following is illegal

Some_Record'Update
  (Field_1 => ... ,
   Field_2 => ... ,
   Field_1 => ... ); -- illegal; components not distinct

because the order of component updates is unspecified.]

4.4.1.2. Array Update Expressions

For an array update expression of type T the following are required.

Legality Rules

  1. Each array_component_association of the attribute reference shall have one or more array_component_associations, each of which shall have an expression.
  1. The expected type and applicable index constraint of the expression is defined as for an array_component_association occurring within an array aggregate of type T. The expected type for each discrete_choice is the index type of T.
  1. The reserved word others shall not occur as a discrete_choice of an array_component_association of the attribute_reference.

Dynamic Semantics

  1. The discrete choices and array component expressions are evaluated. Each array component expression is evaluated once for each associated component, as for an array aggregate. For each such associated component of the result object, the expression value is assigned to the component.
  1. Evaluations and updates are performed in the order in which the array_component_associations are given; within a single array_component_association, in the order of the discrete_choice_list; and within the range of a single discrete_choice, in ascending order.

[Note: the Update attribute for an array object allows multiple assignments to the same component, as in either

Some_Array'Update (1 .. 10 => True, 5 => False)

or

Some_Array'Update (Param_1'Range => True, Param_2'Range => False)
-- ok even if the two ranges overlap]

4.4.1.3. Multi-dimensional Array Update Expressions

For a multi-dimensional array update expression of type T the following are required.

Legality Rules

  1. The expected type and applicable index constraint of the expression of a multidimensional_array_component_association are defined as for the expression of an array_component_association occurring within an array aggregate of type T.
  1. The length of each index_expression_list shall equal the dimensionality of T. The expected type for each expression in an index_expression_list is the corresponding index type of T.

Dynamic Semantics

  1. For each multidimensional_array_component association (in the order in which they are given) and for each index_expression_list (in the order in which they are given), the index values of the index_expression_list and the expression are evaluated (in unspecified order) and the expression value is assigned to the component of the result object indexed by the given index values. Each array component expression is evaluated once for each associated index_expression_list.

Examples

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
package Update_Examples
  with SPARK_Mode
is
   type Rec is record
      X, Y : Integer;
   end record;

   type Arr is array (1 .. 3) of Integer;

   type Arr_2D is array (1 .. 3, 1 .. 3) of Integer;

   type Nested_Rec is record
      A : Integer;
      B : Rec;
      C : Arr;
      D : Arr_2D;
   end record;

   type Nested_Arr is array (1 .. 3) of Nested_Rec;

   -- Simple record update
   procedure P1 (R : in out Rec)
     with Post => R = R'Old'Update (X => 1);
   -- this is equivalent to:
   --   R = (X => 1,
   --        Y => R'Old.Y)

   -- Simple 1D array update
   procedure P2 (A : in out Arr)
     with Post => A = A'Old'Update (1 => 2);
   -- this is equivalent to:
   --   A = (1 => 2,
   --        2 => A'Old (2),
   --        3 => A'Old (3));

   -- 2D array update
   procedure P3 (A2D : in out Arr_2D)
     with Post => A2D = A2D'Old'Update ((1, 1) => 1,
                                        (2, 2) => 2,
                                        (3, 3) => 3);
   -- this is equivalent to:
   --   A2D = (1 => (1 => 1,
   --                2 => A2D'Old (1, 2),
   --                3 => A2D'Old (1, 3)),
   --          2 => (2 => 2,
   --                1 => A2D'Old (2, 1),
   --                3 => A2D'Old (2, 3)),
   --          3 => (3 => 3,
   --                1 => A2D'Old (3, 1),
   --                2 => A2D'Old (3, 2)));

   -- Nested record update
   procedure P4 (NR : in out Nested_Rec)
     with Post => NR = NR'Old'Update (A => 1,
                                      B => NR'Old.B'Update (X => 1),
                                      C => NR'Old.C'Update (1 => 5));
   -- this is equivalent to:
   --   NR = (A => 1,
   --         B.X => 1,
   --         B.Y => NR'Old.B.Y,
   --         C (1) => 5,
   --         C (2) => NR'Old.C (2),
   --         C (3) => NR'Old.C (3),
   --         D => NR'Old.D)

   -- Nested array update
   procedure P5 (NA : in out Nested_Arr)
     with Post =>
       NA = NA'Old'Update (1 => NA'Old (1)'Update
                                  (A => 1,
                                   D => NA'Old (1).D'Update ((2, 2) => 0)),
                           2 => NA'Old (2)'Update
                                  (B => NA'Old (2).B'Update (X => 2)),
                           3 => NA'Old (3)'Update
                                  (C => NA'Old (3).C'Update (1 => 5)));
   -- this is equivalent to:
   --   NA = (1 => (A => 1,
   --               B => NA'Old (1).B,
   --               C => NA'Old (1).C,
   --               D => NA'Old (1).D),
   --         2 => (B.X => 2,
   --               B.Y => NA'Old (2).B.Y,
   --               A => NA'Old (2).A,
   --               C => NA'Old (2).C,
   --               D => NA'Old (2).D),
   --         3 => (C => (1 => 5,
   --                     2 => NA'Old (3).C (2),
   --                     3 => NA'Old (3).C (3)),
   --               A => NA'Old (3).A,
   --               B => NA'Old (3).B,
   --               D => NA'Old (3).D));

end Update_Examples;

4.5. Operators and Expression Evaluation

Ada grants implementations the freedom to reassociate a sequence of predefined operators of the same precedence level even if this changes the behavior of the program with respect to intermediate overflow (see Ada 2012 RM 4.5). SPARK 2014 assumes that an implementation does not take advantage of this permission; in particular, a proof of the absence of intermediate overflow in this situation may depend on this assumption.

A SPARK 2014 tool is permitted to provide a warning where operators may be re-associated by a compiler.

[The GNAT Ada 2012 compiler does not take advantage of this permission. The GNAT compiler also provides an option for rejecting constructs to which this permission would apply. Explicit parenthesization can always be used to force a particular association in this situation.]

4.6. Type Conversions

No extensions or restrictions.

4.7. Qualified Expressions

No extensions or restrictions.

4.8. Allocators

Legality Rules

  1. The use of allocators is not permitted.

4.9. Static Expressions and Static Subtypes

No extensions or restrictions.