Go backward to Structured Specifications
Go up to CASL
Go forward to Union and Extension

Translation and Hiding

The symbols declared by a specification may be translated to different ones, and they may be hidden.
Translation is needed primarily to allow the reuse of specifications with change of notation, which is important since different applications may require the use of different notation for the same entities. But also when specifications that have been developed in parallel are to be combined, some notational changes may be needed for consistency.

Hiding symbols ensures that they are not available to the user of the specification, which is appropriate for symbols that denote auxiliary entities, introduced by the specifier merely to facilitate the specification, and not necessarily to be implemented. CASL tentatively provides two constructs for hiding: one where the symbols to be hidden are listed directly (other symbols remaining visible--although hiding a sort entails hiding all function and predicate symbols whose profile involves that sort), the other where only the symbols to be `revealed' are listed.


CoFI Tentative Document: Mosses97TAPSOFT --TAPSOFT'97-- April 1997.
Comments to pdmosses@brics.dk