**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:

Because the "from_univ" operator is defined from Univ_Integer, integer literals are effectively overloaded on any type produced by instantiating the IntegerinterfaceInteger<First, Last : Univ_Integer>isoperator"from_univ" (Univ : Univ_Integer {UnivinFirst .. Last}) -> Integer;operator"to_univ"(Int : Integer) -> Result : Univ_Integer {ResultinFirst .. Last};operator"+"(Left, Right : Integer) -> Integer;operator"-"(Left, Right : Integer) -> Integer; ...endinterfaceInteger;

**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]]This is equivalent to:inFirst .. Last }

{ "to_univ"(Left) + "to_univ"(Right)This notation is intended to be a nod to the double bracket notation used ininFirst .. Last }

*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**:

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.interfaceInteger<First, Last : Univ_Integer>isoperator"from_univ" (Univ : Univ_Integer {UnivinFirst .. Last}) -> Integer;operator"to_univ"(Int : Integer) -> Result : Univ_Integer {ResultinFirst .. 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]]}; ...endinterfaceInteger;

## No comments:

## Post a Comment