Specification

Construction

We specify the application in a bottom-up fashion. We build specs for the concepts involved in the application, starting with the simplest ones up to the spec for the application.

Metaslang provides strings of characters among the built-in types, ops, and axioms. We could define messages and words as strings satisfying certain properties, e.g., that the character * can appear in messages but not in words, etc.

However, it is generally better to specify things as abstractly as possible. It is clear that the problem as stated above does not depend on obscured characters being represented as * and on non-obscured characters being uppercase letters only, or letters and numbers, or other. The abstract notion is that there are characters that form words, and messages are made of those characters but some characters may be obscured.

So, we start with a spec for symbols (i.e., characters):

    Symbols = spec
      type Symbol
    endspec

This is a very simple spec: it just consists of one type. This is perfectly adequate because the application treats symbols atomically: it only compares them for equality (which is built-in in Metaslang for every type). Any further constraint on symbols would just make the spec unnecessarily less general.

The text above is Metaslang syntax: it not only introduces a spec consisting of the type Symbol, but also assigns a name to it, Symbols. This spec can thus be referred to by its name, as shown shortly. The exact way in which the text above is supplied to Specware is explained later.

Now that we have the concept of symbols, we can introduce the concept of word as a sequence of symbols. Metaslang provides lists, built-in. The polymorphic type List a is used to define words:

    Words = spec
      import Symbols
      type Word = List Symbol
    endspec

The name of the spec is Words. The spec imports Symbols defined above, and extends it with a new type Word, defined to be List Symbol. This type is obtained as an instantiation of List a by replacing the type parameter a with Symbol.

A message is a sequence of symbols some of which may be obscured. This can be specified by lists whose elements are either symbols or a special extra value that stands for an "obscured symbol" (the "*" in the problem description given earlier).

Metaslang provides, built-in, a polymorphic type Option a that adds an extra element to a type. More precisely, it is defined as type Option a = | Some a | None. The type Option a is defined as a coproduct of type a tagged by Some and the singleton type consisting of the constant None.

So, we can define messages as follows:

    Messages = spec
      import Symbols
      type Message = List (Option Symbol)
    endspec

At this point, we can define the notion of symbol matching: a symbol must be matched by the exact same symbol, while an obscured symbol may be matched by any symbol. This is captured by the following spec:

    SymbolMatching = spec
    import Symbols
    
    op symb_matches?(s: Symbol, os: Option Symbol): Boolean
      = case os of
          | Some s1 -> s = s1
          | None    -> true
    endspec

The spec imports Symbols and extends it with an op symb_matches? that returns a boolean from a pair whose first component is a symbol and the second component is a possibly obscured symbol. This op can be viewed as a binary predicate. The op is defined by pattern matching on the second argument, in a straightforward way. Note that s = s1 is a term of type Boolean.

The definition is constructive in the sense that code can be eventually generated directly, without any need to refine it. This is one of those cases where the simplest and most abstract definition of an op happens to be directly executable.

Having the notion of symbol matching, now we define the notion of word matching, i.e., when a word matches a message. We could define an op (predicate) of type Word * Message -> Boolean. However, since the application involves offsets for matching words, it is better to declare the op to have type Word * Message * Nat -> Boolean: the predicate is true if the given word matches the given message at the given position. Here is the spec:

    WordMatching = spec
    
    import Words
    import Messages
    import SymbolMatching
  
    op word_matches_at?(wrd: Word, msg: Message, pos: Nat)
         : Boolean =
      pos + length wrd <= length msg &&
      (fa(i:Nat) i < length wrd
         => symb_matches?(wrd@i, msg@(pos+i)))
  
    endspec

First, the spec imports the specs for words, messages, and symbol matching. Then it introduces the op word_matches_at?, with the type explained above. Its definition says that the predicate holds on a triple (wrd,msg,pos) if and only if two conditions are satisfied:

1. msg is long enough to possibly contain the whole wrd at position pos;

2. every symbol of wrd at position i matches the corresponding, possibly obscured symbol in msg at position pos + i.

Note the use of symb_matches? previously defined. The ops length and @ are built-in, polymorphic ops over lists: the former returns the length of a list, while the latter returns the n-th element of a list (n is numbered starting from 0).

Unlike symb_matches? above, the definition of word_matches_at? is not executable. This means that it must be eventually refined. An executable definition of this op involves some kind of loop through the message: so, it would not be as simple and abstract as it is now. The general rule is that, at the specification level, things should be expressed as simply, clearly, and declaratively as possible.

Having all the above concepts in hand, we are ready to define how a message and a list of words are processed by the application to produce a list of matches. As explained in the problem description above, a match is not only a word, but also the (least) position in the message at which the match occurs. So, it is appropriate to define the concept of a match, as a pair consisting of a word and a position (i.e., a natural number):

    Matches = spec
      import Words
      type Match = {word : Word, position : Nat}
    endspec

The type Match is defined to be a record with two components, named word and position. A record is like a cartesian product, but the components have user-chosen names.

Finally, the spec for the whole application is the following:

    FindMatches = spec
  
    import WordMatching
    import Matches
  
    op find_matches : Message * List Word -> List Match
    axiom match_finding is
      fa(msg,wrds,mtch)
        mtch in? find_matches(msg,wrds)
         <=>
        mtch.word in? wrds
         && word_matches_at?(mtch.word,msg,mtch.position)
         && (fa(pos) word_matches_at?(mtch.word,msg,pos)
               => pos >= mtch.position)
  
    endspec

The spec imports WordMatching and Matches, and declares an op find_matches that, given a message and a list of words, returns a list of matches. This op captures the processing performed by the application. The axiom (whose name is match_finding) states the required properties. The built-in polymorphic op member is a predicate that says whether an element belongs to a list or not. So, the required property for find_matches is the following: given a message msg and a list of words wrds, a match mtch belongs to the result of find_words if and only if:

1. the word of the match is in wrds, i.e., the word must have been given as input;

2. the word can be matched with msg at the position indicated by the match;

3. the position of the match is the least position where the word matches.

Note how the specification of this word matching application is simple and abstract. No commitments have been made to particular data structures or algorithms. These commitments are made during the refinement process. Note also that the op find_matches is not completely defined by the axiom: the order of the resulting matches is not specified (the axiom only says what the members of the resulting list are, but not their order). The axiom does not prohibit duplicate elements in the output list; a suitable conjunct could be added to enforce uniqueness, if desired. This under-specification is consistent with the informal problem description given above. Of course, it is possible to change the axiom to require a particular order (e.g., the same as in the input list), if desired.

Processing by Specware

How do we actually enter the above text into Specware and how do we have Specware process it?

The current version of Specware works more or less like a compiler: it processes one or more files producing results. The files define specs, morphisms, etc. The results include error messages if something is wrong (e.g., type errors in specs), and possibly the generation of other files (e.g., containing code generated by Specware).

The files processed by Specware are text files with extension .sw (the "s" and "w" come from the first and fifth letter of "Specware"). A .sw file contains a sequence of definitions of specs, morphisms, etc.

For the word matching application constructed above, it is sensible to put all the specs above inside a file MatchingSpecs.sw:

    Symbols = spec
      type Symbols
    endspec
    
    ...
    
    FindMatches = spec
     ...
    endspec

Unlike a traditional compiler, the interaction with Specware is within a shell. When Specware is started, the shell is available for interaction with Specware (Specware is part of the Lisp image). In the shell, the user can move to any desired directory of the file system by means of the cd command, followed by the name of the directory, e.g., cd c:\mydir (Windows) and cd ~/mydir (Linux). Usually, the .sw files that form an application are put inside a directory, and from the shell the user moves to that directory.

In order to have Specware process a spec (or morphism, etc.) contained in a .sw file in the current directory, the user provides the following command in the shell:

    proc <filename>#<specname>

The <filename> portion of the argument string is a place holder for the file name (without the .sw extension); the <specname> portion is a place holder for the spec (or morphism, etc.) name as it appears inside the file.

The effect of the above command is to have Specware process the indicated spec (or morphism, etc.) in the indicated file, recursively processing other specs, morphisms, etc. that are referenced by the indicated spec.

To have Specware process the spec of the word matching application, the command is:

    proc MatchingSpecs#FindMatches

This has the effect of processing the spec named FindMatches in file MatchingSpecs.sw. Since this spec imports specs WordMatching and Matches, these are processed first, and so are the specs imported by them, recursively. Thus, all the specs in MatchingSpecs.sw are processed. FindMatches is the top-level spec in the file.

Specware finds the specs WordMatching and Matches, imported by FindMatches, because they are contained in the same file. As it will be explained shortly, it is possible to refer from one file to specs defined in different files.