The refinement for the word matching application developed above is certainly not the only one possible.
For example, we could have refined symbols differently. We could have refined them to be all letters (uppercase or lowercase) and numbers, or to be natural numbers. It is worth noting that the refinement for symbols is encapsulated in spec MatchingRefinements#Symbols. If we want to change the refinement for symbols, we just need to change that spec, while the other specs remain unaltered.
As another example, we could have chosen a more efficient refinement for op find_matches, using some fast substring search algorithm. In particular, while we have refined op word_matches_at? first, and then composed its refinement with one for find_matches, we could have refined find_matches "directly", without using word_matches_at?, so that it would have been unnecessary to refine word_matches_at?.
The latter example illustrates an important principle concerning refinement. In general, it is not necessary to refine all ops present in a spec. Only the ops that are meant to be used by an external program need to be refined to be executable, and in turn the ops that are used inside their executable definitions. Other ops serve only an auxiliary role in specifying abstractly the ops that are meant to be eventually refined.
Currently, Specware provides no support to indicate explicitly which ops are meant to be "exported" by a spec. In future versions of the system, some functionality like this may be included.