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.