This chapter presents a step-by-step example of a small application developed with Specware. Despite its small size, the example illustrates the general methodology to develop software with Specware. Furthermore, the description of the example includes concrete explanations to run the example through Specware, thus serving as a usage tutorial. The code for this example may be found in the Examples\Matching\ folder in your installation directory (e.g. C:\Program Files\Specware\).
The problem solved by this simple application is the following. A message is given, consisting of a sequence of characters, some of which are "obscured", i.e., it may look something like:
**V*ALN**EC*E*S |
Then, a list of words is given, where a word is a sequence of characters, e.g.:
CERAMIC
CHESS
DECREE
FOOTMAN
INLET
MOLOCH
OCELOT
PROFUSE
RESIDE
REVEAL
SECRET
SODIUM
SPECIES
VESTIGE
WALNUT
YOGURT |
Even though the above list is alphabetically sorted, the list of words can be given in any order.
The application must find which words of the list may occur somewhere in the message, where an obscured character in the message may match any character in a word, while a non-obscured character must be matched exactly. The application must also show the offset in the message at which the possible occurrence is found; if there is more than one offset, the smallest one should be returned. So, the output for the example message and word list above is the following:
10 CHESS
8 DECREE
0 REVEAL
8 SECRET
7 SPECIES
3 WALNUT |
Again, even though the list of words and numbers is alphabetically ordered, the application can produce it in any order.