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

op ::= op-name

In Metaslang, op is used used as an abbreviation for "op-name", where op-names are declared names representing values. (Op for operator, a term used for historical reasons, although including things normally not considered operators.)

spec ::= spec-form

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 sets of values (called "types") to all the type-names and of "typed" values to all the ops declared -- explicitly or implicitly -- in the spec. The notion of value includes numbers, strings, arrays, functions, etcetera. A typed value can be thought of as a pair (T, V), in which T is a type and V is a value that is an inhabitant of T. For example, the expressions 0 : Nat and 0 : Integer correspond, semantically, to the typed 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 example, given this spec:

spec type 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 typing; 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 claims (axioms, theorems and conjectures) of the spec have to be satisfied in the model. The axiom labeled nextEffect above states that the function assigned to op next maps any value of the type assigned to type-name Even to a different value. So the squaring function, although type-respecting, could not be assigned to next since it maps 0 to itself.

If all type-respecting combinations of assignments of types to type-names and values to ops fail the one or more claims, the spec has no models and is called inconsistent. Although usually undesirable, an inconsistent spec is not by itself considered ill formed. 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 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 simple-name) are "hidden"; any use of the simple-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).

Type-correctness

Next to the general requirement that each model respects typing, there are specific restrictions for various constructs that constrain the possible types for the components. For example, in an application f(x), the type of the actual-parameter x has to match the domain type of function f. These requirements are stated in the relevant sections of this language manual. If no type-respecting combinations of assignments meeting all these requirements exist for a given spec, it is considered type-incorrect and therefore ill formed. This is determined by Specware while elaborating the spec, and signaled as an error. Type-incorrectness differs from inconsistency in that the meaning of the claims does not come into play, and the question whether an ill-formed spec is consistent is moot.

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

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

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

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

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

Here there are two constructors Positive of different types, the type Outcome and the type 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 type-ambiguous. Metaslang allows omitting type information provided that, given a type assignment to all local-type-variables in scope, unique types for all typed constructs, such as expressions and patterns, can be inferred from the context. If no complete and unambiguous type-assignment can be made, the spec is not accepted by the Specware system. Type-ambiguous expressions can be disambiguated by using a type 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 type 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 type-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 type of a type-name without definition is not constructive. A type is only constructive if all component types are. An op without definition is non-constructive, and so is an op whose type is non-constructive. A quantification is non-constructive. The polymorphic inbuilt-op = for testing equality and its inequality counterpart ~= are only constructive for discrete types (see below).

A type is called discrete if the equality predicate = for that type is constructive. The inbuilt and base-library types Boolean, Integer, NonZeroInteger, Nat, PosNat, Char, String and Compare are all discrete. Types List T and Option T are discrete when T is. All function types are non-discrete (even when the domain type is the unit type). Sum types, product types and record types are discrete whenever all component types are. Subtype (T | P) is discrete when supertype T is. (Predicate P need not be constructive: the equality test is that of the supertype.) Quotient type T / Q is discrete when predicate Q is constructive. (Type T need not be discrete: the equality test on the quotient type is just the predicate Q applied to pairs of members of the Q-equivalence classes.)