Relational attributes can be viewed as "syntactic sugaring" for a functional definition of formal relations. SpecL users who prefer to limit the number of constructs used in a specification may prefer not to use relational attributes.

Formally, the relation between two objects is represented as a function (or operation) with an appropriate signature. Consider the following bi-directional relation:

define object attribute R;


object O1 is
    ...
    R: O2;
end O1;


object O2 is
    ...
    R: O1
end O2

object O1 is
    ...
end O1;


object O2 is
    ...
end O2;


function O1_R_O2(O1):(O2);


function O2_R_O1(O2):(O1);

object O3 is
    ...
    R: O1,O2;
end O3;

An additional consideration regarding relational definitions concerns the future enhancement of the SpecL development environment. A near-term goal is to provide a formal verification environment for SpecL, so that properties of a specification can be mechanically verified. The most effective means to provide such verification is to translate SpecL into an existing formal language for which mechanized verification support already exists. Candidates for the target of translation include EHDM [Rushby 91] and HOL [Gordon 87]). These and similar systems do not provide direct verification support for relational definitions. Therefore, translation of relations into functional form will be necessary if mechanized verification support is to be provided for SpecL in the foreseeable future.