Prev Up Next
Go backward to 6.1.5 Free Specifications
Go up to 6.1 Structured Specifications
Go forward to 6.1.7 Closed Specifications

6.1.6 Local Specifications

      LOCAL-SPEC ::= local-spec SPEC SPEC

A local specification LOCAL-SPEC is written:

local SP1 within SP2

It is equivalent to writing:

{ SP1 then SP2 } hide SY1, ..., SYn
where SY1, ..., SYn are all the symbols declared by SP1 that are not already in the current local environment. Thus the symbols SY1, ..., SYn are only for local use in (SP1 and) SP2. The hiding must not affect symbols that are declared only in SP2 (thus operation or predicate symbols declared in SP2 should not have sorts declared by SP1 in their profiles).
CoFI Document: CASL/Summary-v1.0 -- Version: 1.0 -- 22 October 1998.
Comments to

Prev Up Next