Declarations

Import-declarations

A spec may contain one or more import-declarations. On elaboration, these are "expanded". The effect is as if the bodies of these imported specs (themselves in elaborated form, which means that all import-declarations have been expanded, all translations performed and all shorthand employs of names have been resolved to full names, after which only declarations or definitions of sorts, ops and axioms are left) is inserted in place in the receiving spec.

For example, the result of

spec import spec sort A.Z op b : Nat -> Z end sort A.Z = String def b = toString endspec

is this "expanded" spec:

spec sort A.Z op b : Nat -> A.Z sort A.Z = String def b = toString endspec

For this to be correct, the imported specs must be correct by themselves; in addition, the result of expanding them in place must result in a correct spec.

There are a few restrictions, which are meant to catch unintentional naming mistakes. First, if two different imported specs each introduce a sort or op with the same (full) name, the introductions must be identical declarations or definitions, or one may be a declaration and the other a "compatible" definition. For example, given

S1 = spec op e : Int end S2 = spec op e : Char end S3 = spec def e = 0 end

the specs S1 and S3 can be imported together, but all other combinations of two or more co-imported specs are incorrect. This restriction is in fact a special case of the general requirement that import expansion must result in a correct spec. Secondly, a sort-name introduced in any of the imported specs cannot be re-introduced in the receiving spec except for the case of an "imported" declaration together with a definition in the receiving spec. Similarly for op-names, with the addition that an op-definition in the receiving spec must be compatible with an op-declaration for the same name in an imported spec. The latter is again a special case of the general requirement that import expansion must result in a correct spec.

What is specifically excluded by the above, is giving a definition of a sort or op in some spec, import it, and then redefining or declaring that sort or op with the same full name in the receiving spec.

import-declaration ::= import spec-term

Sample import-declarations

import Lookup

An import-declaration is contained in some spec-form, and to elaborate that spec-form the spec-term of the import-declaration is elaborated first, giving some spec S. The import-declaration has then the effect as if the declarations of the imported spec S are expanded in place. This cascades: if spec A imports B, and spec B imports C, then effectively spec A also imports C. An important difference with earlier versions of Specware than version 4 is that multiple imports of the same spec have the same effect as a single import.

If spec A is imported by B, each model of B is necessarily a model of A (after "forgetting" any names newly introduced by B). So A is then refined by B, and the morphism from A to B is known as the "import morphism". As it does not involve translation of sort-names or op-names, it can be denoted by morphism A -> B {}.

Sort-declarations

sort-declaration ::= sort sort-name [ formal-sort-parameters ] formal-sort-parameters ::= local-sort-variable | ( local-sort-variable-list ) local-sort-variable ::= name local-sort-variable-list ::= local-sort-variable { , local-sort-variable }*

Restriction. Each local-sort-variable of the formal-sort-parameters must be a different name.

Sample sort-declarations:

sort Date sort Array a sort Map(a, b)

Every sort-name used in a spec must be declared (in the same spec or in an imported spec, included the "built-in" specs that are always implicitly imported). A sort-name may have sort parameters. Given the example sort-declarations above, some valid sorts that can be used in this context are Array Date, Array (Array Date) and Map (Nat, Boolean).

In a model of the spec, a sort is assigned to each unparameterized sort-name, while an infinite family of sorts is assigned to parameterized sort-names "indexed" by tuples of sorts, that is, there is one family member, a sort, for each possible assignment of sorts to the local-sort-variables. So for the above example sort-declaration of Array one sort must be assigned to Array Nat, one to Array Boolean, one to Array (Array Date), and so on. These assigned sorts could all be the same sort, or perhaps all different, as long as the model respects sorting.

Sort-definitions

sort-definition ::= sort sort-name [ formal-sort-parameters ] equals sort

Sample sort-definitions:

sort Date = {year : Nat, month : Nat, day : Nat} sort Array a = List a sort Map(a, b) = (Array (a * b) | key_uniq?)

In each model, the sort assigned to the sort-name must be the same as the right-hand-side sort. For parameterized sorts, this extends to all possible assignments of sorts to the local-sort-variables, taking the right-hand sorts as interpreted under each of these assignments. So, for the example, Map(Nat, Char) is the same sort as (Array (Nat * Char) | key_uniq?), and so on.

With recursive sort-definitions, there are additional requirements. For example, consider

sort Stack a = | Empty | Push {top : a, pop : Stack a}

This means that for each sort a there is a value Empty of sort Stack a, and further a function Push that maps values of sort {top : a, pop : Stack a} to Stack a. Furthermore, the sort assigned to Stack a must be such that all its inhabitants can be constructed exclusively and uniquely in this way: there is one inhabitant Empty, and all others are the result of a Push. Finally -- this is the point -- the sort in the model must be such that its inhabitants can be constructed this way in a finite number of steps. So there can be no "bottom-less" stacks: deconstructing a stack using

def fa(a) hasBottom? (s : Stack a) : Boolean = case s of | Empty -> true | Push {top, pop = rest} -> hasBottom? rest

is a procedure that is guaranteed to terminate, always resulting in true.

In general, sort-definitions generate implicit axioms, which for recursive definitions imply that the sort is not "larger" than necessary. In technical terms, in each model the sort is the least fixpoint of a recursive domain equation.

Op-declarations

op-declaration ::= op op-name [ fixity ] : sort-scheme fixity ::= associativity priority associativity ::= infixl | infixr priority ::= nat-literal sort-scheme ::= [ sort-variable-binder ] sort sort-variable-binder ::= fa ( local-sort-variable-list )

Sample op-declarations:

op usage : String op o infixl 24 : fa(a,b,c) (b -> c) * (a -> b) -> a -> c

An op-declaration introduces an op-name with an associated sort. The sort can be "monomorphic", like String, or "polymorphic" (indicated by a sort-variable-binder). In the latter case, an indexed family of values is assigned to parameterized sort-names "indexed" by tuples of sorts, that is, there is one family member, a sorted value, for each possible assignment of sorts to the local-sort-variables of the sort-variable-binder, and the sort of that value is the result of the corresponding substitution of sorts for local-sort-variables on the polymorphic sort of the op. In the example above, the declaration of polymorphic o can be thought of as introducing a family of (fictitious) ops, one for each possible assignment to the local-sort-variables a, b and c:

oNat,String,Char : (String -> Char) * (Nat -> String) -> Nat -> Char oNat,Nat,Boolean : (Nat -> Boolean) * (Nat -> Nat) -> Nat -> Boolean oChar,Boolean,Nat : (Boolean -> Nat) * (Char -> Boolean) -> Char -> Nat

and so on. Any op-definition for o must be likewise accommodating.

Only binary ops (those having some sort S * T -> U) may be declared with a fixity. When declared with a fixity, the op-name may be used in infix notation, and then it is called an infix operator. For o above, this means that o(f, g) and f o g may be used, interchangeably, with no difference in meaning. If the associativity is infixl, the infix operator is called left-associative; otherwise, if the associativity is infixr, it is called right-associative. If the priority is priority N, the operator is said to have priority N. The nat-literal N stands for a natural number; if infix operator O1 has priority N1, and O2 has priority N2, with N1 < N2, we say that O1 has lower priority than O2, and that O2 has higher priority than (or takes priority over) O1. For the role of the associativity and priority, see further at Infix-applications.

Op-definitions

op-definition ::= def [ sort-variable-binder ] formal-expression [ : sort ] equals expression formal-expression ::= op-name | formal-application formal-application ::= formal-application-head formal-parameter formal-application-head ::= op-name | formal-application formal-parameter ::= closed-pattern

Sample op-definitions:

def usage = "Usage: Lookup key [database]" def fa(a,b,c) o(f : b -> c, g: a -> b) : a -> c = fn (x : a) -> f(g x) def o(f, g) x = f(g x)

Restriction. See the restriction under Op-declarations on redeclaring/redefining ops.

Note that a formal-expression always contains precisely one op-name, which is the op being defined by the op-definition. Note further that the formal-application of an op-definition always uses prefix notation, also for infix operators.

An op can be defined without having been declared. In that case the op-definition generates an implicit op-declaration for the op, as well as implicit sort-declarations for "place-holder" sorts needed for the op-declaration. For example, an undeclared op defined by

def f x y = (x, y x)

generates implicit declarations like:

sort s4771 sort s4772 op f : s4771 -> (s4771 -> s4772) -> (s4771 * s4772)

in which s4771 and s4772 are fresh names. Note that this is not polymorphic, but monomorphic with unspecified sorts. However, the further uses of f must uniquely determine sorts for the place-holders. In general, sorting information on ops may be omitted, but sufficient information must be supplied when used, so that all expressions can be assigned a sort in the context in which they occur while uniquely associating the ops with op-declarations or op-definitions. If two different associations both give sort-correct specs, the spec is ambiguous and incorrect.

As for op-definitions, the presence of a sort-variable-binder signals that the op being defined is polymorphic. Note that the optional sort annotation in an op-definition may not be a polymorphic sort-scheme, unlike for op-declarations. For example, the following is ungrammatical:

def o : fa(a,b,c) (b -> c) * (a -> b) -> a -> c = fn (f, g) -> fn (x) -> f(g x)

The presumably intended effect is achieved by

def fa(a,b,c) o : (b -> c) * (a -> b) -> a -> c = fn (f, g) -> fn (x) -> f(g x)

In a model of the spec, an indexed family of sorted values is assigned to a polymorphic op, with one family member for each possible assignment of sorts to the local-sort-variables of the sort-variable-binder, and the sort of that value is the result of the corresponding sort-instantiation for the polymorphic sort of the op. Thus, we can reduce the meaning of a polymorphic op-definition to a family of (fictitious) monomorphic op-definitions.

An op-definition with formal-prefix-application

def H P = E

in which H is a formal-application-head, P is a formal-parameter and E an expression, is equivalent to the op-definition

def H = fn P -> E

For example,

def o (f, g) x = f(g x)

is equivalent to

def o (f, g) = fn x -> f(g x)

which in turn is equivalent to

def o = fn (f, g) -> fn x -> f(g x)

By this deparameterizing transformation for each formal-parameter, an equivalent unparameterized op-definition is reached. The semantics is described in terms of such op-definitions.

In each model, the sorted value assigned to the op being defined must be the same as the value of the right-hand-side expression. For polymorphic op-definitions, this extends to all possible assignments of sorts to the local-sort-variables.

An op-definition can be thought of as a special notation for an axiom. For example,

def fa(a) double (x : a) = (x, x)

can be thought of as standing for:

op double : fa(a) a -> a * a axiom double_def is sort fa(a) fa(x : a) double x = (x, x)

In fact, Specware generates such axioms for use by provers. But in the case of recursive definitions, this form of axiomatization does not adequately capture the meaning. For example,

def f (n : Nat) : Nat = 0 * f n

is an improper definition, while

axiom f_def is fa(n : Nat) f n = 0 * f n

characterizes the function that maps every natural number to 0. The issue is the following. Values in models can not be undefined and functions assigned to ops must be total. But in assigning a meaning to a recursive op-definition, we -- temporarily -- allow undefined and partial functions (functions that are not everywhere defined on their domain sort) to be assigned to recursively defined ops. In the thus extended class of models, the recursive ops must be the least-defined solution to the "axiomatic" equation (the least fixpoint as in domain theory), given the assignment to the other ops. For the example of f above this results in the everywhere undefined function, since 0 times undefined is undefined. If the solution results in an undefined value or a function that is not total (or for higher-order functions, functions that may return non-total functions, and so on), the op-definition is improper. Specware 4.0 does not attempt to detect this condition or generate proof obligations for showing its absence.

Functions that are determined to be the value of an expression, but that are not assigned to ops, need not be total, but the context must enforce that the function can not be applied to values for which it is undefined. Otherwise, the spec is incorrect.

Claim-definitions

claim-definition ::= claim-kind claim-name equals claim claim-kind ::= axiom | theorem | conjecture claim-name ::= name claim ::= [ sort-quantification ] expression sort-quantification ::= sort sort-variable-binder

Sample claim-definitions:

axiom norm_idempotent is norm o norm = norm theorem o_assoc is sort fa(a,b,c,d) fa(f : c -> d, g : b -> c, h : a -> b) f o (g o h) = (f o g) o h conjecture pivot_hold is let p = pivot hold in fa (n : {n : Nat | n < p}) ~(hold n = hold p)

Restriction. The sort of the claim must be Boolean.

When a sort-quantification is present, the claim is polymorphic. The claim may be thought of as standing for an infinite family of monomorphic claims, one for each possible assignment of sorts to the local-sort-variables.

The claim-kind theorem should only be used for claims that have actually been proved to follow from the (explicit or implicit) axioms. In other words, giving them axiom status should not change the class of models. Theorems can be used by provers.

Conjectures are meant to represent proof obligations that should eventually attain theoremhood. Like theorems, they can be used by provers.

The Specware system passes on the claim-name of the claim-definition with the claim for purposes of identification. Both may be transformed to fit the requirements of the prover, and appear differently there. Not all claims can be faithfully represented in all provers, and even when they can, the logic of the prover may not be up to dealing with them.

Remark. It is a common mistake to omit the part "claim-name equals" from a claim-definition. A defensive style against this mistake is to have the claim always start on a new text line. This is additionally recommended because it may become required in future revisions of Metaslang.