A "unit" is an identifiable unit-term, where "identifiable" means that the unit-term can be referred to by a unit-identifier. Unit-terms can be "elaborated", resulting in specs, morphisms, diagrams or other entities. The effect of elaborating a unit-definition is that its unit-term is elaborated and becomes associated with its unit-identifier.
For the elaboration of a unit-term to be meaningful, it has to be well formed and result in a well-formed -- and therefore type-correct -- entity. Well-formedness is a stricter requirement than type-correctness. If a unit-term or one of its constituent parts does not meet any of the restrictions stated in this language manual, it is ill formed. This holds throughout, also if it is not mentioned explicitly for some syntactic construct. Well-formedness is more than a syntactic property; in general, to establish well-formedness it may be necessary to "discharge" (prove) proof obligations engendered by the unit-term.
A Specware project consists of a collection of Metaslang unit-definitions. They can be recorded in one or more Specware files. There are basically two styles for recording unit-definitions using Specware files. In the single-unit style, the file, when processed by Specware, contributes a single unit-definition to the project. In the multiple-unit style, the file may contribute several unit-definitions. The two styles may be freely mixed in a project (but not in the same Specware file). This is explained in more detail in what follows.
unit-definition ::= unit-identifier = unit-term unit-term ::= spec-term | morphism-term | diagram-term | target-code-term | proof-term specware-file-contents ::= unit-term | infile-unit-definition { infile-unit-definition }* infile-unit-definition ::= fragment-identifier = unit-term fragment-identifier ::= word-symbol |
Unit-definitions may use other unit-definitions, including standard libraries, which in Specware 4.1 are supposed to be part of each project. However, the dependencies between units must not form a cycle; it must always be possible to arrange the unit-definitions in an order in which later unit-definitions only depend on earlier ones. How unit-definitions are processed by Specware is further dealt with in the Specware User Manual.
As mentioned above, unit-definitions are collected in Specware files, which in Specware 4.1 must have an .sw extension. The Specware files do not directly contain the unit-definitions that form the project. In fact, a user never writes unit-definition explicitly. These are instead determined from the contents of the Specware files using the following rules. There are two possibilities here. The first is that the specware-file-contents consists of a single unit-term. If P.sw is the path for the Specware file, the unit being defined has as its unit-identifier P. For example, if file C:/units/Layout/Fixture.sw contains a single unit-term U, the unit-identifier is /units/Layout/Fixture, and the unit-definition it contributes to the project is
/units/Layout/Fixture = U |
The second possibility is that the Specware file contains one or more infile-unit-definitions. If I is the fragment-identifier of such an infile-unit-definition, and P.sw is the path for the Specware file, the unit being defined has as its unit-identifier P#I. For example, if file C:/units/Layout/Cart.sw contains an infile-unit-definition Pos = U, the unit-identifier is /units/Layout/Cart#Pos, and the unit-definition it contributes to the project is
/units/Layout/Cart#Pos = U |
unit-identifier ::= swpath-based-path | relative-path swpath-based-path ::= / relative-path relative-path ::= { path-element / }* path-element [ # fragment-identifier ] path-element ::= word-symbol |
Warning. Recall that whitespace is not allowed within unit-identifiers. Note that unit-identifiers are processed by the tokenizer like everything else. This means that marks not allowed in word-symbols, even if otherwise permitted in filenames (such as -), cannot appear in unit-identifiers. For this reason, some care must be taken when naming units.
Unit-identifiers are used to identify unit-terms. Typically, only a final part of the full unit-identifier is used. When Specware is started with environment variable SWPATH set to a semicolon-separated list of pathnames for directories, the Specware files are searched for relative to these pathnames; for example, if SWPATH is set to C:/units/Layout;C:/units/Layout/Cart, then C:/units/Layout/Fixture.sw may be shortened to /Fixture, and C:/units/Layout/Cart.sw to /Cart. How unit-definitions are processed by Specware is further dealt with in the Specware User Manual.
Further, unit-identifiers can be relative to the directory containing the Specware file in which they occur. So, for example, both in file C:/units/Layout/Fixture.sw and in file C:/units/Layout/Cart.sw, unit-identifier Tools/Pivot refers to the unit-term contained in file C:/units/Layout/Tools/Pivot.sw, while Props#SDF refers to the unit-term of infile-unit-definition SDF = ... contained in file C:/units/Layout/Props.sw. As a special case, a unit-term with the same name as the file may be referenced without a fragment-identifier. For example, in the current case, if the file C:/units/Layout/Props.sw contains the unit-term of infile-unit-definition Props = ..., then this unit-term can be referred to either by Props#Props or Props.
The unit-identifier must identify a unit-definition as described above; the elaboration of the unit-identifier is then the result of elaborating the corresponding unit-term, yielding a spec, morphism, diagram, or other entity.
spec-term ::= unit-identifier | spec-form | spec-qualification | spec-translation | spec-substitution | diagram-colimit | obligator |
The elaboration of a spec-term, if defined, yields an "expanded" spec-form as defined in the next subsection.
spec-form ::= spec { declaration }* endspec |
Sample spec-forms:
spec import Measures import Valuta endspec |
An expanded spec-form is a spec-form containing no import-declarations.
The elaboration of a spec-form yields the Metaslang text which is that spec itself, after expanding any import-declarations. The meaning of that text is the class of models of the spec, as described throughout this Chapter.
Names of types and ops may be simple or qualified. The difference is that simple-names are "unqualified": they do not contain a dot sign ".", while qualified-names are prefixed with a "qualifier" followed by a dot. Examples of simple-names are Date, today and <*>. Examples of qualified-names are Calendar.Date, Calendar.today and Monoid.<*>.
Qualifiers can be used to disambiguate. For example, there may be reason to use two different ops called union in the same context: one for set union, and one for bag (multiset) union. They could then more fully be called Set.union and Bag.union, respectively. Unlike in earlier versions of Specware, there is no rigid relationship between qualifiers and the unit-identifiers identifying specs. The author of a collection of specs may use the qualifier deemed most appropriate for any type- or op-name. For example, there could be a single spec dubbed SetsAndBags that introduces two new ops, one called Set.union and one called Bag.union. Generally, types and ops that "belong together" should receive the same qualifier. It is up to the author of the specs to determine what belongs together.
Type-names and ops are introduced in a declaration or definition, and may then be employed elsewhere in the same spec. Thus, all occurrences of a type- or op-name can be divided into "introductions" and "employs". The name as introduced in an introduction is the full name of the type or op. If that name is a simple-name, the full name is a simple-name. If the name as introduced is a qualified-name, then so is the full name.
For employs the rules are slightly different. First, if the name employed occurs just like that in an introduction, then it is the full name. Also, if the name employed is qualified, it is the full name. Otherwise, the name as employed may be unqualified shorthand for a qualified full name. For example, given an employ of the unqualified type-name Date, possible qualified full names for it are Calendar.Date, DateAndTime.Date, Diary.Date, and so on. But, of course, the full name must be one that is introduced in the spec. If there is precisely one qualified-name introduced whose last part is the same as the simple-name employed, then that name is the full name. Otherwise, type information may be employed to disambiguate ("resolve overloading").
Here is an illustration of the various possibilities:
spec
type Apple
type Fruit.Apple
type Fruit.Pear
type Fruit.Date
type Calendar.Date
type Fruit.Basket = Apple * Pear * Date
endspec |
It is possible to give a qualification in one go to all simple-names introduced in a spec. If Q is a qualifier, and S is a term denoting a spec, then the term Q qualifying S denotes the same spec as S, except that each introduction of an simple-name N is replaced by an introduction of the qualified-name Q.N. Employs that before referred to the unqualified introduction are also accordingly qualified, so that they now refer to the qualified introduction. For example, the value of
Company qualifying spec
type Apple
type Fruit.Apple
type Fruit.Pear
type Fruit.Basket = Apple * Pear
endspec |
spec
type Company.Apple
type Fruit.Apple
type Fruit.Pear
type Fruit.Basket = Company.Apple * Fruit.Pear
endspec |
spec-qualification ::= qualifier qualifying spec-term qualifier ::= word-symbol name ::= simple-name | qualified-name qualified-name ::= qualifier . simple-name |
Sample spec-qualification:
Weight qualifying /Units#Weights |
Key
$
Calendar.Date
Monoid.<*> |
For example, the elaboration of
Buffer qualifying spec
op size : Nat
axiom LargeSize is size >= 1024
endspec |
spec
op Buffer.size : Nat
axiom Buffer.LargeSize is Buffer.size >= 1024
endspec |
spec-translation ::= translate spec-term by name-map name-map ::= { [ name-map-item { , name-map-item }* ] } name-map-item ::= type-name-map-item | op-name-map-item type-name-map-item ::= [ type ] name +-> name op-name-map-item ::= [ op ] annotable-name +-> annotable-name annotable-name ::= name [ : type-descriptor ] |
Sample spec-translation:
translate A by {Counter +-> Register, tally +-> incr} |
For example, the elaboration of
translate spec
type E
op i : E
endspec by {
E +-> Counter,
i +-> reset
} |
spec
type Counter
op reset : Counter
endspec |
spec-substitution ::= spec-term [ morphism-term ] |
Routing#Basis[morphism /Coll/Lattice ->
/Coll/LatticeWithTop {} ] |
The elaboration of spec-substitution S[M] yields the spec T obtained as follows. Let spec R be the result of elaborating S, and morphism N that of M. Let specs D and C be the domain and codomain of N. First, remove from R all declarations of D, and subject the result to the effect of N, meaning that all name translations of N and all extensions with declarations are performed. Then add the declarations of C, but without duplications, i.e., as if C is imported. The result obtained is T.
Restriction. Spec D must be a "sub-spec" of spec R, meaning that each declaration of D is also a declaration of R.
Informally, T is to R as C is to D.
Except when R introduces, next to the type- and op-names it has in common with D, new type- or op-names that also occur in C, the result spec T is a categorical colimit of this pushout diagram:
D ---------> R
| |
| |
| |
v v
C ---------> T |
For example, assume we have:
A = spec
type Counter
op reset: Counter
op tally : Counter -> Counter
axiom Effect is
fa (c : Counter) ~(tally c = c)
endspec
B = spec
type Register = Nat
def reset = 0
def incr c = c+1
endspec
M = morphism A -> B {Counter +-> Register, tally +-> incr}
AA = spec
import A
type Interval = {start: Counter, stop: Counter}
op isEmptyInterval? : Interval -> Boolean
def isEmptyInterval? {start = x, stop = y} = (x = y)
endspec |
spec
import B
type Interval = {start: Register, stop: Register}
op isEmptyInterval? : Interval -> Boolean
def isEmptyInterval? {start = x, stop = y} = (x = y)
endspec |
diagram-colimit ::= colimit diagram-term |
obligator ::= obligations unit-term |
The result of elaborating an obligator is a spec containing the proof obligations engendered by the spec or morphism resulting from elaborating its unit-term. These proof obligations are expressed as conjectures; they can be discharged by proving them, using proof-terms. See further the Specware User Manual.
morphism-term ::= unit-identifier | spec-morphism spec-morphism ::= morphism spec-term -> spec-term name-map |
Restriction. When used as a morphism-term, the elaboration of a unit-identifier must yield a morphism.
Restriction ("proof obligations"). Given spec-morphism morphism S -> T { M1 +-> N1, ... Mn +-> Nn } let R be the result of elaborating S, and let S' be R with each occurrence of a name Mi replaced by Ni. The same rules apply as for spec-translation translate S by {...}, and the result S' must be well formed, with the exception that the restriction on spec-translations requiring different type- or op-names to be mapped to different simple-names does not apply here. Let T' be the result of elaborating T. Then, first, each type-name or op-name introduced in S' must also be introduced in T'. Further, no type-name or op-name originating from a library spec may have been subject to translation. Finally, each claim in S' must be a theorem that follows from the claims of T'. Collectively, the claims in S' are known as the proof obligations engendered by the morphism. They are the formal expression of the requirement that the step from S' to T' is a proper refinement.
For example, in
S = spec endspec
T = spec type Bullion = (Char | isAlpha) endspec
M = morphism S -> T {Boolean -> Bullion} |
S = spec
op f : Nat -> Nat
axiom ff is fa(n:Nat) f(n) ~= f(n+1)
endspec
T = spec
def f(n:Nat) = n*n rem 5
endspec
M = morphism S -> T |
Sample spec-morphism:
morphism A -> B {Counter +-> Register, tally +-> incr} |
The elaboration of spec-morphism morphism S -> T {M} results in the morphism whose domain and codomain are the result of elaborating S and T, respectively, and whose mapping is given by the list of name-map-items in M, using type annotations and indicators type and op as described for spec-translations, and extended to all domain type- and op-names not yet covered by having these map to themselves. (In particular, simple-names from the base-libraries always map to themselves.)
diagram-term ::= unit-identifier | diagram-form diagram-form ::= diagram { diagram-element { , diagram-element }* } diagram-element ::= diagram-node | diagram-edge diagram-node ::= simple-name +-> spec-term diagram-edge ::= simple-name : simple-name -> simple-name +-> morphism-term |
Restriction. In a diagram, the first simple-name of each diagram-node and diagram-edge must be unique (i.e., not be used more than once in that diagram). Further, for each diagram-edge E : ND -> NC +-> M, there must be diagram-nodes ND +-> D and NC +-> C of the diagram such that, after elaboration, M is a morphism from D to C.
Sample diagram:
diagram {
A +-> /Coll/Lattice,
B +-> /Coll/LatticeWithTop,
m : A -> B +-> /Coll/AddTop,
C +-> Routing#Basis,
i : A -> C +-> morphism /Coll/Lattice ->
Routing#Basis {}
} |
The result of elaborating a diagram-form is the categorical diagram whose nodes are labeled with the specs and whose edges are labeled with the morphisms that result from elaborating the corresponding spec-terms and morphism-terms.
target-code-term ::= generate target-language-name spec-term [ generate-option ] generate-option ::= in string-literal | with unit-identifier target-language-name ::= c | java | lisp |
generate lisp /Vessel#Contour
in "C:/Projects/Vessel/Contour.lisp" |
proof-term ::= prove claim-name in spec-term [ with prover-name ] [ using claim-list ] [ options prover-options ] prover-name ::= snark claim-list ::= claim-name { , claim-name }* prover-options ::= string-literal |
Restriction. The claim-names must occur as claim-names in the spec that results from elaborating the spec-term.
Sample proof-term:
prove Effect in obligations M
options "(use-paramodulation t)" |
The elaboration of a proof-term invokes the prover suggested by the prover-name (currently only SNARK). The property to be proved is the claim of the first claim-name; the claim-list lists the hypotheses (assumptions) that may be used in the proof. The prover-options are prover-specific and are not further described here. For details, see the Specware User Manual.