| Specware 4.0 Tutorial | ||
|---|---|---|
| Prev | Chapter 2. Example | |
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 Lisp shell:
:swl <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:
:swl 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 two .sw files:
Test = spec
import MatchingRefinements#FindMatches
op word_char? : Char -> Boolean
def word_char? ch = isUpperCase ch
op msg_char? : Char -> Boolean
def msg_char? ch = isUpperCase ch or ch = #*
sort WordString = (String | all word_char?)
sort MessageString = (String | all msg_char?)
op word2string : Word -> WordString
def word2string wrd = implode wrd
op string2word : WordString -> Word
def string2word wstr = explode wstr
op message2string : Message -> MessageString
def message2string msg =
implode(map (fn msym -> case msym
of Some ch -> ch
| None -> #*)
msg)
op string2message : MessageString -> Message
def string2message mstr =
map (fn ch -> if ch = #* then None else Some ch)
(explode mstr)
sort MatchString = {word : WordString, position : Nat}
op match2string : Match -> MatchString
def match2string mtch =
{word = word2string mtch.word,
position = mtch.position}
op test_find_matches :
MessageString * List WordString -> List MatchString
def test_find_matches(mstr,wstrs) =
map match2string
(find_matches(string2message mstr,
map string2word wstrs))
endspec |
Since the translation is not defined on all strings, we introduce two subsorts of the built-in sort String: the sort WordString consists of all strings whose characters are uppercase letters; the sort MessageString consists of all strings whose characters are uppercase letters or *. The built-in op all over strings is used to define the subsorts, 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 sort 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:
:swl MatchingTest#Test find-matches-test.lisp |
In order to test the generated code, we need to load the generated Lisp file into the Lisp environment. We do that from the Lisp shell, by means of the following command:
: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 <arg1> <arg2>) to call the function. 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 <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 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.