We now refine the application specified above in order to obtain a running program that implements the specified functionality. We do that by defining the specs and morphisms below inside a file MatchingRefinements.sw, in the same directory as MatchingSpecs.sw.
In order to obtain an executable program, we need to choose a concrete representation for the symbols composing words and messages. For example, we can choose uppercase characters:
Symbols = spec
sort Symbol = (Char | isUpperCase)
endspec |
The built-in sort Char is the sort for characters. The built-in op isUpperCase is a predicate on characters that says whether a character is an uppercase letter or not. The subsort construct "|" is used to define the sort Symbol as a subsort of Char.
Note that the above spec has the same name (Symbols) as its corresponding abstract spec. This is allowed and it is a feature of Specware: .sw files define separate name spaces. The file MatchingSpecs.sw creates a name space, and the file MatchingRefinements.sw creates a separate name space. The full name of the spec Symbols in MatchingSpecs.sw is MatchingSpecs#Symbols, while the full name of the spec Symbols in MatchingRefinements.sw is MatchingRefinements#Symbols. Indeed, when Specware is invoked to process a spec (or morphism, etc.), the full name is supplied, as in :sw MatchingSpecs#FindMatches.
The fact that spec MatchingRefinements#Symbols is a refinement of MatchingSpecs#Symbols is expressed by the following morphism:
Symbols_Ref = morphism MatchingSpecs#Symbols ->
MatchingRefinements#Symbols {} |
This text defines a morphism called Symbols_Ref, with domain MatchingSpecs#Symbols and codomain MatchingRefinements#Symbols and where the sort Symbol in MatchingSpecs#Symbols is mapped to the sort Symbol in MatchingRefinements#Symbols.
The specs Words, Messages, and SymbolMatching (in MatchingSpecs.sw) need not be refined, because they constructively define their sorts and ops. But the op word_matches_at? in WordMatching needs to be refined. We do that by constructing a spec that imports the same specs imported by WordMatching and that defines op word_matches_at? in an executable way:
WordMatching0 = spec
import MatchingSpecs#Words
import MatchingSpecs#Messages
import MatchingSpecs#SymbolMatching
op word_matches_at? : Word * Message * Nat -> Boolean
def word_matches_at?(wrd,msg,pos) =
if pos + length wrd > length msg
then false
else word_matches_aux?
(wrd, if pos = 0 then msg
else nthTail(msg, pos - 1))
op word_matches_aux? :
{(wrd,msg) : Word * Message | length wrd <= length msg}
-> Boolean
def word_matches_aux?(wrd,msg) =
case wrd of Nil -> true
| Cons(wsym,wrd1) ->
let Cons(msym,msg1) = msg in
if symb_matches?(wsym,msym)
then word_matches_aux?(wrd1,msg1)
else false
endspec |
Since the imported specs are not in the file MatchingRefinements.sw, their full names are used after import.
The definition of word_matches_at? makes use of an auxiliary op word_matches_aux?, which takes as input a word and a message such that the length of the word is not greater than that of the message. This constraint is expressed as a subsort of the cartesian product Word * Message. Op word_matches_aux? returns a boolean if the word matches the message, at the start of the message. It is defined recursively, by pattern matching on the word. Note the use of let to decompose the msg into the initial symbol and the rest. This is always possible because of the subsort constraint on the word and the message. So, word_matches_at? simply calls word_matches_aux? with the word and the tail of the message obtained by eliminating the first pos symbols, by means of the built-in op nthTail over lists.
The fact that WordMatching0 is a refinement of MatchingSpecs#WordMatching is expressed by the following morphism:
WordMatching_Ref0 = morphism MatchingSpecs#WordMatching ->
WordMatching0 {} |
The refinement for word matching can be composed with the refinement for symbols constructed earlier. This is achieved by means of Specware's substitution operator:
WordMatching = WordMatching0[Symbols_Ref] |
The resulting spec is like WordMatching0, but in addition the sort Symbol is defined to consist of uppercase characters.
The fact that MatchingRefinements#WordMatching is a refinement of MatchingSpecs#WordMatching is expressed by the following morphism:
WordMatching_Ref =
morphism MatchingSpecs#WordMatching ->
MatchingRefinements#WordMatching {} |
Now we proceed to refine op find_matches. We do that in two steps, analogously to word matching above. First, we build a spec FindMatches0 that imports the same specs imported by MatchingSpecs#FindMatches and that defines op find_matches in an executable way:
FindMatches0 = spec
import MatchingSpecs#WordMatching
import MatchingSpecs#Matches
op find_matches : Message * List Word -> List Match
def find_matches(msg,wrds) =
foldl (fn(wrd,mtchs) ->
case find_matches_aux(msg,wrd,0)
of Some pos ->
Cons({word = wrd, position = pos},
mtchs)
| None -> mtchs)
Nil
wrds
op find_matches_aux : Message * Word * Nat -> Option Nat
def find_matches_aux(msg,wrd,pos) =
if pos + length wrd > length msg
then None
else if word_matches_at?(wrd,msg,pos)
then Some pos
else find_matches_aux(msg, wrd, pos + 1)
endspec |
Op find_matches makes use of the auxiliary op find_matches_aux, which takes as input a message msg, a word wrd, and a position pos. It returns either a natural number (a position where the match starts) or None if there is no match. Op find_matches_aux first checks if msg is long enough to possibly contain a match for wrd starting at pos. If that is not the case, None is returned. Otherwise, word_matches_at? is called: if it returns true, then the position pos is returned (wrapped by Some). Otherwise, find_matches_aux is recursively called, incrementing the position by 1. So, when find_matches_aux is called with 0 as its third argument, it iterates through the message to find the first match, if any. The position of the first match is returned, otherwise None.
The op find_matches iterates through the words of the list constructing a list of matches. The iteration is performed by means of the built-in op foldl for lists. For each word, find_matches_aux is called, with 0 as its third argument. Then, a pattern matching on the result is done: if the result is a position, a match is added to the output list; otherwise, the list is left unmodified.
The following morphism expresses that FindMatches0 is a refinement of MatchingSpecs#FindMatches:
FindMatches_Ref0 = morphism MatchingSpecs#FindMatches ->
FindMatches0 {} |
This refinement for MatchingSpecs#FindMatches can be composed with the one for MatchingSpecs#WordMatching built earlier. The composition is analogous to the one for MatchingSpecs#WordMatching:
FindMatches = FindMatches0[WordMatching_Ref] |
The resulting spec includes the refinement for op find_matches as well as the refinement for op word_matches_at? and for symbols.
The fact that MatchingRefinements#FindMatches is a refinement of MatchingSpecs#FindMatches is expressed by the following morphism:
FindMatches_Ref =
morphism MatchingSpecs#FindMatches ->
MatchingRefinements#FindMatches {} |
All the specs and morphisms of the file MatchingRefinements.sw can be processed by means of the following command:
:sw MatchingRefinements#FindMatches_Ref |
In general, a morphism has proof obligations associated to it: all the axioms in the source spec must be mapped to theorems in the target spec. These proof obligations are expressed in the form of a spec obtained by extending the target spec of the morphism with the axioms of the source spec (translated along the morphism) as conjectures. The user can then attempt to prove these conjectures using theorem provers linked to Specware.
We collect the proof obligations of the morphisms defined above in a file MatchingObligations.sw, in the same directory as MatchingSpecs.sw and MatchingRefinements.sw. The file contains the following definitions:
SymbolMatching_Oblig =
obligations MatchingSpecs#SymbolMatching
Symbols_Ref_Oblig =
obligations MatchingRefinements#Symbols_Ref
WordMatching_Ref0_Oblig =
obligations MatchingRefinements#WordMatching_Ref0
FindMatches_Ref0_Oblig =
obligations MatchingRefinements#FindMatches_Ref0 |
SymbolMatching_Oblig is a spec that expresses the proof obligations that arise as a result of typechecking the spec SymbolMatching. Symbols_Ref_Oblig, WordMatching_Ref0_Oblig, and FindMatches_Ref0_Oblig are specs that express the proof obligations of the associated morphisms as conjectures. Specware provides the capability to display (i.e., print) any spec, morphism, etc., via the :show command. This command can be used to see the proof obligations associated to the morphisms, by displaying the specs expressing such obligations.
For instance, the proof obligations associated to the morphism Symbols_Ref can be displayed by using the following command:
:show MatchingObligations#Symbols_Ref_Oblig |
The absence of conjectures indicates that no proof obligations need to be discharged in order to establish the validity of the morphism Symbols_Ref. In fact, this morphism is very simple: its source MatchingSpecs#Symbols has no axioms, just an abstract sort Symbol that the morphism maps to the concretely defined sort Symbol in MatchingRefinements#Symbols.
Unlike Symbols_Ref, WordMatching_Ref0 has a non-trivial proof obligation that needs to be discharged in order to establish the validity of the morphism. Inspection (via :show) of the spec WordMatching_Ref0_Oblig reveals a conjecture. The conjecture is the axiom about word_matches_at? in MatchingSpecs#WordMatching, which is indeed provable from the executable definition of word_matches_at?.
Also FindMatches_Ref0 has a non-trivial proof obligation, consisting of the axiom about find_matches in MatchingSpecs#FindMatches. This obligation is indeed provable from the executable definition of find_matches.
The validity of the morphisms WordMatching_Ref and FindMatches_Ref follows from the validity of the morphisms Symbols_Ref, WordMatching_Ref0, and FindMatches_Ref0. The reason is that sequential composition of morphisms always yields a morphism and that substitution always produces a spec and (implicitly) two morphisms.
WordMatching_Ref is the sequential composition of WordMatching_Ref0 with the morphism from WordMatching0 to MatchingRefinements#WordMatching that is implicitly computed by the substitution operator used to define MatchingRefinements#WordMatching. Similarly, FindMatches_Ref is the sequential composition of FindMatches_Ref0 with the morphism from FindMatches0 to MatchingRefinements#FindMatches that is implicitly computed by the substitution operator used to define MatchingRefinements#FindMatches.
Specware provides the capability to invoke external theorem provers in order to attempt proofs of conjectures. Concretely, this is carried out by creating proof objects. Each proof object is associated with a certain conjecture in a certain spec; it also indicates the prover to use and some directives on how to perform the proof. Processing of the proof object invokes the indicated prover with the given directives. Currently, the only available prover is Snark; more provers will be added in the future.
For example, the user can attempt to discharge the proof obligation for MatchingSpecs#SymbolMatching by writing the following command in a file named MatchingProof.sw, located in the same directory as MatchingObligations.sw:
prove symb_matches? in
MatchingObligations#SymbolMatching_Oblig |
:sw MatchingProof |