Declarations
Sample
declarations:
import Lookup
type Key
op present : Database * Key -> Boolean
type Key = String
def present(db, k) = embed? Some (lookup (db, k))
axiom norm_idempotent is fa(x) norm (norm x) = norm x |
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
type A.Z = String
def b = toString
endspec |
is this
"expanded" spec:
spec
type A.Z
op b : Nat -> A.Z
type 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.
Sample
import-declarations
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- or op-names,
it can be denoted by morphism A
-> B {}.
Type-declarations
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 Map(a, b) |
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).
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).
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
Sample
type-definitions:
type Date = {year : Nat, month : Nat, day : Nat}
type Array a = List a
type Map(a, b) = (Array (a * b) | key_uniq?) |
In each model, the type assigned to the
type-name must be the same as the right-hand-side
type-descriptor.
For parameterized types, this extends to all possible
assignments
of types to the
local-type-variables, taking the right-hand
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.
For example, consider
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
Sample
op-declarations:
op usage : String
op o infixl 24 : [a,b,c] (b -> c) * (a -> b) -> a -> c |
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 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-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
Sample
op-definitions:
def 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(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, 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.
In general, typing information on ops may be omitted, but sufficient
information must be supplied when used, so that all
expressions can be assigned a type in the context in which
they occur while uniquely associating the ops with
op-declarations or op-definitions.
If two different associations both give type-correct specs,
the spec is ambiguous and ill formed.
As for op-definitions, the presence of a type-variable-binder
signals that the op being defined is polymorphic.
Note that the optional type annotation in an op-definition
can not be a polymorphic type-scheme, unlike for
op-declarations. For example, the following is ungrammatical:
def o : [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 [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 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-prefix-application
in which
H is a
formal-application-head,
P is a
formal-parameter and
E an
expression,
is equivalent to the
op-definition
For example,
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,
def [a] double (x : a) = (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.1 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-definitions
Sample
claim-definitions:
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) |
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.
then it identifies the textually most recent introduction.
Otherwise, the
simple-name is a
type-name.
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-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
is" 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.