Expressions
(The distinctions
tight- and
closed- for
expressions lack
semantic significance, and merely serve the purpose of avoiding
grammatical ambiguities.)
Sample expressions:
fn (s : String) -> s ^ "."
case z of {re = x, im = y} -> {re = x, im = ~y}
let x = x + 1 in f(x, x)
if x <= y then x else y
fa(x,y) (x <= y) <=> ((x < y) or (x = y))
f(x, x)
[] : List Arg
<=>
x
3260
z.re
("George", Poodle : Dog, 10)
{name = "George", kind = Poodle : Dog, age = 10}
(writeLine "key not found"; embed Missing)
["Sun", "Mon", "Tue", "Wed", "Thu", "Fri", "Sat"]
project 2
(n + 1) |
Restriction.
Like all polymorphic or sort-ambiguous constructs, an
expression
can only be used in a context if its sort can be inferred
uniquely, given the
expression and the context.
This restriction will not be repeated for the various kinds of
expressions defined in the following subsections.
The meaning of a parenthesized expression
(E) is the same
as that of the enclosed expression
E.
The various other kinds of expressions not defined here are described
each in their following respective sections, with the exception
of local-variable, whose
meaning as an expression is described below.
Restriction.
A local-variable may only be used as an expression if
it occurs in the scope of the local-variable-list of a
quantification or of a variable-pattern in which it is
introduced.
Disambiguation.
A single name used as an expression is a local-variable
when it occurs in the scope of a local-variable-list
or variable-pattern in which a synonymous local-variable
is introduced, and then it identifies the textually most recent
introduction.
Otherwise, the name is an op-name or an embedder; for the
disambiguation between the latter two, see Embedders.
A local-variable used as an expression has the sorted value
assigned to it in the environment.
Lambda-forms
Sample
lambda-form:
fn (s : String) -> s ^ "." |
The value of a
lambda-form is a partial or total function.
If the value determined for a
lambda-form as described
below is not a total function, the context must enforce
that the function can not be applied to values for which it
is undefined.
Otherwise, the
spec is incorrect.
Specware 4.0 does not attempt to generate proof obligations for
establishing this.
The sort of a lambda-form is that of its match.
The meaning of a given lambda-form of sort
S -> T is
the function f mapping each
inhabitant x of
S to a value
y of sort
T, where
y is the return value
of x for the match of the
lambda-form.
If the match accepts each x of
sort S (for acceptance and return
value, see the section on Matches) function
f is total; otherwise it is
partial, and undefined for those values
x rejected.
In case of a recursive definition, the above procedure may
fail to determine a value for y,
in which case function f is not
total, but undefined for x.
Case-expressions
Sample
case-expressions:
case z of {re = x, im = y} -> {re = x, im = ~y}
case s of
| Empty -> true
| Push {top = _, pop = rest} -> hasBottom? rest |
The value of a
case-expression
case E of M is the same as that of
the
application
(fn M)
(E).
Let-expressions
Sample
let-expressions:
let x = x + e in f(x, x)
let def f x = x + e in f (f x) |
In the case of a
recless-let-binding (recless =
recursion-less), the value of the
let-expression
let P = A in E is the same as that of the
application
(fn P -> E)
(A).
For the first example above, this amounts to
f(x + e, x + e).
Note that
x = x + e is not interpreted as a recursive
definition.
In case of a rec-let-binding-sequence (rec = recursive), the
rec-let-bindings have the role of "local"
op-definitions; that is, they are treated exactly like
op-definitions except that they are interpreted in the
local environment instead of the global model.
For the second example above, this amounts to
(x + e) + e.
(If e is a local-variable in this scope, the definition
of f can not be "promoted" to an
op-definition, which would be outside the scope binding
e.)
A spec with rec-let-bindings can be transformed into one
without such by creating op-definitions for each
rec-let-binding that take additional arguments, one for each of
the local-variables referenced. For the example, in which
f references local-variable e, the
op-definition for the "extended" op f+
would be def f+ e x = x + e, and the
let-expression would become f+ e (f+ e x).
The only difference in meaning is that the models of the
transformed spec assign a value to the newly introduced
op-name f+.
Note that the first occurrence of x in the above example
of a rec-let-binding is a variable-pattern and the
second-occurrence is in its scope; the third and last occurrence of
x, however, is outside the scope of the first x and
identifies an op or local-variable x introduced
elsewhere.
So, without change in meaning, the rec-let-binding can be
changed to:
let def f xena = xena + e in f (f x) |
Applications
Sample
applications:
Disambiguation.
The grammar for
application is ambiguous for cases
like
P N Q, in which
P and
Q are
closed-expressions, and
N is the
name of an infix operator.
The ambiguity is resolved in favor of the reading
as an
infix-application, and then the
infix-application P N Q
is equivalent to the
prefix-application
N (P, Q).
For example, in the second example
application
f x (g y) given above,
if
x is an infix operator,
the
application is an
infix-application
equivalent to
prefix-application x (f, g y).
If
x is not defined as an infix operator, or is a
local-variable in scope, the
application is the same as
the unconditionally unambiguous version
(f x) (g y).
Note that the resolution of the ambiguity does not rely on
information about the sorts. Even if
(f x) (g y) is sort-correct and
x (f, g y) is not, the latter interpretation is chosen
for disambiguating
f x (g y)
whenever
x is an infix operator in the context, and
consequently
f x (g y) is then also sort-incorrect.
Disambiguation.
An infix-application
P M Q N R, in which
P,
Q and
R are actual-parameters and
M and
N are infix operators,
is interpreted as either
(P M Q) N
R or
P M (Q N
R).
The choice is made as follows.
If M has higher priority than
N, or the priorities are the same
but M is left-associative,
the interpretation is
(P M Q) N
R.
In all other cases
the interpretation is
P M (Q N
R).
For example, given
op @ infixl 10: Nat * Nat -> Nat
op $ infixr 20: Nat * Nat -> Nat |
the following interpretations hold:
1 $ 2 @ 3 = (1 $ 2) @ 3
1 @ 2 @ 3 = (1 @ 2) @ 3
1 @ 2 $ 3 = 1 @ (2 $ 3)
1 $ 2 $ 3 = 1 $ (2 $ 3) |
Note that no sort information is used in the disambiguation.
If
(1 @ 2) $ 3 is sort-correct but
1 @ (2 $ 3) is
not, the formula
1 @ 2 $ 3 is sort-incorrect, since its
interpretation is.
Restriction.
In an application H
P, in which
H is an application-head
and P an actual-parameter,
the sort of P
must be some function sort
S -> T, and then
H must have the domain sort
S.
The sort of the whole application is then
T.
The value of
application H
P is the value returned by
function H for the argument
value P.
(Since infix-applications may always be rewritten
equivalently as
prefix-applications, only the semantics for
prefix-applications is given explicitly.)
Annotated-expressions
Restriction.
In an
annotated-expression
E : S, the
expression
E must have sort
S.
Sample annotated-expression:
[] : List Arg
Positive : Sign |
The value of an
annotated-expression
E : S is the value of
E.
The sort of some expressions is polymorphic. For example,
for any sort T,
[] denotes the empty list of sort List T.
Likewise, constructors of parameterized sum sorts can be
polymorphic, as the constructor None of
sort Option a = | Some a | None |
Further, overloaded
constructors have an ambiguous sort.
By annotating such polymorphic or sort-ambiguous
expressions with a
sort, their sort can
be disambiguated, which is required unless an
unambiguous sort can already be inferred from the context.
Annotation, even when redundant, can further help to
increase clarity.
Op-names
Sample
op-names:
length
>=
DB_LOOKUP.Lookup |
Restriction.
An
op-name may only be used if there is an
op-declaration
and/or
op-definition for it in the current
spec or in some
spec that is imported (directly or indirectly) in the current
spec.
If there is a unique
qualified-name for a given unqualified
ending that is sort-correct in the context, the qualification
may be omitted for an
op-name used as an
expression.
So overloaded
ops may only be used as such when their sort can
be disambiguated in the context.
The value of an op-name is the value assigned to
it in the model.
(In this case, the context can not have superseded the
original assignment.)
Literals
Sample
literals:
true
3260
#z
"On/Off switch" |
Restriction:
No whitespace is allowed anywhere inside any kind of
literal,
except for
"significant" whitespace in
string-literals, as explained there.
Literals provide denotations for the inhabitants of the
"built-in" sorts Boolean, Nat, Char
and String.
The value of a literal is independent of the environment.
(There are no literals for the built-in sort Integer.
For nonnegative integers, a nat-literal can be used.
For negative integers, apply the built-in op ~, which
negates an integer, or use the built-in infix operator
-: both ~1 and 0 - 1 denote the negative integer
-1.)
Boolean-literals
boolean-literal ::= true | false
|
Sample
boolean-literals:
The sort
Boolean has precisely two inhabitants,
the values of
true and
false.
Note that true and false are not constructors.
So embed true is ungrammatical.
Nat-literals
Sample
nat-literals:
The
sort Nat is, by definition, the subsort of
Integer restricted to the nonnegative integers 0, 1, 2,
... , which we identify with the natural numbers.
The value of a
nat-literal is the natural number of which
it is a decimal representation; for example, the
nat-literal 3260 denotes the natural number 3260.
Leading
decimal-digits 0 have no significance:
both
007 and
7 denote the number 7.
Char-literals
Sample char-literals:
The sort
Char is inhabited by the 256
8-bit
characters
occupying decimal positions 0 through 255 (hexadecimal
positions 00 through FF) in the ISO 8859-1 code table.
The first 128 characters of that code table are the
traditional ASCII characters (ISO 646).
(Depending on the operating environment, in particular the
second set of 128 characters -- those with
"the high bit set" -- may print or otherwise
be visually presented differently than intended by the
ISO 8859-1 code.)
The value of a
char-literal is a character of sort
Char.
The value of a char-literal #G, where
G is a char-glyph, is the character denoted by
G.
For example, #z is the character that prints as
z.
The two-mark char-literal #" provides a variant notation of the
three-mark char-literal #\" and yields the
character " (decimal position 34).
Each one-mark char-glyph
C denotes the character that
"prints" as C.
The two-mark char-glyph \\ denotes
the character \ (decimal position 92),
and the two-mark char-glyph \" denotes
the character " (decimal position 34).
Notations are provided for denoting eight
"non-printing" characters, which, with the
exception of the first, are meant to regulate lay-out in
printing;
the actual effect may depend on the operating environment:
Finally, every character can be obtained using the
hexadecimal representation of its position.
The four-mark
char-glyph
\xH1H0
denotes the character with hexadecimal position
H1H0,
which is decimal position
16 times the decimal value of
hexadecimal-digit
H1 plus
the decimal value of
hexadecimal-digit
H0,
where the decimal value of the digits
0 through
9 is
conventional, while the six extra digits
A through
F
correspond to 10 through 15.
The case (lower or upper) of the six extra
digits is not significant.
For example,
\x7A or equivalently
\x7a has decimal
position 16 times 7 plus 10 = 122, and either version denotes
the character
z.
The
"null" character can be obtained by using
\x00.
String-literals
The presentation of a
significant-whitespace is the
whitespace suggested by the name (
space,
tab or
newline).
Sample string-literals:
""
"see page"
"see\spage"
"the symbol ' is a single quote"
"the symbol \" is a double quote" |
The sort
String is inhabited by the
strings, which are (possibly empty)
sequences of characters.
The sort
String is primitive; it is a different sort
than the isomorphic sort
List Char, and the list operations
can not be directly applied to strings.
The value of a string-literal is the sequence of characters
denoted by the string-literal-glyphs comprising its
string-body, where
the value of a significant-whitespace is the
whitespace character suggested by the name (space,
horizontal tab or newline).
For example, the string-literal "seepage" is different
from "see page"; the latter denotes an eight-character
string of which the fourth character is a space.
The space can be made explicit by using the char-glyph
\s.
When a double-quote character " is needed in a string, it
must be escaped, as in "[6'2\"]", which would print like
this: [6'2"].
Tuple-displays
Sample
tuple-display:
("George", Poodle : Dog, 10) |
Note that a
tuple-display-body contains either no
expressions, or else at least two.
The value of a tuple-display whose tuple-display-body is
not empty, is the tuple whose
components are the respective values of the expressions of
the tuple-display-body, taken in textual order.
The sort of that tuple is the "product" of the
corresponding sorts of the components.
The value of () is the empty tuple, which is the sole
inhabitant of the unit sort ().
(The fact that the notation () does double duty, for
a sort and as an expression, creates no ambiguity.
Note also that -- unlike the empty list-display [] --
the expression () is monomorphic, so
there is no need to ever annotate it with a sort.)
Record-displays
Sample
record-display:
{name = "George", kind = Poodle : Dog, age = 10} |
The value of a
record-display is the record whose
components are the respective values of the
expressions of
the
record-display-body, taken in the lexicographic order
of the
field-names, as discussed under
Sort-records.
The sort of that record is the record sort with the same set
of
field-names, where the sort for each
field-name
F is the sort of
the corresponding sort of the component selected by
F in the record.
The value of
{} is the empty tuple, which is the sole
inhabitant of the unit sort
().
(For
expressions as well as for
sorts, the notations
{} and
() are fully interchangeable.)
Sequential-expressions
Sample
sequential-expression:
(writeLine "key not found"; embed Missing) |
A
sequential-expression
(V; T) is equivalent to the
let-expression let _ = V in (T).
So the value of a
sequential-expression
(V1;
...
; Vn; E)
is the value of its
last constituent
expression E.
Sequential-expressions can be used to achieve
non-functional "side effects", effectuated by
the elaboration of the void-expressions, in particular
the output of a message.
This is useful for tracing the execution of generated code.
The equivalent effect of the example above can be achieved
by a let-binding:
let _ = writeLine "key not found" in
embed Missing |
(If the intent is to temporarily add, and later remove or
disable the tracing output, this is probably a more convenient
style, as the modifications needed concern a single full text line.)
Any values resulting from elaborating the
void-expressions are
discarded.
List-displays
Sample
list-display:
["Sun", "Mon", "Tue", "Wed", "Thu", "Fri", "Sat"] |
Restriction.
All
expressions of the
list-display-body must have the
same sort.
Note that a list-display [] with empty
list-display-body is polymorphic, and may need to be
sort-disambiguated, for example with a sort annotation.
In a case like [[], [1]], there is no need to
disambiguate [], since the above restriction already
implies that [] here has the same sort as [1],
which has sort List Nat.
The parameterized sort List, although built-in, is
actually not primitive, but defined by:
sort List a =
| Nil
| Cons a * List a |
The empty
list-display [] denotes the same list as the
expression Nil, a singleton
list-display
[E] denotes the same
list as the
expression Cons
(E, Nil), and a
multi-element
list-display
[E1, E2,
...
, En]
denotes the same list as the
expression Cons
(E1,
[E2,
...
, En]).
Structors
The
structors are a medley of constructs, all having polymorphic
or sort-ambiguous function sorts and denoting special functions
that go between structurally related sorts, such as
the constructors of sum sorts and the destructors of product sorts.
Restriction.
Like all polymorphic or sort-ambiguous constructs, a structor
can only be used in a context where its sort can be inferred
uniquely.
This restriction will not be repeated for the various kinds
of structors described in the following subsections.
For example, the following correct spec becomes incorrect when
any of the sort annotations is omitted:
spec
def fa(a) p2 = project 2 : String * a -> a
def q2 = project 2 : String * Nat -> Nat
endspec |
Projectors
Sample
projectors:
When the
field-selector is some
nat-literal with value
i, it is required that
i be at least 1.
The sort of the
projector is a function sort (whose domain sort is a product
sort) of the form
S1 * S2 * ...
* Sn -> Si,
where
n is at least
i,
and the value of the
projector is the function that maps
each
n-tuple
(
v1,
v2, ... ,
vn)
inhabiting the domain sort
to its
ith component
vi.
When the field-selector is some field-name
F,
the sort of the
projector is a function sort (whose domain sort is a record
sort) of the form
{F1
: S1, F2
: S2,
...
, Fn : Sn}
-> Si,
where F is the same field-name
as
Fi
for some natural number i in the
range 1 through n.
Assuming that the fields are lexicographically ordered by
field-name (see under Sort-records),
the value of the projector is the function that maps
each
n-tuple
(v1,
v2, ... ,
vn)
inhabiting the domain sort
to its ith component
vi.
Relaxators
Sample
relaxator:
Restriction.
The
closed-expression of a
relaxator must have some function
sort
S -> Boolean.
The sort of relaxator relax P,
where P has sort
S -> Boolean, is the function
sort (whose domain is a subsort) (S | P) -> S.
The value of the relaxator is the function that maps each
inhabitant of subsort
(S | P) to the same value --
apart from the sort information -- inhabiting supersort
S.
For example, given
we have the sorting
for the function that injects the even natural numbers back
into the supersort of
Even.
Metaslang does not require the explicit use of a relaxator to relax
an expression from a subsort to its supersort if the
context requires the latter.
Implicit relaxation will take place when needed.
For example, in the expression ~1 the nat-literal 1
of sort Nat is implicitly relaxed to sort Integer to
accommodate the unary negation operator ~, which has sort
Integer -> Integer.
Note the remarks about equivalence of sort-restrictions in
the corresponding section.
Restrictors
Sample
restrictor:
Restriction.
The
closed-expression of a
restrictor must have some function
sort
S -> Boolean.
A restrictor
restrict P is a convenient
notation for the lambda-form
fn X ->
let relax P V = X in V, where
V is some unique fresh name, that
is, it is any name that does not already occur in the
spec, directly or indirectly through an import.
The sort of a restrictor is of the form
S ->
(S | P), that is, it goes from a
supersort to a subsort.
In general its value is a partial function, defined only on
the range of the function relax P.
The use of this partial function engenders a proof obligation
that the arguments to which it is applied satisfy predicate
P.
For example, the restrictor
restrict (fn (n : Integer) -> n >= 0) has sort
Integer -> Nat; its domain of definedness are the
nonnegative integers (of sort Integer).
Used in the following expression, which has
sort Nat assuming that i has sort Integer,
if i < 0
then 0
else restrict (fn (n : Integer) -> n >= 0) i |
the context guarantees that integer
i, where it is subjected
to the
restrictor, satisfies the nonnegativity
restriction on natural numbers, and will be accepted and
achieve
Nat-hood.
Formally, the proof obligation here is
~(i < 0) => (i >= 0).
This is a theorem from the Theory of Integers.
Metaslang does not require the explicit use of a restrictor
to restrict
an expression from a sort to a subsort if the
context requires the latter.
Implicit restriction will take place when needed.
For example, in the expression 7 div 2 the nat-literal 2
of sort Nat is implicitly restricted to sort PosNat,
a subsort of Nat, to accommodate the division operator
div, whose second argument has sort PosNat.
But note that implicit restriction engenders the same proof
obligation as results when using an explicit restrictor.
Quotienters
Sample
quotienter:
quotient (fn (m, n) -> m rem 3 = n rem 3) |
Restriction.
The
closed-expression of a
quotienter must have some sort
S * S -> Boolean;
in addition, it must be an equivalence relation, as explained
under
Sort-quotients.
The sort of quotienter quotient Q,
where Q has sort
S * S -> Boolean, is the function sort
S -> S / Q, that is, it goes from some
sort to one of its quotient sorts.
The value of the quotienter is the function that maps each
inhabitant of sort S to the
Q-equivalence class inhabiting S /
Q of which it is a member.
For example, given
def congMod3 : Nat * Nat -> Boolean =
(fn (m, n) -> m rem 3 = n rem 3)
sort Z3 = Nat / congMod3 |
we have the sorting
quotient congMod3 : Nat -> Z3 |
and the function maps, for example, the number 5 to the
equivalence class {2, 5, 8, ...}, which is one of the three
inhabitants of
Z3.
Choosers
Sample
chooser:
Restriction.
The
closed-expression of a
chooser must have some sort
S * S -> Boolean, and
must be an equivalence relation (see under
Sort-quotients).
The sort of a chooser choose Q,
where Q has sort
S * S -> Boolean, is a function sort of the form
(S -> T) ->
(S / Q -> T).
The value of the chooser is the (in general partial)
function mapping each Q-constant
(explained below) function f inhabiting sort
S -> T to the function that maps
each inhabitant C of
S / Q to f
x, where
x is any member of
C.
Expressed symbolically, using a pseudo-function any that
arbitrarily picks any member from a nonempty set, this is
the function
fn f -> fn C -> f (any C) |
The requirement of
Q-constancy
is precisely what is needed to make this function insensitive
to the choice made by
any.
Function f is
Q-constant if,
for each Q-equivalence class
C inhabiting
S / Q,
f x
equals f
y for any two values
x and
y that are members of
C,
or f is undefined on all members of
C.
(Since the result of f is
constant across each equivalence class, it does not matter
which of its elements is selected by any.)
For example -- continuing the example of the previous section --
function fn n -> n*n rem 3 is congMod3-constant;
for the equivalence class {2, 5, 8, ...}, for example, it
maps each member to the same value 1.
So choose congMod3 (fn n -> n*n rem 3) maps the inhabitant
{2, 5, 8, ...} of sort Z3 to the natural number 1.
The most discriminating
Q-constant function is
quotient Q, and
choose Q quotient Q is the identity function on the
quotient sort for Q.
The meaning of choose Q (fn x -> E) A
is the same as that of the let-expression
let quotient Q x = A in E.
Indeed, often a quotient-pattern offers a more convenient
way of expressing the intention of a chooser.
Note, however, the remarks on the proof obligations for
quotient-patterns.
Embedders
Sample
embedders:
Nil
embed Nil
Cons
embed Cons |
Disambiguation.
If an
expression consists of a single
name, which, in the
context, is both the
name of a
constructor and the
name
of an
op or a
local-variable in scope, then it is
interpreted as the latter of the various possibilities.
For example, in the context of
sort Answer = | yes | no
def yes = no : Answer
def which (a : Answer) = case a of
| yes -> "Yes!"
| no -> "Oh, no!" |
the value of
which yes is
"Oh, no!", since
yes
here is disambiguated as identifying the
op yes, which
has value
no.
The interpretation as
embedder is forced by using
the
embed keyword:
the value of
which embed yes is
"Yes!".
By using
names that begin with a capital
letter for
constructors, and
names that do not begin with a capital
letter for
ops and
local-variables, the risk of an accidental wrong
interpretation can be avoided.
The semantics of embedders is described in the section on
Sort-sums.
The presence or absence of the keyword embed is not
significant for the meaning of the construct (although it
may be required for grammatical disambiguation, as described
above).
Embedding-tests
Sample
embedding-test:
Restriction.
The sort of an
embedding-test embed? C must be of the form
SS -> Boolean, where
SS is a sum sort that has a
constructor C.
The value of embedding-test embed? C is the predicate that returns
true if the argument value -- which, as inhabitant of a
sum sort, is tagged -- has tag C,
and otherwise false.
The embedding-test can be equivalently rewritten as
fn
| C _ -> true
| _ -> false |
where the wildcard
_ in the first
branch is omitted when
C is parameter-less.
In plain words, embed? C
tests whether its sum-sorted argument has been constructed with the
constructor C.
It is an error when C is not a
constructor of the sum sort.