Like a programming language, SpecL has a formal syntax. The complete SpecL syntax is given in Appendix D. The syntactic notation is a style of BNF, as is used to define programming language syntax. Readers unfamiliar with BNF notation should consult a text on programming languages, or other suitable reference.

The lexical elements of SpecL are similar to the lexical elements of a programming language. SpecL specifications contain identifiers that denote the objects, operations, and other named components of the specification. Literal values, such as numbers and strings, are used in an SpecL specification. The formal sections of a specification contain expressions that use operator symbols similar to those available in a programming language. These and other lexical elements are defined in the following subsections.

2.1. Identifiers

An SpecL identifier starts with a letter, followed by zero or more letters, digits or underscore characters, followed at the end by an optional single-quote character. Letters include both upper and lower case letters, "A" through "Z" and "a" through "z". Digits are "0" through "9". The underscore character is "_". The single quote character is "'".

The intent of the trailing single quote in an identifier is to provide a prime notation. For example, if "Name" is an identifier in a specification, then "Name'" is read Name prime. "Name" and "Name'" will typically be used in a related context. For example if "Name" is the input to an operation, then "Name'" could be an output. Later examples of illustrate typical uses of the prime notation.

Examples of legal identifiers are the following:

Name    Name'   xyz    XYZ   Object25   operation_15

Literal values in SpecL are numbers, strings, boolean, and empty values. Numbers are composed of one or more digits, with an optional embedded decimal point. Numbers must begin and end with a digit. Hence, 1.0 and 0.1 are a legal numbers, but 1. and .1 are not legal.

String-valued literals are surrounded with double quote characters. A double quote character can be embedded within a string by preceding it with a backslash character.

A boolean literal is denoted by the standard identifier true or false. The empty value is denoted by the standard identifier nil or empty

Examples of legal literal values are the following:

1   1234   1.0   123.4567   "abc"   ""   "Say \"hey\""
true   false   nil   empty

In languages with formal syntax, punctuation symbols are used to separate different syntactic constituents. Table 2 summarizes the use of the SpecL syntactic punctuation symbols.

Further examples of the use of punctuation symbols appear throughout the report.

SpecL definitions contain symbolic expressions in a number of contexts. These expressions are similar to expressions in programming languages. The legal operator symbols in SpecL are the following:

!=   #   &   (   )   *   +   ,   -   ->   .   .-   ..   ...   .:   .<   .>   /   :   ::=   :=   ;
   <   <=   <=>   <>   =   ==   =>   >   >=   ?   ?->   ?.   ?<   [   ]   ^   {   |   }   ~=

In the interest of notational clarity, a distinction is made in this manual between the terms "operation" and "operator". "Operation" refers to a user- defined component of an SpecL specification, defined with operation keyword. "Operator" refers to a built-in expression operator, such as `+', `*', etc.

As in many programming languages, some symbols in SpecL are overloaded. That is, the same symbol has two different meanings depending on the context of its use. For example, the comma is an overloaded symbol in SpecL. In some contexts it is used as a separator and in other contexts as an expression operator. Examples in later sections of the report illustrate the use of all operators. The formal syntax in Appendix D defines all syntactically legal usages.

2.4. Comments

SpecL comments are enclosed in bracket pairs (* and *). Comments cannot be nested. Comments may also be specified in the style of the Ada programming language, using the "--" symbol. In this style, a comment begins with "--" and ends at the physical end of line.

2.5. Scoping

The concept of scoping in SpecL is comparable to other programming and specification languages. Namely, a scope is a "namespace", in which names take on specific meanings. The general purpose of a scope is to ensure that names have consistent meanings within a particular context. For example, the same name cannot be used to define two different objects in the same scope.

2.5.1. Declaration Scopes

When defining a specification, there is an outermost scope called the "top- level". The following declarations can appear at the top-level, in any order, any number of times:

• modules
• objects
• operations
• values
• variables
• axioms
• theorems
• attributes
• rules

In addition to the top-level scope, the following three declarations define their own local scopes:

• modules
• objects
• operations

Within scopes, some name overloading can occur. Overloading means that the same name can have multiple definitions in one scope, subject to specific rules. These overloading rules are as follows:

1. The same name may be used for two or more operations, as long as the input signatures of the operations differ. See the discussion of operation overloading for further details.
2. The same name may be used for an object and one or more operations, as long as the overloading constraints are met for the operation definitions. See the discussion of object construction for further details.
3. The same name may be used for an object and a parent module, as long as the preceding two rules are satisfied. See the discussion of module scoping for further details.
4. The same name may be used on the left-hand side of two or more grammar rules See the discussion of formal grammar rules for further details.

1. Two or more objects cannot have the same name in the same scope.
2. The names of values, variables, axioms, theorems, and attributes must be entirely unique within any scope. When a name is used to define any one of these five constructs, then that name cannot be used for any other purpose in the scope.

A module scope contains exactly the same kind of declarations that appear at the top level. A module provides a well-defined boudary around a set of related definitions.

The purpose of modules is to promote the organized decomposition of a specification, into managebly-sized parts. The larger a specification becomes, the more important is its modularization.

In terms of scoping, a module provides a tight boundary around its contents. By default, all of the names declared in a module are visible only in its scope, and no place else. Module contents can be made visible between modules using qualified references and import/export controls. These topics are covered in detail in Section .

2.5.1.2. Object and Operation Scopes

Objects and operations define much smaller scopes than modules. The scope of an object contains the names of its component parts. The scope of an operation contains its input/output parameters.

Most significantly, objects and operations scopes are flat, i.e., they cannot be nested. In particular, this means that an object definition does not contain other object definitions. The same applies to operations.

Complete details of object and operation scoping are are presented in Section 3.

2.5.2. Expression Scopes

Any parenthesized expression sequence defines a scope, in which local variables can be declared with a let expression. Such expression scopes can be used as function bodies, or any other context in which an expression is legal.

Expression scopes are also created by quatifier expressions, in which quantified variables are defined in a scope that is local just to the quantifier. Complete details of expression scopes are covered in Section 7 of the manual.

2.5.3. Scope Visibilty

The names defined in a scope are visible throughout that scope, as well as to any nested inner scopes. Visibility within nested scopes follows the open- scoping rules typical in other programming and specification languages:

1. All symbols defined in an outer scope are visible within all nested inner scopes, to all depths of nesting.
2. If an inner scope redefines a name that appears in an outer scope, the inner definition hides the outer definition.

object A = ... ;        (* Top level definition of object A *)
object B = ... ;        (* Top level definition of object B *)
variable x:integer;     (* Top level definition of variable x *)

module M;
    object A = ... ;    (* This definition of A hides top-level definition *)
    variable x:string;  (* This definition of x hides top-level definition *)

    operation O(x:A, y:B)   (* This definition of x hides both outer defs *)
        ...
    end O;
end M;

The parameter definitions in O refer to M's definition of A and the top-level definition of B. Since A is defined locally in M, that definition of A is used in O's signature. Since B has no definition in M, the top-level definition of B is used in O's signature.

2.6. Specification Files

An SpecL specification can be defined in one or more files. There is no required correspondence between file names and the any of the names defined in a specification. Therefore, a file name may or may not be the same as some element of a specification, at the choice of the specifier.

The only filing constraint is that a specification declaration cannot span file boundaries. That is, all individual declarations must begin and end in the same file.

By convention, SpecL files are given the extension ".sl". This convention is recommended, but not required.

To process a set of specification files, they are presented by name to the specification checker. In a command-line context, such a presentation looks like this:

Specl file1.sl ... filen.sl

There are some further details of file processing related to specification modules, and their inter-connections. These details are covered in Section 5 of the reference manual.

2.7. Includes

An include declaration is used to include a source file directly into the text of a specification. Specifically, include opens a file, and inserts the verbatim contents of the file at the location where the include declaration appears.

The include declaration has the following form:

include file-path

A file path without a leading slash is relative to the specification file in which the include appears. Specifically, for a specification file "X.sl" stored in directory D, all relative includes paths in X.sl are interpreted with D as the parent directory.

Includes can appear any where in a specification that a top-level declaration can appear. All includes are processed temporally before the syntactic and semantic checking of a specification. Hence, processing an include is an entirely lexical matter, equivalent to the contents of a file having been manually entered at the point where the include appears.

Given this purely lexical form of inclusion, there are no restrictions on the contents of included files, other than the normal rules of syntax and semantics. That is, the contents of an included file must be syntactically and semantically legal at their place of inclusion.

Recall from above the rule that a declaration must begin and end in the same file. For the purposes of this definition, the "same file" means after all include declarations have been processed. Hence, a single declaration could in fact span the boundaries of included files. However, there is no particularly good reason for this to happen.

2.8. The Top-Level Interactive Scope

After files are processed, the SpecL checker can enter an interactive processing loop, very much like interactive programming languages such as Lisp, ML, Python, and others. From the command line, the interactive loop is entered by supplying the "-i" argument, as in

specl -i file1.sl ... filen.sl

SpecL keywords are distinguished words that can only be used in particular syntactic contexts. Keywords cannot be used as identifiers. The following are the legal SpecL keywords:

actions   all   and   attribute   ax   axiom   begin   components   dataflow
define   else   end   eq   equations   except   exists   export   extends
forall   foreach   from   func   function   if   iff   implies   import   in
inputs   is   lambda   let   mod   module   not   obj   object   op   operation
operations   ops   or   out   outputs   parts   post   postcondition   pre
precondition   return   then   theorem   thm   val   value   var   variable
where   while   xor

The reader should note that in some cases, certain keywords are synonymous. That is, two or more SpecL keywords may have exactly the same meaning. The existence of synonymous keywords is an historical feature, intended originally to provide convenient abbreviations for long keywords. While the language would probably be more clearly defined if synonymous keywords were eliminated, they have been retained for compatibility with existing SpecL specifications. Table 3 shows all synonymous keywords and symbols. The keywords in a given row of the table are synonymous. The usages shown in the table are explained further in later sections of the manual.

SpecL standard identifiers are names that have pre-defined meanings. The difference between keywords and standard identifiers is that keywords appear in particular syntactic contexts, whereas standard identifiers appear in the more general syntactic context of an identifier. Other than syntactic context, there is no practical difference between keywords and standard identifiers, since neither class of symbol can be redefined by the user. The SpecL standard identifiers are the following:

boolean  description   empty   false   integer   nil   real   string   true

Other than the syntactic rules for identifiers, there are no required conventions for the names of specification elements. The following conventions are observed in this reference manual, and in the examples it references:

1. ... spell these out, please ...