The grammar description formalism

The grammar rules used to describe the Metaslang language use the conventions of (extended) BNF. For example, a grammar rule like:

wiffle ::= waffle [ waffle-tail ] | piffle { + piffle }*

defines a wiffle to be: either a waffle optionally followed by a waffle-tail, or a sequence of one or more piffles separated by terminal symbols + . (Further rules would be needed for waffle, waffle-tail and piffle.) In a grammar rule the left-hand side of ::= shows the kind of construct being defined, and the right-hand side shows how it is defined in terms of other constructs. The sign | separates alternatives, the square brackets [ ... ] enclose optional parts, and the curly braces plus asterisk { ... }* enclose a part that may be repeated any number of times, including zero times. All other signs stand for themselves, like the symbol + in the example rule above.

In the grammar rules terminal symbols appear in a bold font. Some of the terminal symbols used, like | and {, are very similar to the grammar signs like | and { as described above. They can hopefully be distinguished by their bold appearance.

Grammar rules may be recursive: a construct may be defined in terms of itself, directly or indirectly. For example, given the rule:

piffle ::= 1 | M { piffle }*

here are some possible piffles:

1 M M1 M111 MMMM M1M1

Note that the last two examples of piffles are ambiguous. For example, M1M1 can be interpreted as: M followed by the two piffles 1 and M1, but also as: M followed by the three piffles 1, M, and another 1. Some of the actual grammar rules allow ambiguities; the accompanying text will indicate how they are to be resolved.

Models

spec ::= spec-form op ::= op-name

The term spec is used as short for spec-form. The semantics of Metaslang specs is given in terms of classes of models. A model is an assignment of sorts (sets of values) to all the sort-names and of "sorted" values to all the op-names declared -- explicitly or implicitly -- in the spec. The notion of value includes numbers, strings, arrays, functions, etcetera. A sorted value can be thought of as a pair (S, V), in which S is a sort and V is a value that is an inhabitant of S. For example, the expressions 0 : Nat and 0 : Integer correspond, semantically, to the sorted values (N, 0) and (Z, 0), respectively, in which N stands for the set of natural numbers {0, 1, 2, ...}, and Z for the set of integers {..., -2, -1, 0, 1, 2, ...}. (For historical reasons, the term sort is traditionally used in specification languages with essentially the same meaning as the term type in programming languages.) In Metaslang, op is used -- again for historical reasons -- for declared names representing values. The term "op" is used as an abbreviation for "op-name". (Op for operator, a term used, again, for historical reasons, although including things normally not considered operators.) For example, given this spec:

spec sort Even op next : Even -> Even axiom nextEffect is fa(x : Even) ~(next x = x) endspec

one possible model (out of many!) is the assignment of the even integers to Even, and of the function that increments an even number by 2 to next.

Each model has to respect sorting; for example, given the above assignment to Even, the function that increments a number by 1 does not map all even numbers to even numbers, and therefore can not -- in the same model -- be assigned to next. Additionally, the axioms of the spec have to be satisfied by the model. The axiom labeled nextEffect above states that the function assigned to op-name next maps any value of the sort assigned to sort-name Even to a different value. So the squaring function, although sort-respecting, could not be assigned to next since it maps 0 to itself.

If all sort-respecting combinations of assignments of sorts to sort-names and ops to op-names fail the axioms test, the spec has no models and is called inconsistent. Although usually undesirable, an inconsistent spec is not by itself considered erroneous. The Specware system does not attempt to detect inconsistencies, but associated provers can sometimes be used to find them. Not always; in general it is undecidable whether a spec is consistent or not.

In general, the meaning of a construct in a model depends on the assignments of that model, and more generally on an environment: a model possibly extended with assignments to local-variables. For example, the meaning of the claim fa(x : Even) ~(next x = x) in the axiom nextEffect depends on the meanings of Even and next, while the sub-expression next x, for example, also depends on an assignment (of an "even" value) to x. To avoid laborious phrasings, the semantic descriptions use language like "the function next applied to x" as shorthand for this lengthy phrase: "the function assigned in the environment to next applied to the value assigned in the environment to x".

When an environment is extended with an assignment to a local-variable, any assignments to synonymous ops or other local-variables are superseded by the new assignment in the new environment. In terms of Metaslang text, within the scope of the binding of local-variables, synonymous ops and earlier introduced local-variables (that is, having the same name) are "hidden"; any use of the name in that scope refers to the textually most recently introduced local-variable. For example, given:

def x = "op-x" def y = let v = "let-v" in x def z = let x = "let-x" in x

the value of y is "op-x" (op x is not hidden by the local-variable v of the let-binding), whereas the value of z is "let-x" (op x is hidden by the local-variable x of the let-binding).

Sort-correctness

If no sort-respecting combinations of assignments exist for a given spec, it is considered incorrect, and is said to have a sort error (or type error). This is determined by Specware while elaborating the spec, and signaled as an error. Sort-incorrectness differs from inconsistency in that the meaning of the axioms does not come into play, and the question whether an incorrect spec is consistent is moot.

To be precise, there are subtle and less subtle differences between sort-incorrectness of a spec and its having no sort-respecting combinations of assignments. For example, the following spec is sort-correct but has no models:

spec sort Empty = | Just Empty op IdoNotExist : Empty endspec

The explanation is that the sort-definition for Empty generates an implicit axiom that all inhabitants of the sort Empty must satisfy, and for this recursive definition the axiom effectively states that such creatures can't exist: the sort Empty is uninhabited. That by itself is no problem, but precludes a sort-respecting assignment of an inhabitant of Empty to op IdoNotExist. So the spec, while sort-correct, is actually inconsistent. See further under Sort-definitions.

Here is a sort-incorrect spec that has sort-respecting combinations of assignments:

spec sort Outcome = | Positive | Negative sort Sign = | Positive | Zero | Negative def whatAmI = Positive endspec

Here there are two constructors Positive of different sorts, the sort Outcome and the sort Sign. That by itself is fine, but when such "overloaded" constructors are used, the context must give sufficient information which is meant. Here, the use of Positive in the definition for op whatAmI leaves both possibilities open; as used it is sort-ambiguous. Metaslang allows omitting sort information provided that, given a sort assignment to all local-sort-variables in scope, unique sorts for all sorted constructs, such as expressions and patterns, can be inferred from the context. If no complete and unambiguous sort-assignment can be made, the spec is not accepted by the Specware system. Sort-ambiguous expressions can be disambiguated by using a sort annotation, as described under Annotated-expressions. In the example, the definition of whatAmI can be disambiguated in either of the following ways:

def whatAmI : Sign = Positive def whatAmI = Positive : Sign

Also, if the spec elsewhere contains something along the lines of:

op signToNat : Sign -> Nat def sw = signToNat whatAmI

that is sufficient to establish that whatAmI has sort Sign and thereby disambiguate the use of Positive. See further under Op-definitions and Structors.

Constructive

When code is generated for a spec, complete "self-contained" code is only generated for sort-definitions and op-definitions that are fully constructive. Non-constructiveness is "contagious": a definition is only constructive if all components of the definition are. The sort of a sort-name without definition is not constructive. A sort is only constructive if all component sorts are. An op without definition is non-constructive, and so is an op whose sort is non-constructive. A quantification is non-constructive. The built-in polymorphic equality predicate = is only constructive for discrete sorts (see below).

A sort is called discrete if the equality predicate = for that sort is constructive. The built-in sorts Integer, Nat, Boolean, Char and String are all discrete. Sort List S is discrete when S is. All function sorts are non-discrete (even when the domain sort is the unit sort). Sum sorts, product sorts and record sorts are discrete whenever all component sorts are. Subsort (S | P) is discrete when supersort S is. (Predicate P need not be constructive: the equality test is that of the supersort.) Quotient sort S / Q is discrete when predicate Q is constructive. (Sort S need not be discrete: the equality test on the quotient sort is just the predicate Q applied to pairs of members of the Q-equivalence classes.)