ParaSail Universal types in Annotations

As explained in the prior entry, ParaSail has four universal types, Univ_Integer, Univ_Real, Univ_Character, and Univ_String, with corresponding literals.  The universal numeric types have the usual arithmetic operators, and the universal character and string types have the usual operations for concatenation and indexing.  In some ways values of the universal types may be thought of as abstract mathematical objects, while the values of "normal" types are the typical concrete representations of such mathematical objects, with attendant limitations in range or precision.  To connect a normal, concrete type to a corresponding universal type, the type defines the operator "from_univ" to convert from the universal type to the concrete type, and "to_univ" to convert back to the universal type.

In the prior entry, we learned that by defining "from_univ" a type can use the corresponding literal notation.  For example, imagine an Integer interface:

interface Integer<First, Last : Univ_Integer> is
    operator "from_univ"
      (Univ : Univ_Integer {Univ in First .. Last})
      -> Integer;
    operator "to_univ"(Int : Integer)
      -> Result : Univ_Integer {Result in First .. Last};
    operator "+"(Left, Right : Integer) -> Integer;
    operator "-"(Left, Right : Integer) -> Integer;
    ...
end interface Integer;

Because the "from_univ" operator is defined from Univ_Integer, integer literals are effectively overloaded on any type produced by instantiating the Integer interface.  So what about the "to_univ" operator?  If "to_univ" is provided, then ParaSail allows the use of a special convert-to-universal notation "[[...]]", which would typically be used in annotations, such as:

{ [[Left]] + [[Right]] in First .. Last }

This is equivalent to:

{ "to_univ"(Left) + "to_univ"(Right) in First .. Last }

This notation is intended to be a nod to the double bracket notation used in denotational semantics to represent the denotation or abstract meaning of a program expression. Using this notation we can give a more complete definition of the semantics of the Integer interface:

interface Integer<First, Last : Univ_Integer> is
    operator "from_univ"
      (Univ : Univ_Integer {Univ in First .. Last})
      -> Integer;
    operator "to_univ"(Int : Integer)
      -> Result : Univ_Integer {Result in First .. Last};
    operator "+"(Left, Right : Integer 
          {[[Left]] + [[Right]] in First .. Last}) 
      -> Result : Integer 
          {[[Result]] == [[Left]] + [[Right]]};
    operator "-"(Left, Right : Integer 
          {[[Left]] - [[Right]] in First .. Last}) 
      -> Result : Integer 
          {[[Result]] == [[Left]] - [[Right]]};
    ...
end interface Integer;

Here we are defining the pre- and postconditions for the various operators by expressing them in terms of corresponding universal values, analogous to the way that denotational semantics defines the meaning of a program by defining a transformation from the concrete program notations to corresponding abstract mathematical objects.