Text Box: 1The purpose of this assignment is to give you experience developing an Object-Z specification towards an implementation using refinement and refactoring. The case study is a document search engine. The search engine allows a user to load a number of text documents, and then perform searches for words contained in those documents.
The search engine has two modes of operation: it either searches for documents which contain all words in the query, or some (i.e., one or more) words in the query. It has three operations as follows.
LoadDoc loads a document into the search engine (the document will be an input) ToggleMode toggles the mode of the document between 'all words' and 'some words'
Query finds the previously loaded documents which satisfy a query (the input will be a sequence of words denoting the query, and the output a mapping from words in the query to document records - see below).
A document record consists of two components: the name of a document, and a number denoting the number of occurrences of a particular word in that document. The document records associated with a word w in the output of Query are such that: (i) the document name is the name of a document d containing w, and (ii) the number is the number of occurrences of w in d.
The output of Query is meant to be sent to a user interface class responsible for sorting and presenting the information to the search engine user. This user interface class is outside the system we are concerned with in this assignment.
Task 1
Your first task is to specify the search engine as a single Object-Z class SearchEngine. You will need to choose appropriate types for words, documents and document records.
Task 2
Your second task is to modify the design of the Object-Z specification from Task 1 as follows.
1. To ensure the search engine operates efficiently, documents will be searched for the words they contain when first loaded rather than on each query. When a document is loaded, the search engine will store the required information about the document in a word table. The word table maps a given word to a set of document records. Each document record in the set will correspond to a document which contains the word, and the number of times the word occurs in that document.
A new class WordTable will be added to the specification. This class is not responsible for dealing with adjusting the output according to the mode. That responsibility should remain with the SearchEngine class.
2. Assume the following class Comparable is also part of the specification.
A subclass of Comparable called DocRecordl will be added to the specification for representing document records. The class should capture the same information as a document record and additionally have a Compare To operation which (like the compareTo method of the class Comparable in Java) outputs a negative number whenever the input (an instance of DocRecordl) has a larger number, a positive value when the input has a smaller number, and zero when it has the same number.
3. Finally, modify the specifications of SearchEngine and WordTable to use DocRecordl in place of your document record type.
Each modification of the specification will require one or more refactoring and/or refinement steps. You do not need to prove the refinement steps, but for each you should (i) state the proof obligations, (ii) specify any schemes needed by them, e.g., the schema R representing the retrieve relation for a data refinement, and (iii) provide a short informal (English) justification for why the refinement holds.
Each class and schema in your assignment should be preceded by explanatory text. This text should not simply paraphrase the formal text, but explain it in the context of the specification development. Further text may follow a class or schema where necessary, e.g., to help clarify complicated predicates.