Code Generation and Testing

Code Generation

Now that our simple word matching application has been refined to be executable, we can generate code from it. This is concretely achieved by creating a (Lisp) program from a spec, indicating a file name where the code is deposited as a side effect. The following command is given in the shell:

    gen-lisp <specname> <targetfilename>

The above command first processes the named spec and then generates Lisp code from it, writing the code into the indicated file. The file is created if it does not exist; if it exists, it is overwritten.

For instance, we can generate Lisp code for the word matching application by means of the following command:

    gen-lisp MatchingRefinements#FindMatches find-matches

Note that if the .lisp suffix is omitted, Specware adds it to the file name.

After we generate the code, we can then try to run it by calling the Lisp function produced from op find_matches. Since messages and words are represented as lists of characters (plus None for messages), it would be slightly inconvenient to enter and read lists of characters. It would be better to enter strings with letters and *'s, as shown in the informal problem description at the beginning of this chapter.

In order to do that, we define translations between strings and messages and words, and we wrap find_matches in order to translate from and to strings. We do that inside a spec called Test in a file MatchingTest.sw in the same directory as the other .sw files:

    Test = spec
  
    import MatchingRefinements#FindMatches
  
    op word_char?(ch: Char): Boolean = isUpperCase ch
  
    op msg_char?(ch: Char): Boolean = isUpperCase ch || ch = #*
  
    type WordString = (String | all word_char?)
  
    type MessageString = (String | all msg_char?)
  
    op word2string(wrd: Word): WordString = implode wrd
  
    op string2word(wstr: WordString): Word = explode wstr
  
    op message2string(msg: Message): MessageString =
      implode(map (fn Some ch -> ch | None -> #*) msg)
  
    op string2message(mstr: MessageString): Message =
      map (fn ch -> if ch = #* then None else Some ch)
        (explode mstr)
  
    type MatchString = {word : WordString, position : Nat}
  
    op match2string(mtch: Match): MatchString =
        {word = word2string mtch.word, position = mtch.position}
  
    op test_find_matches(mstr: MessageString, wstrs: List WordString)
         : List MatchString =
      map match2string
        (find_matches(string2message mstr, map string2word wstrs))
  
    def implode l = foldl (fn (s,c) -> s ^ toString c) "" l
    def explode s =
      if s = "" then []
        else sub(s,0) :: explode(substring(s,1,length s))
    
    endspec

Since the translation is not defined on all strings, we introduce two subtypes of the built-in type String: the type WordString consists of all strings whose characters are uppercase letters; the type MessageString consists of all strings whose characters are uppercase letters or *. The built-in op all over strings is used to define the subtypes, using the ops (predicates) word_char? and msg_char?.

The op word2string translates a word to a word string, by means of the built-in op implode. The op string2word performs the opposite translation, using the built-in op explode. The ops message2string and string2message translate between messages and string messages. Besides the use of implode and explode, they need to map Some ch from/to ch (where ch is an uppercase letter) and None from/to *.

Since find_matches returns a match, i.e., a pair consisting of a word and a position, we define a type MatchString consisting of a word string and a position, together with an op match2string that translates from a match to a string match.

Finally, we define an op test_find_matches to take a message string and a list of word strings as input, and to return a list of string matches as output. The message string and word strings are first translated to a message and list of words, then find_matches is called, and then the resulting matches are translated to string matches. Note that the op message2string is never used. In fact, it could have been omitted.

Now, instead of generating code from MatchingRefinements#FindMatches, we generate code from MatchingTest#Test:

    gen-lisp MatchingTest#Test find-matches-test.lisp

Testing

In order to test the generated Lisp code, we need to load the generated Lisp file into a Lisp environment (provided with Specware). We do that by means of the following command (this and all the following commands must be given in the Lisp environment, not the Specware shell):

    ld find-matches-test

In Lisp, entities like functions, constants, etc. are defined inside packages. When Specware generates code, it puts it inside a package named sw-user. This can be seen from the package declaration at the beginning of file find-matches-test.lisp (note that Lisp is case-insensitive).

So, in order to call the functions defined in that file (after it has been loaded), it is necessary either to prepend the package name to them, or to move to that package and then call them without package qualification. To follow the first approach, we would write (sw-user::test_find_matches-2 <arg1> <arg2>) to call the function. (The "-2" appended to the function name is for the two-argument version of the Lisp function; see the Section on Arity and Currying Normalization in the User Manual. Alternatively, we can supply a single argument by consing <arg1> and <arg2>, thus: (sw-user::test_find_matches (cons <arg1> <arg2>)).)

To follow the second approach, we would first change package by means of the Lisp command pa sw-user, and then we can just write (test_find_matches-2 <arg1> <arg2>) to call the function.

In order to test the program on the example input and output given at the beginning of the chapter, we proceed as follows. First, we define a variable containing the message:

    (setq msg "**V*ALN**EC*E*S")

Then we define a variable containing the list of words:

    (setq words '("CERAMIC" "CHESS" "DECREE" "FOOTMAN"
                  "INLET" "MOLOCH" "OCELOT" "PROFUSE"
                  "RESIDE" "REVEAL" "SECRET" "SODIUM"
                  "SPECIES" "VESTIGE" "WALNUT" "YOGURT"))

Finally, we call (assuming to be in package sw-user):

    (test_find_matches-2 msg words)

The following result is then displayed:

    ((3 . "WALNUT") (7 . "SPECIES") (8 . "SECRET")
     (0 . "REVEAL") (8 . "DECREE") (10 . "CHESS"))

The result is a list of pairs, each of which represents a match.