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 types, ops and claims are left) is inserted in place in the receiving spec.

For example, the result of

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

is this "expanded" spec:

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

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

There are a few restrictions, which are meant to catch unintentional naming mistakes. First, if two different imported specs each introduce a type 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 : Integer 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 result in an ill-formed spec. This restriction is in fact a special case of the general requirement that import expansion must result in a well-formed spec. Secondly, a type-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 well-formed spec.

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

import-declaration ::= import spec-term

Sample import-declaration:

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 simple-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 type-names or op-names, it can be denoted by morphism A -> B {}.

Type-declarations

type-declaration ::= type type-name [ formal-type-parameters ] [ equals old-or-new-type-descriptor ] formal-type-parameters ::= local-type-variable | ( local-type-variable-list ) local-type-variable ::= simple-name local-type-variable-list ::= local-type-variable { , local-type-variable }* old-or-new-type-descriptor ::= type-descriptor | new-type-descriptor

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

Sample type-declarations:

type Date type Array a type Array a = List a type Map(a, b)

A type-declaration of the form type T = D is equivalent to the type-declaration type T followed by the type-definition def type T = D.

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

Restriction. Except for the exception provided in the next paragraph, type-names may not be redeclared and/or redefined, whether in the same spec or after having been defined in an imported spec, not even when both declarations or definitions are identical.

In Specware 4.2, a type may be declared in a type-declaration not containing a defining part (introduced by an equals), and in the same context also be defined in a type-declaration containing a defining part. This is now a deprecated feature that may not persist in future releases. Users are advised to either use a type-declaration not containing a defining part followed by a type-definition, or to combine the two in one type-declaration containing a defining part.

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

Type-definitions

type-definition ::= type-abbreviation | new-type-definition type-abbreviation ::= def [ type ] type-name [ formal-type-parameters ] equals type-descriptor new-type-definition ::= def [ type ] type-name [ formal-type-parameters ] equals new-type-descriptor

Sample type-abbreviations:

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

Sample new-type-definitions:

def Tree a = | Leaf a | Fork (Tree a * Tree a) def {Bush,Shrub} a = | Leaf a | Fork (Tree a * Tree a) def type Z3 = Nat / (fn (m, n) -> m rem 3 = n rem 3)

The keyword type may be omitted after def unless the name following the keyword type is declared or defined in the context as an op-name.

Restriction. The type-name of a type-definition must have been previously declared in a type-declaration, and either the declaration and definition both must contain no formal-type-parameters, or agree in the number of local-type-variables in their formal-type-parameters.

In each model, the type assigned to the type-name of a type-abbreviation must be the same as the right-hand-side type-descriptor, while that assigned to the type-name of a new-type-definition must be isomorphic to the type of the new-type-descriptor. Thus, while Array Nat and List Nat from the examples denote the same type, the types assigned to Tree Nat and Bush Nat are equivalent but not necessarily equal, and commingling them in a spec results in a type error. On the other hand, Bush Nat and Shrub Nat are truly synonymous.

For parameterized types, this extends to all possible assignments of types to the local-type-variables, taking the right-hand type-descriptors and new-type-descriptors as interpreted under each of these assignments. So, for the example, Map(Nat, Char) is the same type as (Array (Nat * Char) | key_uniq?), and so on.

With recursive type-definitions, there are additional requirements. Consider

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

This means that for each type a there is a value Empty of type Stack a, and further a function Push that maps values of type {top : a, pop : Stack a} to Stack a. Furthermore, the type 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 type 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 [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, type-definitions generate implicit axioms, which for recursive definitions imply that the type is not "larger" than necessary. In technical terms, in each model the type is the least fixpoint of a recursive domain equation.

Op-declarations

op-declaration ::= op [ type-variable-binder ] formal-expression [ fixity ] type-annotation [ equals expression ] | op formal-expression [ fixity ] polytype-annotation [ equals expression ] polytype-annotation ::= : type-variable-binder type-descriptor type-variable-binder ::= [ local-type-variable-list ] formal-expression ::= op-name | formal-application formal-application ::= formal-application-head formal-parameter formal-application-head ::= op-name | formal-application formal-parameter ::= closed-pattern | ( pattern | expression ) fixity ::= associativity priority associativity ::= infixl | infixr priority ::= nat-literal

Note that the formal-expression of an op-declaration always uses prefix notation, even for infix-operators.

Sample op-declarations:

op usage : String op usage : String = "Usage: Lookup key [database]" op [a,b,c] o infixl 24 : (b -> c) * (a -> b) -> a -> c op o infixl 24 : [a,b,c] (b -> c) * (a -> b) -> a -> c op f (s : String) ((i, j) : Nat * Nat | i < j) (c : Char) : String = substring (s, i, j) ^ toString c

The placement of a type-variable-binder, if present, is of no significance; the two declarations given above for op o are completely equivalent. Note that the presence of a type-annotation or polytype-annotation is mandatory even if the type can be determined from a defining expression, as in the second example for op usage above.

The meaning of a formal-parameter (P|E) is the same as that of the formal-parameter ((P):{(P):T|E}), in which T is a type-descriptor such that in the context the annotated-pattern (P):T is type-correct. If no such type-descriptor exists, or its type cannot be unambiguously be determined, the formal-parameter is type-incorrect. For example, in the declaration for f above, the formal-parameter ((i, j) : Nat * Nat | i < j) is a shorthand notation for (((i, j) : Nat * Nat) : {(((i, j) : Nat * Nat) : Nat * Nat | i < j)}), which can be simplified to ((i, j) : {((i, j) : Nat * Nat | i < j)}).

Restriction. The restricting expression following a vertical bar in a formal-parameter must not refer to local variables introduced by preceding formal-parameters. (To do so would effectively create dependent types, which are currently not supported.)

An op-declaration of the form op B F X A = E, in which B is an optional type-variable-binder, F is a formal-expression, X is an optional fixity, A is a type-annotation and E is an expression, is equivalent to the op-declaration op B F X A followed by the op-definition def op B F = E.

In an op-declaration of the form op N : T, in which N is an op-name, N is declared to have type T. An op-declaration of the form op H (P:S) : T, in which P is a pattern whose type is given by type-descriptor T, is equivalent to op H : S -> T. So the simple-names used as local-variables in each formal-parameter are only bound to that formal-parameter, and are further irrelevant for its type. For example, the op-declaration of f above is equivalent to the following:

op f : String -> {(i, j) : Nat * Nat | i < j} -> Char -> String def f s (i, j) c = substring (s, i, j) ^ toString c

in which the type-annotations in the op-definition have been omitted as being redundant.

Restriction. User-defined ops may not be "overloaded", or otherwise be redeclared and/or redefined, whether in the same spec or after having been defined in an imported spec, not even when both declarations or definitions are identical.

However, one can get the effect of overloading by declaring distinct ops with different qualifiers for the same unqualified name, e.g.

op Table.length : Table -> Nat op Vector.length : Vector -> Nat

Here, subsequent references of the form length may be resolved to refer to Table.length or Vector.length as appropriate, provided exactly one is type-consistent in the context of the reference.

An op-declaration introduces an op with an associated type. The type can be "monomorphic", like String, or "polymorphic" (indicated by a type-variable-binder). In the latter case, an indexed family of values is assigned to parameterized type-names "indexed" by tuples of types, that is, there is one family member, a typed value, for each possible assignment of types to the local-type-variables of the type-variable-binder, and the type of that value is the result of the corresponding substitution of types for local-type-variables on the polymorphic type of the op. In the examples above, the two forms given for the declaration of polymorphic o are entirely equivalent; they can be thought of as introducing a family of (fictitious) ops, one for each possible assignment to the local-type-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 type S * T -> U) may be declared with a fixity. When declared with a fixity, the op 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 [ op ] [ type-variable-binder ] formal-expression [ type-annotation ] equals expression | def [ op ] formal-expression polytype-annotation equals expression

Sample op-definitions:

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

The keyword op may be omitted after def unless the part between the keyword def and the equals has the syntactic form of a name N followed by an optional formal-type-parameters, where the name N is declared or defined in the context as a type-name. As for op-declarations, the placement of any type-variable-binder is of no significance.

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-expression of an op-definition always uses prefix notation, even for infix-operators.

Restriction. The type information, if any, presented in an op-definition must be consistent with the type specified by the preceding op-declaration. For example, the presence of a type-variable-binder signals that the op being defined is polymorphic, but then the op-declaration must contain an identical type-variable-binder. (A type-variable-binder may be needed to introduce local-type-variables for employ in type-annotations within the defining expression, as exemplified in the first definition for o.)

In Specware 4.2, an op still may be defined without having been previously declared, but this is now a deprecated feature. When an op is defined without having been declared, the op-definition generates an implicit op-declaration for the op, provided a monomorphic type for the op can be unambiguously determined from the op-definition together with the uses of the op in applications and other contexts, so that all expressions can be assigned a type in the context in which they occur. This feature may not persist in future releases, so users are advised to provide an op-declaration somewhere before each op-definition, either in the same spec or (more typically) in an imported spec. Alternatively, the newly expanded syntax for op-definitions makes it simple to both give a unique type to and define an op within one declaration.

In a model of the spec, an indexed family of typed values is assigned to a polymorphic op, with one family member for each possible assignment of types to the local-type-variables of the type-variable-binder, and the type of that value is the result of the corresponding type-instantiation for the polymorphic type 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-application

def op 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 op 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 typed 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 types to the local-type-variables.

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

op double : [a] a -> a * a def double x = (x, x)

can be thought of as standing for:

op double : [a] a -> a * a axiom double_def is [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 type) 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. Although Specware 4.2 does attempt to generate proof obligations for this condition, it currently covers only "simple" recursion, and not mutual recursion or recursion introduced by means of higher-order functions.

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 ill formed.

Claim-declarations

claim-declaration ::= claim-kind claim-name is claim [ proof-script ] claim-kind ::= axiom | theorem | conjecture claim-name ::= name claim ::= [ type-variable-binder ] expression

Sample claim-declarations:

axiom norm_idempotent is norm o norm = norm theorem o_assoc is [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)

Proof-scripts are currently only available for use with Isabelle, and are not described here. For further details, see the Specware to Isabelle Translator Manual.

Restriction. The type of the claim must be Boolean.

Restriction. A claim must not be an expression whose first symbol is [. In order to use such an expression as a claim, it can be parenthesized, as in

axiom nil_fits_nil is ([] fits [])

This restriction prevents ambiguities between claims with and without type-variable-binders.

When a type-variable-binder is present, the claim is polymorphic. A polymorphic claim may be thought of as standing for an infinite family of monomorphic claims, one for each possible assignment of types to the local-type-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. This is only sound if circularities (vicious circles) are avoided. This kind of claim is usually created automatically by the elaboration of an obligator, but can also be created manually.

The Specware system passes on the claim-name of the claim-declaration 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 is" from a claim-declaration. 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.