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
type Symbol = (Char | isUpperCase)
endspec |
The built-in type Char is the type for characters. The built-in op isUpperCase is a predicate on characters that says whether a character is an uppercase letter or not. The subtype construct "|" is used to define the type Symbol as a subtype 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 proc 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 type Symbol in MatchingSpecs#Symbols is mapped to the type Symbol in MatchingRefinements#Symbols.
The specs Words, Messages, and SymbolMatching (in MatchingSpecs.sw) need not be refined, because they constructively define their types 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 subtype 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 subtype 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 type 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:
proc 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.
Also specs have proof obligations associated to them. Some are part of typechecking, e.g., if an expression of a type T is used as an argument to a function whose domain is a subtype T|p of T, the expression must satisfy p, in the context in which the application occurs. Others arise from definitions via def: the equation must be uniquely define the op. The proof obligations associated to a spec ensure that the spec satisfied certain expected well-formedness properties, which is useful to validate the spec.
We collect the proof obligations of the specs and morphisms defined above in a file MatchingObligations.sw, in the same directory as MatchingSpecs.sw and MatchingRefinements.sw. The file contains the following definitions:
%%% obligations from MatchingSpecs.sw:
SymbolMatching_Oblig =
obligations MatchingSpecs#SymbolMatching
WordMatching_Oblig =
obligations MatchingSpecs#WordMatching
%%% obligations from MatchingRefinements.sw:
WordMatching0_Oblig =
obligations MatchingRefinements#WordMatching0
WordMatching_Ref0_Oblig =
obligations MatchingRefinements#WordMatching_Ref0
FindMatches0_Oblig =
obligations MatchingRefinements#FindMatches0
FindMatches_Ref0_Oblig =
obligations MatchingRefinements#FindMatches_Ref0 |
SymbolMatching_Oblig is a spec that expresses the proof obligations associated to the spec SymbolMatching as conjectures. Analogously for WordMatching_Oblig, WordMatching0_Oblig, and FindMatches0_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 specs and morphisms, by displaying the specs expressing such obligations: the conjectures are the obligations.
Note that not all specs and morphisms from MatchingSpecs.sw and MatchingRefinements.sw are listed in MatchingObligations. Those that are not listed have really no proof obligations associated to them. For example, inspection (via show) of obligations MatchingSpecs#Symbols would reveal no conjectures because the spec is very simple (it just declared an abstract type). As another example, the spec MatchingRefinements#WordMatching is built by substituting MatchingSpecs#Symbols with MatchingRefinements#Symbols in WordMatching0: thus, the validity of the morphism WordMatching_Ref (i.e., that all axioms in the source are theorems in the target) follows immediately from the validity of the morphism WordMatching_Ref0.
The proof obligations associated to the spec SymbolMatching can be displayed by using the following command:
show MatchingObligations#SymbolMatching_Oblig |
The spec only contains one conjecture, arising from the typechecking of the case expression used in the definition of symb_matches?, namely that the branches cover all possible cases, which is very easy to prove.
The spec MatchingSpecs#WordMatching has three proof obligations, all arising from subtypes, e.g., that pos + i < length msg in the context that (i.e., under the assumption that) pos + length wrd <= length msg and i < length wrd.
The morphism FindMatches_Ref0 contains the "main" proof obligation of the overall refinement, namely that the definitio of find_matches in MatchingRefinements#FindMatches0 satisfies the axiom in MatchingSpecs#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 MatchingProofs.sw, located in the same directory as MatchingObligations.sw:
p1 = prove symb_matches? in
MatchingObligations#SymbolMatching_Oblig |
At the shell, the user can issue this command to attempt the proof:
proc MatchingProofs#p1 |
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.