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, mprhisms, 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.
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 |
Unit-definitions may use other unit-definitions, including standard libraries, which in Specware 4.0 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.0 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 [ # path-element ] path-element ::= word-symbol |
Warning. Note that unit-identifiers are processed by the tokenizer like everything else. This means that whitespace is removed and marks not allowed in names, 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.
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 a "closed" spec-form as defined in the next subsection.
spec-form ::= spec { declaration }* endspec |
Sample spec-forms:
spec import Measures import Valuta endspec |
A closed 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 sorts and ops may be unqualified or qualified. The difference is that unqualified-names do not contain a dot sign ".", while qualified-names are prefixed with a "qualifier" followed by a dot. Examples of unqualified 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 sort-name 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, sorts and ops that "belong together" should receive the same qualifier. It is up to the author of the specs to determine what belongs together.
Sort-names and op-names are introduced in a declaration or definition, and may then be employed elsewhere in the same spec. Thus, all occurrences of a sort-name or op-name can be divided into "introductions" and "employs". The name as introduced in an introduction is the full name of the sort or op. If that name is unqualified, the full name is unqualified. If the name as introduced is qualified, 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 sort-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 unqualified-name employed, then that name is the full name. Otherwise, sort information may be employed to disambiguate ("resolve overloading").
Here is an illustration of the various possibilities:
spec
sort Apple
sort Fruit.Apple
sort Fruit.Pear
sort Fruit.Date
sort Calendar.Date
sort Fruit.Basket = Apple * Pear * Date
endspec |
It is possible to give a qualification in one go to all unqualified-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 unqualified-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
sort Apple
sort Fruit.Apple
sort Fruit.Pear
sort Fruit.Basket = Apple * Pear
endspec |
spec
sort Company.Apple
sort Fruit.Apple
sort Fruit.Pear
sort Fruit.Basket = Company.Apple * Fruit.Pear
endspec |
spec-qualification ::= qualifier qualifying spec-term qualifier ::= word-symbol qualifiable-name ::= unqualified-name | qualified-name unqualified-name ::= name qualified-name ::= qualifier . name |
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 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 ::= sort-name-map-item | op-name-map-item sort-name-map-item ::= [ sort ] qualifiable-name +-> qualifiable-name op-name-map-item ::= [ op ] annotable-qualifiable-name +-> annotable-qualifiable-name annotable-qualifiable-name ::= qualifiable-name [ : sort ] |
translate A by {Counter +-> Nat} |
For example, the elaboration of
translate spec
sort E
op i : E
endspec by {
E +-> Counter,
i +-> zero
} |
spec
sort Counter
op zero : 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 C must be a "sub-spec" of spec R, meaning that each declaration of C is also a declaration of R.
Informally, T is to R as C is to D.
Except when R introduces, next to the sort-names and op-names it has in common with D, new sort-names 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
sort Counter
op reset: Counter
op tick : Counter -> Counter
axiom Effect is
fa (c : Counter) ~(tick c = c)
endspec
B = spec
def reset = 0
def tick c = c+1
endspec
M = morphism A -> B {Counter +-> Nat}
AA = spec
import A
sort Interval = {start: Counter, stop: Counter}
op isEmptyInterval? : Interval -> Boolean
def isEmptyInterval? {start = x, stop = y} = (x = y)
endspec |
spec
import B
sort Interval = {start: Nat, stop: Nat}
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 spec morphism.
Restriction ("proof obligations"). Given spec-morphism morphism S -> T { M }, let S' be the result of elaborating translate S by { M }, and let T' be the result of elaborating T. Then, first, each sort-name or op-name introduced in S' must also be introduced in T'. Further, no sort-name or op-name originating from a library spec may have been subject to translation. Finally, each axiom in S' must be a theorem that follows from the axioms of T'. Collectively, the axioms 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.
diagram-term ::= unit-identifier | diagram-form diagram-form ::= diagram { diagram-element { , diagram-element }* } diagram-element ::= diagram-node | diagram-edge diagram-node ::= name +-> spec-term diagram-edge ::= name : name -> name +-> morphism-term |
Restriction. In a diagram, the first 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 [ in string-literal ] target-language-name ::= 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 translate A by {Counter +-> Nat}
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.