\documentclass[11pt]{report} \usepackage{a4,xy} \xyoption{all} \input{macros.tex} \begin{document} \title{A Student Dictionary System\footnote{project written in the course of the RISC-lecture {\em Formal Specification of Abstract Data Types}}} \author{Fabrizio Caruso\and Carsten Schneider\and Geert Van de Weyer} \maketitle \begin{abstract} In this document we present a loose specification of a student dictionary system. The presented specification not only allows the user to generate a dictionary and get translations of a word, but it also allows the user to generate a test suite to test his knowledge of a given language. Apart from the loose specification, we also provide an implementation of the specification in the cafeOBJ language. And use this implementation to illustrate the functionality of the dictionary system with examples. \end{abstract} \tableofcontents \chapter{Introduction} In this paper we will present a loose specification of a student dictionary system. The primary purpose of this system is to allow its user to test his current knowledge of a certain language by generating a test suite. In addition to this main purpose, other operations are of course also provided. These operations include the generation and construction of dictionaries, automated translation of a given word and alphabetically ordered output of all known words. Besides the loose specification, we also provide an implementation of this specification in the cafeOBJ language. This implementation provides examples of the various aspects of the student dictionary. The remaining part of this paper has two more chapters. The first chapter of these two is titled {\em The Mechanics of the Specification}. It contains the entire loose specification, cut into parts. For each of these parts, we give the main ideas behind this specification. The last chapter then contains the cafeOBJ implementation of the specification and demonstrates the working of the dictionary through some examples. \chapter{The Mechanics of the Specification} Let us first of all explain the main idea behind the entire specification. The very core of the dictionary system is the sort $vocsystem$ (short for vocabulary system). This sort has two major components: a couple of languages, and a list of vocabulary items. Of this couple of languages, the first is called the native language and the second is called the foreign language. The list of vocabulary items then contains the actual data of the dictionary, which is represented by the sort $vocitem$ (short for vocabulary item). This sort $vocitem$ actually has two components. The first component is a pair of words, its first entry containing a native word and its second entry containing the foreign translation of the first entry. The second component of a $vocitem$ is a boolean value. This value is used when generating a test suite: it tells the system whether the vocabulary item is already in the test suite or not. It is clear from this description that the sorts $vocsystem$ and $vocitem$ are composed out of other sorts, representing the brickwork that is always used to build any dictionary, electronically or not. This brickwork, of course, are the languages and the words in which the languages are written. In our loose specification, we introduced the sorts $language$ and $word$ to represent these basic concepts of any dictionary. We chose to work with this sort $word$ internally instead of working with the simpler sort $string$ for a very natural reason: the notion of $word$ which we introduced has apart from a string also a component $language$. This allows us to check the spelling of a string when making it into a word, avoiding tedious spelling checks throughout the dictionary later on. The $language$ sort then contains the two final aspects one needs to build up a dictionary. These are the characters and their ordering, and the lexicographical rules, telling which character combinations cannot occur in a language. The purpose of these lexicographical rules is to avoid often occuring typing mistakes. The build-up explained in the previous paragraphs can be visualised nicely using the following graph: \begin{figure} \xymatrix{ & & *+[F]{\txt{Character}}\ar[ddl]\ar[ddddd] & *+[F]{\txt{SimpleList}}\ar@{.>}[ddd]\ar@{.>}[lddddd] \cr\cr & *+[F]{\txt{SimpleCharacterOrder}}\ar[d] & & \cr & *+[F]{\txt{CharacterOrder}}\ar[ddddr]\ar[ddddd] & & *+[F]{\txt{List}}\ar@{.>}[llu]\ar@{.>}[lllddd] \cr\cr & & *+[F]{\txt{SimpleString}}\ar[dd]\ar[dll] & \cr *+[F]{\txt{SimpleRule}}\ar[d] & & &\cr *+[F]{\txt{Rule}}\ar[rd]& & *+[F]{\txt{String}}\ar[dd] & &\cr & *+[F]{\txt{Language}}\ar[rd] & & &\cr & & *+[F]{\txt{Word}}\ar[dd] & & \cr\cr & & *+[F]{\txt{Pair}}\ar[dd] & & \cr\cr & & *+[F]{\txt{VocItem}}& & } \caption{The structure of the lower level of the Student Dictionary System} \end{figure} Apart from the vocabulary system $vocsystem$ there are two other important sorts for the user. These are the sorts $testnativevocsystem$ and $testforeignvocsystem$ that represent the test suites a user can construct to test his knowledge of a given language. These two sorts basically consist out of a list of words (either native or foreign) and two integers. These integers represent the score of the user when he goes through the test. This concludes the basic idea which lies behind the loose specification. Let us now have a look at the detailed operations of the specification. Doing this, we will adopt a bottom-up approach to the problem, although the actual design of the specification happened more or less top down. Working bottom-up, however, allows us to build up the dictionary from scratch. \section{Tools for the Weary: Lists and Boolean} Throughout the rest of the construction of our specification, we will often use sorts that are only slight modifications of the basic list sort. For this purpose we provide the basic list in this section. First of all, we need the notion of an element. An element can be any arbitrary object at this point, so its loose specification only contains a type, and no operations or axioms. This sort only serves as a placeholder and will be replaced by more explicit sorts when we will use the list type constructed in this section in order to create more elaborate sorts needed at a higher level in the student dictionary system. The loose specification for the sort element becomes: \begin{spec}{ElementSpec} \item type element \end{spec} The fact that the sort element we just introduced is a placeholder becomes clearer when we take a look at the first list sort we create, in the specification \textit{SimpleListSpec}. This specification contains the standard list as we all know it from computer science, extended with operations that allow us to get the first element of the list or remove the first element from the list (Head resp.\ Tail), concatenate lists (\_.\_), check whether an element belongs to a list or not ($\in$) and tell us the length of a list (Length). For these last two operations, we need to import the boolean values and the integers into this specification, as can be seen in the import section of the specification \textit{SimpleListSpec} given below. \begin{spec}{SimpleListSpec(E: ElementSpec)} \item import E, BoolSpec, IntegerSpec \item freely generated type list \item \begin{opns} \item constr \opE{\emptyL}{list} \item constr \opII{AddToSimpleList}{element}{list}{list} \item \opI{[$\_$]}{element}{list} \item \opI{Head}{list}{element} \item \opI{Tail}{list}{list} \item \opII{\_.\_}{list}{list}{list} \item \opII{\_$\in$\_}{element}{list}{boolean} \item \opI{Length}{list}{int} \end{opns} \begin{vars} \item l,m,n: list \item e:element \end{vars} \begin{axioms} \item Head(AddToSimpleList(e,l))=e \item Tail(AddToSimleList(e,l))=l \item {[e]}=AddToSimpleList(e,\emptyL) \item \emptyL.l=l \item AddToSimpleList(e,l).m=AddToSimpleList(e,l.m) \item e$\in$l={\bf If} $\exists$ m,n: (l=m.[e].n) \item\hspace*{0.8cm} {\bf then} True {\bf else} False \item Length(\emptyL)=0 \item Length(AddToSimpleList(e,l))=Succ(Length(l)) \end{axioms} \end{spec} This first specification of list will now be extended to a list that does not contain the same element twice. In order to create this list sort out of the previous sort we only have to provide one additional operation, taking the role of AddToSimpleList in the previous specification. This operation, named AddToList, only adds an element to a list if this element was not in the list before, as is seen in the axioms of the specification \textit{ListSpec} given below. \begin{spec}{ListSpec(E: ElementSpec)} \item extends SimpleListSpec(E) by \item \begin{opns} \item\opII{AddToList}{element}{list}{list} \end{opns} \item \begin{vars} \item e:element \item l:list \end{vars} \item \begin{axioms} \item AddToList(e,l)= \item\hspace*{0.5cm}{\bf If} $e\in l$ {\bf then } l {\bf else} AddToSimpleList(e,l) \end{axioms} \end{spec} It is now clear from the previous specifications that the boolean values play an important role in this specification, as they allow us to check (among other things) whether elements are in a list or not, so we provide them in the next specification: \begin{spec}{BooleanSpec} \item freely generated type boolean \item \begin{opns} \item constr \opE{True}{boolean} \item constr \opE{False}{boolean} \end{opns} \end{spec} \section{Clay for the Bricks: Characters and Character Ordering} The very basic components of our (written) language are of course the characters making up the language. We introduce the characters here in the specification \textit{CharacterSpec} as a freely generated sort containing only constants. \begin{spec}{CharacterSpec} \item freely generated type char \item \begin{opns} \item constr \opE{a}{char} \item constr \opE{b}{char} \item[]$\vdots$ \end{opns} \end{spec} Closely linked to the characters is of course the alphabet, which simply lists all possible characters in a certain order. This order is then later on used to order words made up of these characters. This ordered list of characters is the sort we call $charorder$ and is simply a list of characters where we renamed some sorts and operation and added the operation $IsCharSmaller$ representing the order of the characters. So it is really an alphabet in the sense that it contains all characters and has an ordering on these characters. The modification of the sort $list$ to the sort $charorder$ is done in the specification \textit{CharacterOrderSimpleSpec}: \begin{spec}{CharacterOrderSimpleSpec} \item import ListSpec(CharacterSpec \{element $\to$ char\}) by renaming \begin{itemize} \item list to charorder \item AddToList to AddToOrder \item AddToSimpleList to NewChar \end{itemize} \end{spec} The specification \textit{CharacterOrderSimpleSpec} is then extended with an ordering, represented by the operation $IsCharSmaller$, in the specification \textit{CharacterOrderSpec}. This operation simply tell us that the characters appear in ascending order in the list containing all characters. Note that we can do this since the list sort we use cannot contain the same element twice. \begin{spec}{CharacterOrderSpec} \item import BoolSpec \item extends CharacterOrderSimpleSpec by \item \begin{opns} \item \opIII{IsCharSmaller}{char}{char}{charorder}{boolean} \end{opns} \begin{vars} \item c1,c2: char \item co,co1,co2,co3: charorder \end{vars} \begin{axioms} \item IsCharSmaller(c1,c2,co)= \item\hspace*{1cm} {\bf If} $\exists$ co1,co2,co3: (co1.[c1].co2.[c2].co3=co) \item\hspace*{2cm} {\bf then} True {\bf else} False \end{axioms} \end{spec} \section{Baking the Bricks: Strings and Rules} The next step in the construction of the language is glueing together characters to form strings, and telling which combinations cannot occur. For specifying strings, we make use of the earlier introduced sorts $list$ and $charorder$. We begin by stating that basically a string is nothing else but a simple list of characters (where simple list means that we allow multiple occurences of the same character). This statement is formalized in the specification \textit{SimpleStringSpec}. \begin{spec}{SimpleStringSpec} \item import SimpleListSpec(CharacterSpec \{element $\to$ char\}) by renaming \begin{itemize} \item list to string \item \emptyL to $\epsilon$ \item AddToSimpleList to AddToString \end{itemize} \end{spec} However, instead of simply stating that a string is a list of characters, we provide additional operations that represent the basic notion of alphabetical ordering. For this purpose we provide the operation $IsStringSmaller$. We also provide an additional operation that will be used later on in the specification to change a string into a correctly spelled word. This operation, $CheckAlphabet$, checks whether a given string is written in a correct alphabet. There is also an error operation which is used later on (on a higher level) in the specification. This extension is done in the specification \textit{StringSpec}. \begin{spec}{StringSpec} \item imports CharacterOrderSpec \item extends SimpleString by \item \begin{opns} \item\opE{Error\_NoStringLeft}{string} \item\opIII{IsStringSmaller}{string}{string}{charorder}{boolean} \item\opII{CheckAlphabet}{string}{charorder}{boolean} \end{opns} \item \begin{vars} \item s1,s2:string \item c:char \item co:charorder \end{vars} \item \begin{axioms} \item IsStringSmaller(s1,s2,co)= \item\hspace*{1cm} {\bf If} s1=$\epsilon$ {\bf then} True \item\hspace*{1.5cm} {\bf else} \item\hspace*{2cm} {\bf If} s2=$\epsilon$ {\bf then} False \item\hspace*{2.5cm} {\bf else} \item\hspace*{3cm} {\bf If} Head(s1)=Head(s2) \item\hspace*{3.5cm} {\bf then} IsStringSmaller(Tail(s1),Tail(s2),co) \item\hspace*{3.5cm} {\bf else} IsCharacterSmaller(Head(s1),Head(s2)) \item \item CheckAlphabet($\epsilon$,co)=False \item CheckAlphabet(AddToString(c,$\epsilon$))= \item\hspace*{1cm} {\bf If} $c\in co$ {\bf then} True {\bf else} False \item CheckAlphabet(AddToString(c,s1),co)= \item\hspace*{1cm} {\bf If} $c\in co$ \item\hspace*{1.5cm} {\bf then} CheckAlphabet(s1,co) {\bf else} False \end{axioms} \end{spec} As we stated earlier in this paper, we also introduce lexicographical rules in order to check whether certain typing mistakes occured when entering a word. We introduce these rules once again through the extension of the sort list. Basically, the lexicographical rules are a list of strings, as is seen in the specification \textit{SimpleRuleSpec}. \begin{spec}{SimpleRuleSpec} \item import ListSpec(StringSpec \{element $\to$ string\}) by renaming \item \begin{itemize} \item list to rules \item AddToList to AddToRules \item AddToSimpleList to NewRule \end{itemize} \end{spec} The strings in a list of lexicographical rules represent sequences of characters that cannot occur in the language the lexicographical rules cover. We will need to be able to check whether a given string contains such a misspelling, so we provide the operation $MatchRule$ to check for these typing mistakes in the specification \textit{RuleSpec}. \begin{spec}{RuleSpec} \item extends SimpleRuleSpec by \item \begin{opns} \item \opII{MatchRule}{string}{rule}{boolean} \end{opns} \item \begin{vars} \item s,s1,s2:string \item R:rules \end{vars} \item \begin{axioms} \item MatchRule(s,R)= \item\hspace*{0.5cm}{\bf If} R=\emptyL {\bf then} False \item\hspace*{1cm}{\bf else} \item\hspace*{1.5cm}{\bf If} $\exists$ s1,s2: (s1.[Head(R)].s2=s) {\bf then} True \item\hspace*{2cm}{\bf else} MatchRule(s,Tail(R)) \end{axioms} \end{spec} \section{Bricks to Build With: Word and Language} Now that we have an alphabet and rules, we basically have all the ingredients for a language. The notion of language that we will use is simply a couple of an alphabet and rules. This is seen in the specification \textit{LanguageSpec} (containing also operations to extract the lexicographic rules and the characters out of a given language). \begin{spec}{LanguageSpec} \item import RuleSpec, CharacterOrderSpec \item freely generated type language \item \begin{opns} \item constr \opII{MakeLanguage}{rules}{charorder}{language} \item\opI{GetRules}{language}{rules} \item\opI{GetCharacterOrder}{language}{charorder} \end{opns} \item \begin{vars} \item co:charorder \item r:rules \end{vars} \item \begin{axioms} \item GetRules(MakeLanguage(r,co))=r \item GetCharacterOrder(MakeLanguage(r,co))=co \end{axioms} \end{spec} This language is now used to make correctly spelled words. Up until now, we only had sequences of characters and the possibility to order them. In our dictionary, however, we want to work with correctly spelled words, so we combine the means we have for spelling checking with the means we have for making strings. This results in the sort $word$. This sort is basically a couple consisting out of a string and a language and checks whether the given string is correctly spelled in the given language, using the operations $MatchRules$ and $CheckAlphabet$. \begin{spec}{WordSpec} \item freely generated type word \item import StringSpec, LanguageSpec \item \begin{opns} \item\opII{MakeWord}{string}{language}{word} \item constr \opI{CorrectWord}{string}{word} \item constr \opE{Error\_Misspelled}{word} \item constr \opE{Error\_NoWordLeft}{word} \item constr \opE{DummyValue}{word} \item\opI{GetString}{word}{string} \end{opns} \item \begin{vars} \item s:string \item l:language \end{vars} \item \begin{axioms} \item GetString(CorrectWord(s))=s \item GetString(Error\_NoWordLeft)=Error\_NoWordLeft \item MakeWord(s,l)= \item\hspace*{0.5cm}{\bf If} MatchRule(s,GetRules(l))=False \&\& \item\hspace*{0.9cm}CheckAlphabet(s,GetCharacterOrder(l))=True \item\hspace*{1.3cm} {\bf then} CorrectWord(s) {\bf else} Error\_Misspelled \end{axioms} \end{spec} GetString(Error\_Misspelled) is intentionally left unspecified. \section{Laying the Foundation: Pair, PairList and ListOfPairList} A dictionary consists out of pairs of words, representing a word in a given language and its translation into another given language. For this purpose, we have to introduce the concept of pairs and lists of pairs, as is seen below. \begin{spec}{PairSpec} \item freely generated type pair \item import WordSpec, StringSpec \item \begin{opns} \item constr \opII{MakePair}{word}{word}{pair} \item \opI{GetNative}{pair}{string} \item \opI{GetForeign}{pair}{string} \end{opns} \item \begin{hopns} \item\opII{CheckWords}{word}{word}{boolean} \end{hopns} \item \begin{vars} \item n,f: word \item p: pair \end{vars} \item \begin{axioms} \item CheckWords(n,f)= \item\hspace*{0.2cm}{\bf If} n=!=Error\_Misspelled \&\& f=!=Error\_Misspelled \item\hspace*{0.4cm} {\bf then} True {\bf else} False \item \item GetNative(MakePair(n,f))= \item\hspace*{0.2cm} {\bf If} CheckWords(n,f)=True {\bf then} GetString(n) \item GetForeign(MakePair(n,f))= \item\hspace*{0.2cm} {\bf If} CheckWords(n,f)=True {\bf then} GetString(f) \end{axioms} \end{spec} It is clear from this specification that a pair is simply a couple of words, the first element of this couple is called the native word whereas the second element is called the foreign word. We also provide an operation to check whether the pair contains the error message introduced in the word specification. \begin{spec}{PairListSpec} \item import ListSpec(PairSpec \{element $\to$ pair\}) by renaming \item \begin{itemize} \item list to pairlist \item AddToList to AddPair \end{itemize} \end{spec} Once again, we use the specification for a list, introduced earlier on in this paper, to create list of pairs, as is seen in the specification \textit{PairListSpec}. Of course one word can have many different translations, and it is useful to group all these translations. If the user then wants to see the entire dictionary, he is returned a list of these groups. For this purpose we introduce a list of a list of pairs, again using the list specification introduced earlier. \begin{spec}{ListOfPairListsSpec} \item import ListSpec(PairListSpec \{element $\to$ pairlist\}) by renaming \item \begin{itemize} \item list to listofpairlists \item AddToList to AddPairList \item AddToSimpleList to NewPair \end{itemize} \end{spec} \section{A Skeleton Arises: VocItem and ListOfVocItem} Our ultimate goal is to construct test suites out of a given dictionary. This means we have to select several entries out of the dictionary, which we use to test the user. Of course we do not want to ask the user the same question several times, so we have to indicate whether a certain entry has been chosen or not. For this purpose, our dictionary does not simply contain pairs of words, but contains so-called vocabulary items. These $vocitem$s contain in addition to a pair also a boolean flag, which is set to true if the pair is in the testsuite that is generated. These vocitems are introduced in the \textit{VocItemSpec} specification below. \begin{spec}{VocItemSpec} \item freely generated type vocitem \item import PairSpec \item \begin{opns} \item constr \opII{MakeItem}{pair}{boolean}{vocitem} \item\opI{GetPair}{vocitem}{pair} \item\opI{GetFlag}{vocitem}{boolean} \end{opns} \item \begin{vars} \item vi:vocitem \item p:pair \item f:boolean \end{vars} \item \begin{axioms} \item GetFlag(MakeItem(p,f))=f \item GetPair(MakeItem(p,f))=p \end{axioms} \end{spec} Of course our dictionary will then contain a list of these vocabulary items, specified in the \textit{ListOfItemsSpec} specification below. \begin{spec}{ListOfItemsSpec} \item import ListSpec(VocItemSpec \{element $\to$ vocitem\}) by renaming \item \begin{itemize} \item list to listofitems \item AddToList to AddItem \item AddToSimpleList to NewItem \end{itemize} \end{spec} For the user-interface we will also need data types which are specified in the following. \begin{spec}{ListOfStringsSpec} \item import ListSpec(StringSpec \{element $\to$ String\}) by renaming \item \begin{itemize} \item list to listofstrings \item AddToList to AddString \item AddToSimpleList to NewString \end{itemize} \end{spec} \begin{spec}{ListOfStringListSpec} \item import ListSpec(ListOfStringsSpec \{element $\to$ listofstrings\}) by renaming \item \begin{itemize} \item list to listofstringlist \item AddToList to AddStringList \item AddToSimpleList to NewStringList \end{itemize} \end{spec} \begin{spec}{ListOfListOfItemsSpec} \item import ListSpec(ListOfItmesSpec \{element $\to$ listofitems\}) by renaming \item \begin{itemize} \item list to listoflistofitems \item AddToList to AddToItemListsList \item AddToSimpleList to NewStringListsList \end{itemize} \end{spec} \section{A Dictionary Has Been Built: DictionarySpec} We now have introduced all the basics we need to create the core of our student dictionary, namely the vocabulary system. The essence of this sort is that it consists out of a couple of languages and a list of vocabulary items. In addition to this, we provide all operations that are nescessary to build this dictionary from scratch and operations that provide us with information on the current dictionary. \begin{spec}{DictionarySpec} \item freely generated type vocsystem \item import ListOfItemsSpec \item \begin{opns} \item constr \opIII{Dictionary}{language}{language}{listofitems}{vocsytem} \item constr \opE{Error\_NativeWordIsMisspelled}{vocsystem} \item constr \opE{Error\_ForeignWordIsMisspelled}{vocsystem} \item \item\opIII{AddEntryToDictionary}{string}{string}{vocsystem}{vocsystem} \item\opIII{DeleteEntryFromDictionary}{string}{string}{vocsystem}{vocsystem} \item \item\opI{GetNativeLanguage}{vocsystem}{language} \item\opI{GetForeignLanguage}{vocsystem}{language} \item\opI{GetItemList}{vocsystem}{listofitems} \item\opI{RandomVocItem}{vocsystem}{vocitem} \item\opI{ResetFlags}{vocsystem}{vocsystem} \item\opII{ResetFlagsRec}{listofitems}{listofitems}{listofitems} \item\opII{SetVocItemFlag}{vocitem}{boolean}{vocitem} \item\opII{SetNativeFlags}{word}{vocsystem}{vocsystem} \item\opIII{SetNativeFlagsRec}{word}{listofitems}{listofitems}{listofitems} \item\opII{SetForeignFlags}{word}{vocsystem}{vocsystem} \item\opIII{SetForeignFlagsRec}{word}{listofitems}{listofitems}{listofitems} \item \item\opII{TranslateIntoNative}{string}{vocsystem}{listofitems} \item\opIII{TranslateIntoNativeRec}{string}{listofitems}{listofitems}{listofitems} \item\opII{TranslateIntoForeign}{string}{vocsystem}{listofitems} \item\opIII{TranslateIntoForeignRec}{string}{listofitems}{listofitems}{listofitems} \end{opns} \item \begin{vars} \item l1,l2: language \item s1,s2,s: string \item il,output: listofitems \item vi: vocitem \item voc: vocsystem \item $w_1$,$w_2$,w: word \item b: Bool \end{vars} \item \begin{axioms} %\item GenerateDictionary(l1,l2) = %\item\hspace*{0.2cm} {\bf If} l1 $\neq$ l2 {\bf then} Dictionary(l1,l2,[]) %\item\hspace*{0.2cm} else ERROR\_IdenticalLanguages %\item AddEntry(s1,s2,voc) = AddEntryDictionary(voc,s1,s2) \item GetNativeLanguage(Dictionary(l1,l2,il))=l1 \item GetForeignLanguage(Dictionary(l1,l2,il))=l2 \item GetItemList(Dictionary(l1,l2,li))=il \item \item AddEntryToDictionary(s1,s2,voc) = \item\hspace*{0.2cm} {\bf Let} $w_1$:= MakeWord(s1,GetNativeLanguage(voc)); \item\hspace*{0.2cm} {\bf Let} $w_2$:= MakeWord(s2,GetForeignLanguage(voc)); \item\hspace*{0.2cm} {\bf If} $w_1$=Error\_Misspelled \item\hspace*{0.4cm} {\bf then} Error\_NativeWordIsMisspelled \item\hspace*{0.6cm} {\bf If} $w_2$=Error\_Misspelled \item\hspace*{0.8cm} {\bf then} Error\_ForeignWordIsMisspelled \item\hspace*{0.8cm} {\bf else} \item\hspace*{1cm} Dictionary(GetNativeLanguage(voc), GetForeignLanguage(voc), \item\hspace*{1.2cm} AddItem(MakeItem(MakePair($w_1$,$w_2$),False),GetItemList(voc))) \item \item DeleteEntryFromDictionary(s1,s2,Dictionary(l1,l2,\emptyL)) = \item \hspace*{0.2cm} Dictionary(l1,l2,\emptyL) \item DeleteEntryFromDictionary(s1,s2,Dictionary(l1,l2,AddItem(vi,il))) = \item\hspace*{0.2cm} {\bf If} s1 = s1 and s2 = s2 {\bf then} Dictionary(l1,l2,il)) \item\hspace*{0.2cm} else \item\hspace*{0.4cm} AddEntryToDictionary(GetNative(GetPair(vi)), GetForeign(GetPair(vi)), \item\hspace*{0.6cm} DeleteEntryFromDictionary(s1,s2,Dictionary(l1,l2,il)) \item \item SetVocItemFlag(vi,b) = MakeItem(GetPair(vi),b) \item \item SetNativeFlags($w$,voc) = \item\hspace*{0.2cm} Dictionary(GetNativeLanguage(voc), GetForeignLanguage(voc), \item\hspace*{0.4cm} SetNativeFlagsRec($w$,GetItemList(voc),\emptyL)) \item {\sf SetForeignFlags is analogeous.} \item \item SetNativeFlagRec($w$,il,output) = \item\hspace*{0.2cm} {\bf If} il = \emptyL {\bf then} output \item\hspace*{0.2cm} else \item\hspace*{0.4cm} {\bf Let} hdvcitm:= Head(il) \item\hspace*{0.4cm} {\bf If} GetNative(GetPair(hdvcitm)) = GetString($w$) {\bf then} \item\hspace*{0.6cm} SetNativeFlagsRec($w$,Tail(il), AddItem(SetVocItemFlag(hdvcitm),true),output) \item\hspace*{0.4cm} else \item\hspace*{0.6cm} SetNativeFlagsRec($w$,Tail(il),AddItem(il,output)) \item {\sf SetForeignFlagRec is analogeous.} \item \item ResetFlagsRec(il,output) = \item\hspace*{0.2cm} {\bf If} il = emptyL {\bf then} \item\hspace*{0.4cm} output \item\hspace*{0.2cm} else \item\hspace*{0.4cm} {\bf Let} hdvcitm := Head(il) \item\hspace*{0.4cm} ResetFlagsRec(Tail(il), AddItem(SetVocItemFlag(hdvcitm,False),output)) \item ResetFlags(voc) = \item \hspace*{0.2cm} Dictionary(GetNativeLanguage(voc), GetForeignLanguage(voc), \item\hspace*{0.4cm} ResetFlagsRec(GetItemList(voc),\emptyL)) \item \item RandomVocItem(voc)= \item\hspace*{0.4cm} {\bf If} $\exists p\in$ GetItemList(voc): (GetFlag(p)=0) \item\hspace*{0.6cm} {\bf then} \item\hspace*{0.8cm} ``Take randomly'' p: GetFlag(p)=0 \item\hspace*{0.8cm} MakeItem(p,*) \item\hspace*{0.6cm} {\bf else} Error\_OutOfEntries \item \item \item TranslateIntoNativeRec(s,il,output) = \item \hspace*{0.2cm} {\bf If} il $=$ \emptyL\ {\bf then} output \item \hspace*{0.2cm} {\bf else} \item\hspace*{0.4cm} {\bf Let} foreignstr := GetForeign(GetPair(Head(il))) \item\hspace*{0.4cm} {\bf If} foreignstr = s {\bf then} \item\hspace*{0.6cm} TranslateIntoNativeRec(s, Tail(il),AddItem(Head(il),output)) \item\hspace*{0.4cm} else \item\hspace*{0.6cm} TranslateIntoNativeRec(s, Tail(il),output) \item {\sf TranslateIntoForeignRec is analogeous.} \item \item TranslateIntoNative(s,voc) = \item\hspace*{0.2cm} TranslateIntoNativeRec(s,GetItemList(voc),\emptyL) \item {\sf TranslateIntoForeign is analogeous.} \end{axioms} \end{spec} * is a dummy value and can be either True or False. ResetFlags is not specified yet. In this specification, we provided operations to extract the languages and the list of vocabulary items from a given vocabulary system; these are the operations $GetNativeLanguage$, $GetForeignLanguage$ and $GetItemList$. We also provided operations to add entries to a dictionary ($AddEntryToDictionary$), to translate a given string, representing either a native or a foreign word ($TranslateIntoForeign$ resp.\ $TranslateIntoNative$), as well as operations for more internal use whose purpose it is to set or reset the flags of vocabulary items ($SetVocItemFlag$ resp. $ResetFlags$). We also provide constants for error checking ($Error\_NativeWordIsMisspelled$ and $Error\_ForeignWordIsMisspelled$). \section{Framework: NativeVocSystem and TestNativeVocSystem} The basic dictionary that we have built is now used to generate a test suite so that the user can test his knowledge of the language. The construction of this test suite is done in two steps. First of all, we construct a sort that is called $nativevocsystem$ (resp. $foreignvocsystem$). This is nothing else but a list of native (resp. $foreign$) words, extracted from a given vocubulary system. Apart from the constructors for this sort and some error handling, an operation $GenerateNativeVocSystem$ is provided, with arity $vocsystem\times int$. This operation is used to generate a $nativevocsystem$ with $n$ entries, where $n$ is the given integer. This operation will later on be used for the generation of a test suite with a user defined number of questions. The other operation which is of importance for the generation of the test suite is the operation $CountMaximumNativeScore$. This operation counts the total amount of possible translations for every word in the $nativevocsystem$ and adds these numbers together to get the final maximal score. These sorts with their operations are specified in \textit{PreTestVocSystemSpec}. \begin{spec}{PreTestVocSystemSpec} \item freely generated type NativeVocSystem \item import DictionarySpec \item import ListOfListOfItemsSpec \item import IntSpec \item \begin{opns} \item constr \opI{NewNativeVocSytem}{vocsystem}{nativevocsytem} \item constr \opII{AddEntryToNativeVocSystem}{word}{nativevocsystem}{nativevocsystem} \item \item constr \opE{ERROR\_NativeVocExceedsVoc}{nativevocsystem} \item constr \opE{ErrorNoEntriesLeft}{nativevocsystem} \item \item \opII{\_In\_}{word}{nativevocsystem}{boolean} \item \opII{AddToNativeVoc}{word}{nativevocsystem}{nativevocsystem} \item \opII{DeleteNativeEntry}{word}{nativevocsystem}{nativevocsystem} \item\opI{GetVocSystem}{nativevocsystem}{vocsystem} \item \item\opIII{RecGenerateNativeVocSystem}{nativevocsystem}{int}{vocsystem}{nativevocsystem} \item\opII{GenerateNativeVocSystem}{vocsystem}{int}{nativevocsystem} \item \item\opI{GetNativeHead}{nativevocsystem}{word} \item \item\opI{GetNativeTail}{nativevocsystem}{nativevocsystem} \item \item\opI{MaxNativeScore}{nativevocsystem}{nat} \item\opII{GetMaxNative}{nativevocsystem}{word}{word} \item\opII{GetNativeTranslationList}{nativevocsystem}{listoflistofitems}{listoflistofitems} \item\opII{GetOrderedNativeWordList}{nativevocsystem}{nativevocsystem}{nativevocsystem} \item\opII{GetNativeOrderedItemList}{nativevocsystem}{listoflistofitems}{listoflistofitems} \item\opII{GetListOfNativeWords}{vocsystem}{vocsystem}{nativevocsystem} \item constr \opI{NewForeignVocSytem}{vocsystem}{foreignvocsytem} \item constr \opII{AddEntryToForeignVocSystem}{word}{foreignvocsystem}{foreignvocsystem} \item \item constr \opE{ERROR\_ForeignVocExceedsVoc}{foreignvocsystem} \item constr \opE{ErrorNoEntriesLeft}{foreignvocsystem} \item \item \opII{\_In\_}{word}{foreignvocsystem}{boolean} \item \opII{AddToForeignVoc}{word}{foreignvocsystem}{foreignvocsystem} \item \opII{DeleteForeignEntry}{word}{foreignvocsystem}{foreignvocsystem} \item\opI{GetVocSystem}{foreignvocsystem}{vocsystem} \item \item\opIII{RecGenerateForeignVocSystem}{foreignvocsystem}{int}{vocsystem}{foreignvocsystem} \item\opII{GenerateForeignVocSystem}{vocsystem}{int}{foreignvocsystem} \item \item\opI{GetForeignHead}{foreignvocsystem}{word} \item \item\opI{GetForeignTail}{foreignvocsystem}{foreignvocsystem} \item \item\opI{MaxForeignScore}{foreignvocsystem}{nat} \item\opII{GetMaxForeign}{foreignvocsystem}{word}{word} \item\opII{GetForeignTranslationList}{foreignvocsystem}{listoflistofitems}{listoflistofitems} \item\opII{GetOrderedForeignWordList}{foreignvocsystem}{foreignvocsystem}{foreignvocsystem} \item\opII{GetForeignOrderedItemList}{foreignvocsystem}{listoflistofitems}{listoflistofitems} \item\opII{GetListOfForeignWords}{vocsystem}{vocsystem}{foreignvocsystem} \end{opns} \begin{vars} \item ntvoc:nativevocsystem \item size:int \item voc:vocsystem \item it:vocitem \item itlst: listofitems \item w,v,output:word \item lstlstit: listoflistofitems \item l1,l2: language \end{vars} \begin{axioms} \item GetVocSystem(NewNativeVocSystem(voc)) = voc \item \item GetVocSystem(AddEntryToNativeVocSystem(w,ntvoc))= \item\hspace*{0.2cm}GetVocSystem(ntvoc) \item \item DeleteNativeEntry(w,NewNativeVocSystem(voc)) = \item\hspace*{0.2cm}NewNativeVocSystem(voc) \item DeleteNativeEntry(w,AddEntryToNativeVocSystem(v,ntvoc)) = \item\hspace*{0.2cm} {\bf If} w = v {\bf then} ntvoc \item\hspace*{0.4cm} {\bf else} AddEntryToNativeVocSystem(v,DeleteNativeEntry(w,ntvoc)) \item AddToNativeVoc(w,ntvoc)= \item \hspace*{0.2cm}{\bf If} (w In ntvoc) {\bf then} ntvoc \item \hspace*{0.4cm} {\bf else} AddEntryToNativeVocSystem(w,ntvoc) \item \item (w In NewNativeVocSystem(voc)) = False \item (w In AddEntryToNativeVocSystem(v,nativevoc)) = \item\hspace*{0.2cm} {\bf If} w = v {\bf then} True {\bf else} (w In ntvoc) \item \item RecGenerateNativeVocSystem(ntvoc,size,voc) = \item\hspace*{0.2cm}{\bf Let} vcitm := RandomVocItem(voc) \item\hspace*{0.2cm}{\bf if} vcitm = ERROR\_OutOfEntries \item\hspace*{0.4cm}{\bf then} \item\hspace*{0.6cm} {\bf If} size=0 {\bf then} ntvoc {\bf else} ERROR\_NativeVocExcedsVoc \item\hspace*{0.4cm}{\bf else} \item\hspace*{0.6cm} {\bf If} size=0 {\bf then} ntvoc {\bf else} \item\hspace*{0.8cm}{\bf Let} nextntvoc := \item\hspace*{1cm} SetNativeFlags(CorrectWord(GetNative(vcitm)),voc) \item\hspace*{0.8cm}RecGenerateNativeVocSystem( \item\hspace*{1cm} AddEntryToNativeVocSystem( \item\hspace*{1.2cm} CorrectWord(GetNative(GetPair(vcitm))),ntvocsys), \item\hspace*{1cm} size-1,nextntvoc) \item GenerateNativeVocSystem(voc,size) = \item\hspace*{0.2cm}RecGenerateNativeVocSystem(NewNativeVocSystem(voc),size,voc) \item \item GetNativeHead(NewNativeVocSystem(voc))=ERROR\_NoWordLeft \item GetNativeHead(AddEntryToNativeVocSystem(w,ntvoc)=w \item GetNativeTail(NewNativeVocSystem(voc))=ERROR\_NoEntriesLeft \item GetNativeTail(AddEntryToNativeVocSystem(w,ntvoc)=ntvoc \item \item MaxNativeScore(NewNativeVocSystem(voc)) = 0 \item MaxNativeScore(AddEntryToNativeVocSystem(w,ntvoc)) = \item\hspace*{0.2cm} {\bf Let} voc := GetVocSystem(ntvoc) \item\hspace*{0.2cm} MaxNativeScore(ntvoc) + \item\hspace*{0.2cm} Length(TranslateIntoForeign(GetString(w),voc)) \item %\item GetListofNativeWords(GenerateDictionary(\dots))=\emptyL %\item %\item GetListofNativeWords(AddEntry(str1,str2,voc)) = %\item AddEntryToListofNative(str1,GetListofNativeWords(voc)) %\item \item GetMaxNative(NewNativeVocSystem(voc),output) = output \item GetMaxNative( \item\hspace*{0.2cm} AddEntryToNativeVocSystem(w,NewNativeVocSystem(voc)), \item \hspace*{0.2cm} output) = \item\hspace*{0.2cm} {\bf If} output=DummyValue {\bf then} w {\bf else} output \item GetMaxNative(ntvoc,output) = \item\hspace*{0.2cm} {\bf Let} first := GetNativeHead(ntvoc) \item\hspace*{0.2cm} {\bf Let} second := GetNativeHead(GetNativeTail(ntvoc)) \item\hspace*{0.2cm} {\bf If} not GetNativeHead(ntvoc) = ErrorNoWordLeft and \item\hspace*{0.6cm} not GetNativeTail(GetNativeTail(ntvoc)) = ErrorNoEntriesLeft \item \hspace*{0.4cm} {\bf If} IsStringSmaller(GetString(first),GetString(second)) {\bf then} \item\hspace*{0.6cm} GetMaxNative(GetNativeTail(ntvoc)) \item \hspace*{0.4cm} {\bf else} \item\hspace*{0.6cm} GetMaxNative( \item\hspace*{0.8cm} AddEntryToNativeVocSystem(first,GetNativeTail(ntvoc)), \item\hspace*{0.8cm} first) \item \item GetOrderedNativeWordList(ntvoc,ntout) = \item\hspace*{0.2cm} {\bf If} GetNativeHead(ntvoc) == ErrorNoWordLeft {\bf then} ntout \item\hspace*{0.2cm} {\bf else} \item\hspace*{0.4cm} {\bf Let} max := GetMaxNative(ntvoc,DummyValue) \item\hspace*{0.4cm} GetOrderedNativeWordList(DeleteNativeEntry(max,ntvoc)), \item\hspace*{0.4cm} AddEntryToNativeVocSystem(max,ntout)) \item \item GetNativeTranslationList(NewNativeVocSystem(voc),lstlstit) = \item\hspace*{0.2cm} lstlstit \item GetNativeTranslationList( \item\hspace*{0.2cm}AddEntryToNativeVocSystem(w,ntvoc),lstlistit) = \item\hspace*{0.4cm} GetNativeTranslationList(ntvoc, \item\hspace*{0.6cm} AddToItemListsList( \item\hspace*{0.8cm} TranslateIntoForeign(GetString(w), GetVocSystem(ntvoc)), \item\hspace*{0.6cm} lstlstit)) \item \item GetNativeOrderedItemList(nativevoc,lstlstit) = \item\hspace*{0.2cm} GetNativeTranslationList( \item\hspace*{0.4cm} GetOrderedNativeWordList(nativevoc, \item\hspace*{0.6cm} NewNativeVocSystem(GetVocSystem(nativevoc))),lstlstit) \item GetListOfNativeWords(Dictionary(l1,l2,\emptyL),voc) = \item\hspace*{0.2cm} NativeVocSystem(voc) \item GetListOfNativeWords(Dictionary(l1,l2,NewItem(it,itlst)),voc) = \item \hspace*{0.2cm}AddToNativeVoc( \item\hspace*{0.4cm} CorrectWord(GetNative(GetPair(it))), \item \hspace*{0.4cm} GetListOfNativeWords(Dictionary(l1,l2,itlst),voc)) \item \item {\sf The axioms of the operations for the foreign case are analogeous to the native case.} \end{axioms} \end{spec} These sorts, $nativevocsystem$ and $foreignvocsystem$, are then used to construct the actual test suite. This test suite is specified in the sorts $testnativevocsystem$ and $testforeignvocsystem$, and is actually nothing else than a $nativevocsystem$ (resp. a $foreignvocsystem$) and an integer, where this integer represents the actual score of the user. This sort is seen in \textit{TestVocSystemSpec}. \begin{spec}{TestVocSystemSpec} \item \begin{opns} \item constr \opII{GenerateNativeTest}{nativevocsystem}{Int}{testnativevocsystem} \item\opI{GetNativeWord}{testnativevocsystem}{word} \item\opI{GetMaxNativeScore}{testnativevocsystem}{Nat} \item\opI{GetNativeScore}{testnativevocsystem}{Int} \item\opI{GetNativeVocSystem}{testnativevocsystem}{nativevocsytem} \item\opII{AdaptNativeVocSysyetm}{string}{testnativevocsystem}{testnativevocsystem} \item\opII{GetnativeStringList}{listofitems}{listofstrings}{listofstrings} \item \item constr \opII{GenerateForeignTest}{foreignvocsystem}{Int}{testforeignvocsystem} \item\opI{GetForeignWord}{testforeignvocsystem}{word} \item\opI{GetMaxForeignScore}{testforeignvocsystem}{Nat} \item\opI{GetForeignScore}{testforeignvocsystem}{Int} \item\opI{GetForeignVocSystem}{testforeignvocsystem}{foreignvocsytem} \item\opII{AdaptForeignVocSystem}{string}{testforeignvocsystem}{testforeignvocsystem} \item\opII{GetforeignStringList}{listofitems}{listofstrings}{listofstring} \item \item\opII{GetPairList}{listofitems}{pairlist}{pairlist} \item\opII{GetListofPairLists}{listoflistofites}{listofpairlists}{listofpairlists} \item \end{opns} \begin{vars} \item tnvoc : testnativevocsystem \item tfvoc : testforeignvocsystem \item fvoc : foreignvocsystem \item pos : Nat \item score : Int \item str : string \item vit : vocitem \item ilst : listofitems \item illst : listoflistofitems \item sllst : listofpairlists \item slst : listofstrings \item plst : pairlist \end{vars} \begin{axioms} \item \item GetNativeVocSystem(GenerateNativeTest(nvoc,score) = nvoc \item \item GetMaxNativeScore(GenerateNativeTest(nvoc,score)) = MaxNativeScore(nvoc) \item \item GetNativeWord(tnvoc) = GetNativeHead(GetNativeVocSystem(tnvoc)) \item \item AdaptNativeVocSystem(str,tnvoc) = \item\hspace*{0.2cm} {\bf if} MakeWord(str,GetForeignLanguage( \item\hspace*{0.6cm} GetVocSystem(GetNativeVocSystem(tnvoc)))) = ErrorMispelled \item\hspace*{0.4cm} or not MakeItem(MakePair( \item\hspace*{0.6cm} GetNativeWord(tnvoc), \item\hspace*{0.6cm} MakeWord(str,GetForeignLanguage( \item\hspace*{0.8cm} GetVocSystem(GetNativeVocSystem(tnvoc))))),false) \item\hspace*{0.4cm} $\in$ GetItemList(GetVocSystem(GetNativeVocSystem(tnvoc))) {\bf then} \item\hspace*{0.4cm} GenerateNativeTest(GetNativeVocSystem(tnvoc), \item\hspace*{0.4cm} GetNativeScore(tnvoc)-1) \item\hspace*{0.2cm} {\bf else} \item\hspace*{0.4cm} GenerateNativeTest(GetNativeVocSystem(tnvoc),GetNativeScore(tnvoc)+1) \item \item GetNativeStringList(\emptyL,slst) = slst \item GetNativeStringList(NewItem(vit,ilst),slst) = \item\hspace*{0.2cm} GetNativeStringList(ilst, AddString(GetNative(GetPair(vit)),slst)) \item \item GetPairList(\emptyL,plst) = plst \item GetPairList(NewItem(vit,ilst),plst) = \item\hspace*{0.2cm} GetPairList(ilst,NewPair(GetPair(vit),plst) \item \item GetListofPairLists(\emptyL,sllst) = sllst \item GetListofPairLists(NewItemListsList(ilst,illst),sllst) = \item\hspace*{0.2cm} GetListOfPairLists(illst, NewPairList(GetPairList(ilst,\emptyL),sllst)) \item \item {\sf The axioms of the operations for the foreign case are analogeous to the native case.} \end{axioms} \end{spec} \section{Doors and Windows: the User Interface} Now that we have all the operations and sorts we need, we can provide an easy interface to all these operations, where the user only has to think about the basic aspects. These basic aspects are: \begin{enumerate} \item for the dictionary: the languages and the strings he uses to enter words; \item for the test suite: the number of questions he wants to be asked \end{enumerate} The fact that these are the only things the user now finally needs is reflected in the arity of the operations in the final user interface, described in the specification \textit{UserInterfaceSpec}. \begin{spec}{UserInterfaceSpec} \item freely generated type Score \item \begin{opns} \item constr \opII{\_Out\_}{Int}{NaT}{Score} \item\opII{GenerateDictionary}{language}{language}{vocsystem} \item\opIII{AddEntry}{string}{string}{vocsystem}{vocsystem} \item\opIII{DeleteEntry}{string}{string}{vocsystem}{vocsystem} \item\opII{GiveNativeTranslation}{string}{vocsystem}{listofstrings} \item\opII{GiveForeignTranslation}{string}{vocsystem}{listofstrings} \item\opI{GetAllTranslationsByNativeOrder}{vocsystem}{listofpairlists} \item\opI{GetAllTranslationsByForeignOrder}{vocsystem}{listofpairlists} \item\opII{TestMyNativeKnowledge}{Nat}{vocsystem}{testnativevocsystem} \item\opII{TestMyForeignKnowledge}{Nat}{vocsystem}{testforeignvocsystem} \item\opII{GiveNativeAnswers}{listofstrings}{testforeignvocsystem}{testforeignvocsystem} \item\opII{GiveForeignAnswers}{listofstrings}{testnativevocsystem}{testnativevocsystem} \item\opII{ShowMyScoreInNative}{testnativevocsystem}{testnativevocsystem}{Score} \item\opII{ShowMyScoreInForeign}{testforeignvocsystem}{testforeignvocsystem}{Score} \end{opns} \begin{vars} \item l1, l2: language \item s1, s2: string \item lst: listofstrings \item sdic: vocsystem \item no: Nat \item tnvoc,nansw: testnativevocsystem \item tfvoc,fansw: testforeignvocsystem \end{vars} \begin{axioms} \item GenerateDictionary(l1,l2) = Dictionary(l1,l2,[]) \item AddEntry(s1,s2,sdic) = AddEntryToDictionary(s1,s2,sdic) \item DeleteEntry(s1,s2,sdic) = DeleteEntryFromDictionary(s1,s2,sdic) \item GiveNativeTranslation(s1,sdic) = GetNativeStringList(TranslateIntoNative(s1,sdic),[]) \item GiveForeignTranslation(s1,sdic) = GetForeignStringList(TranslateIntoForeign(s1,sdic),[]) \item GetAllTranslationsByNativeOrder(sdic) = \item\hspace*{0.2cm} GetListOfPairLists(GetNativeOrderedItemList(GetListOfNativeWords(sdic,sdic),[]),[]) \item GetAllTranslationsByForeignOrder(sdic) = \item\hspace*{0.2cm} GetListOfPairLists(GetForeignOrderedItemList(GetListOfForeignWords(sdic,sdic),[]),[]) \item TestMyNativeKnowledge(no,sdic) = \item\hspace*{0.2cm} GenerateNativeTest(GenerateNativeVocSystem(sdic,no),0) \item TestMyForeignKnowledge(no,sdic) = \item\hspace*{0.2cm} GenerateForeignTest(GenerateForeignVocSystem(sdic,no),0) \item GiveNativeAnswers([],tfvoc) = DeleteForeignEntry(GetForeignHead(tfvoc),tfvoc) \item GiveNativeAnswers(NewString(s1,lst),tfvoc) = \item\hspace*{0.2cm} GiveNativeAnswers(lst,AdaptForeignVocSystem(s1,tfvoc)) \item GiveForeignAnswers([],tnvoc) = DeleteNativeEntry(GetNativeHead(tnvoc),tnvoc) \item GiveForeignAnswers(NewString(s1,lst),tnvoc) = \item\hspace*{0.2cm}GiveForeignAnswers(lst,AdaptNativeVocSystem(s1,tnvoc)) \item ShowMyScoreInNative(nansw,tnvoc) = GetNativeScore(nansw) Out GetMaxNativeScore(tnvoc) \item ShowMyScoreInForeign(fansw,tfvoc) = GetForeignScore(fansw) Out GetMaxForeignScore(tfvoc) \end{axioms} \end{spec} Note that the operations $GetNativeScore$ and $GetForeignScore$ take two $testnativevocsystem$s resp. two $testforeignvocsystem$s. The first entry is the test vocabulary system after all questions have been answered, and consists out of an empty native (or foreign) word vocabulary system and the user's final score. The second entry is the original test suite generated, and is used to get the maximal score. \chapter{The cafeOBJ Implementation: Modules {\tt dictionary} and {\tt lowlevel}} We conclude this paper with the cafeOBJ implementation of the specification introduced in in the previous chapter. This chapter contains two sections: the first contains the cafeOBJ implementation itself, and the second section contains an example of the way this cafeOBJ implementation and the specification work. \section{The cafeOBJ Modules} The source code for these modules is added to this document in the form of two appendices: the first appendix describes the module {\tt lowlevel.mod} and contains the implementation of the low level material of the dictionary as depicted in figure $2.1$. The second appendix describes the module {\tt dictionary.mod} and contains the upper level op the specification, ultimately leading to the implementation of the user interface part of the specification. \section{An English-to-German Student Dictionary} \noindent {\em Let us build a simple English-German dictionary} \smallskip \noindent \%StudentDictionarySpec $>$ op testDict : $->$ vocsystem . \smallskip \noindent \%StudentDictionarySpec $>$ eq testDict = AddEntry("car","Auto",AddEntry("car","Wagen", AddEntry("frog","Frosch", AddEntry("paper","Papier", AddEntry("table","Tisch",AddEntry("blackboard","Tafel", AddEntry("table","Tabelle",GenerateDictionary(English,German)))))))) . \bigskip \noindent {\em Let us see what it is like} \smallskip \noindent \%StudentDictionarySpec $>$ reduce testDict . \smallskip \noindent * -- reduce in % : testDict Dictionary(MakeLanguage(NewRule("qx",NewRule("uu",rEmpty)),NewChar( 'A',NewChar('a',NewChar('B',NewChar('b',NewChar('C',NewChar('c', NewChar('D',NewChar('d',NewChar('E',NewChar('e',NewChar('F',NewChar( 'f',NewChar('G',NewChar('g',NewChar('H',NewChar('h',NewChar('I', NewChar('i',NewChar('J',NewChar('j',NewChar('K',NewChar('k',NewChar( 'L',NewChar('l',NewChar('M',NewChar('m',NewChar('N',NewChar('n', NewChar('O',NewChar('o',NewChar('P',NewChar('p',NewChar('Q',NewChar( 'q',NewChar('R',NewChar('r',NewChar('S',NewChar('s',NewChar('T', NewChar('t',NewChar('U',NewChar('u',NewChar('V',NewChar('v',NewChar( 'W',NewChar('w',NewChar('X',NewChar('x',NewChar('Y',NewChar('y', NewChar('Z',NewChar('z',coEmpty)))))))))))))))))))))))))))))))) ))))))))))))))))))))),MakeLanguage(NewRule("yy",NewRule("jj",rEmpty) ),NewChar('A',NewChar('a',NewChar('B',NewChar('b',NewChar('C',NewChar( 'c',NewChar('D',NewChar('d',NewChar('E',NewChar('e',NewChar('F', NewChar('f',NewChar('G',NewChar('g',NewChar('H',NewChar('h',NewChar( 'I',NewChar('i',NewChar('J',NewChar('j',NewChar('K',NewChar('k', NewChar('L',NewChar('l',NewChar('M',NewChar('m',NewChar('N',NewChar( 'n',NewChar('O',NewChar('o',NewChar('P',NewChar('p',NewChar('Q', NewChar('q',NewChar('R',NewChar('r',NewChar('S',NewChar('s',NewChar( 'T',NewChar('t',NewChar('U',NewChar('u',NewChar('V',NewChar('v', NewChar('W',NewChar('w',NewChar('X',NewChar('x',NewChar('Y',NewChar( 'y',NewChar('Z',NewChar('z',coEmpty)))))))))))))))))))))))))))) ))))))))))))))))))))))))),NewItem(MakeItem(MakePair(CorrectWord( "car"),CorrectWord("Auto")),false),NewItem(MakeItem(MakePair(CorrectWord( "car"),CorrectWord("Wagen")),false),NewItem(MakeItem(MakePair(CorrectWord( "frog"),CorrectWord("Frosch")),false),NewItem(MakeItem(MakePair( CorrectWord("paper"),CorrectWord("Papier")),false),NewItem(MakeItem( MakePair(CorrectWord("table"),CorrectWord("Tisch")),false),NewItem( MakeItem(MakePair(CorrectWord("blackboard"),CorrectWord("Tafel") ),false),NewItem(MakeItem(MakePair(CorrectWord("table"),CorrectWord( "Tabelle")),false),liEmpty)))))))) : vocsystem (0.000 sec for parse, 47165 rewrites(8.930 sec), 61237 match attempts) \bigskip \noindent {\em Let us use it to translate a couple of words in both directions} \smallskip \noindent \%StudentDictionarySpec $>$ reduce GiveNativeTranslation("Wagen",testDict) . \smallskip \noindent -- reduce in % : GiveNativeTranslation("Wagen",testDict) NewString("car",lsEmpty) : listofstrings (0.000 sec for parse, 47367 rewrites(9.570 sec), 61549 match attempts) \bigskip \noindent \%StudentDictionarySpec $>$ reduce GiveForeignTranslation("car",testDict) . \smallskip \noindent -- reduce in % : GiveForeignTranslation("car",testDict) NewString("Auto",NewString("Wagen",lsEmpty)) : listofstrings (0.000 sec for parse, 47351 rewrites(9.610 sec), 61523 match attempts) \bigskip \noindent {\em Let us build a test for testing the knowledge of English words} \smallskip \noindent \%StudentDictionarySpec $>$ op nativeKnowledgeTest : -> testnativevocsystem . \smallskip \noindent \%StudentDictionarySpec $>$ eq nativeKnowledgeTest = TestMyNativeKnowledge(4,testDict) . \bigskip \noindent {\em Let us look at the test} \smallskip \noindent \%StudentDictionarySpec $>$ reduce nativeKnowledgeTest . \smallskip \noindent -- reduce in % : nativeKnowledgeTest GenerateNativeTest(AddEntryToNativeVocSystem(CorrectWord("blackboard") ,AddEntryToNativeVocSystem(CorrectWord("frog"),AddEntryToNativeVocSystem( CorrectWord("table"),AddEntryToNativeVocSystem(CorrectWord("car") ,NewNativeVocSystem(Dictionary(MakeLanguage(NewRule("qx",NewRule( "uu",rEmpty)),NewChar('A',NewChar('a',NewChar('B',NewChar('b',NewChar( 'C',NewChar('c',NewChar('D',NewChar('d',NewChar('E',NewChar('e', NewChar('F',NewChar('f',NewChar('G',NewChar('g',NewChar('H',NewChar( 'h',NewChar('I',NewChar('i',NewChar('J',NewChar('j',NewChar('K', NewChar('k',NewChar('L',NewChar('l',NewChar('M',NewChar('m',NewChar( 'N',NewChar('n',NewChar('O',NewChar('o',NewChar('P',NewChar('p', NewChar('Q',NewChar('q',NewChar('R',NewChar('r',NewChar('S',NewChar( 's',NewChar('T',NewChar('t',NewChar('U',NewChar('u',NewChar('V', NewChar('v',NewChar('W',NewChar('w',NewChar('X',NewChar('x',NewChar( 'Y',NewChar('y',NewChar('Z',NewChar('z',coEmpty)))))))))))))))) ))))))))))))))))))))))))))))))))))))),MakeLanguage(NewRule("yy", NewRule("jj",rEmpty)),NewChar('A',NewChar('a',NewChar('B',NewChar( 'b',NewChar('C',NewChar('c',NewChar('D',NewChar('d',NewChar('E', NewChar('e',NewChar('F',NewChar('f',NewChar('G',NewChar('g',NewChar( 'H',NewChar('h',NewChar('I',NewChar('i',NewChar('J',NewChar('j', NewChar('K',NewChar('k',NewChar('L',NewChar('l',NewChar('M',NewChar( 'm',NewChar('N',NewChar('n',NewChar('O',NewChar('o',NewChar('P', NewChar('p',NewChar('Q',NewChar('q',NewChar('R',NewChar('r',NewChar( 'S',NewChar('s',NewChar('T',NewChar('t',NewChar('U',NewChar('u', NewChar('V',NewChar('v',NewChar('W',NewChar('w',NewChar('X',NewChar( 'x',NewChar('Y',NewChar('y',NewChar('Z',NewChar('z',coEmpty)))) ))))))))))))))))))))))))))))))))))))))))))))))))),NewItem(MakeItem( MakePair(CorrectWord("car"),CorrectWord("Auto")),false),NewItem( MakeItem(MakePair(CorrectWord("car"),CorrectWord("Wagen")),false) ,NewItem(MakeItem(MakePair(CorrectWord("frog"),CorrectWord("Frosch") ),false),NewItem(MakeItem(MakePair(CorrectWord("paper"),CorrectWord( "Papier")),false),NewItem(MakeItem(MakePair(CorrectWord("table") ,CorrectWord("Tisch")),false),NewItem(MakeItem(MakePair(CorrectWord( "blackboard"),CorrectWord("Tafel")),false),NewItem(MakeItem(MakePair( CorrectWord("table"),CorrectWord("Tabelle")),false),liEmpty)))) ))))))))),0) : testnativevocsystem (0.000 sec for parse, 49076 rewrites(10.470 sec), 64000 match attempts) \bigskip \noindent {\em Let us translate the first entry, i.e. blackboard into German} \smallskip \noindent \%StudentDictionarySpec $>$ reduce GiveForeignAnswers( AddString("Tafel",lsEmpty),nativeKnowledgeTest) . \smallskip \noindent -- reduce in % : GiveForeignAnswers(AddString("Tafel",lsEmpty),nativeKnowledgeTest) GenerateNativeTest(AddEntryToNativeVocSystem(CorrectWord("frog"), AddEntryToNativeVocSystem(CorrectWord("table"),AddEntryToNativeVocSystem( CorrectWord("car"),NewNativeVocSystem(Dictionary(MakeLanguage(NewRule( "qx",NewRule("uu",rEmpty)),NewChar('A',NewChar('a',NewChar('B', NewChar('b',NewChar('C',NewChar('c',NewChar('D',NewChar('d',NewChar( 'E',NewChar('e',NewChar('F',NewChar('f',NewChar('G',NewChar('g', NewChar('H',NewChar('h',NewChar('I',NewChar('i',NewChar('J',NewChar( 'j',NewChar('K',NewChar('k',NewChar('L',NewChar('l',NewChar('M', NewChar('m',NewChar('N',NewChar('n',NewChar('O',NewChar('o',NewChar( 'P',NewChar('p',NewChar('Q',NewChar('q',NewChar('R',NewChar('r', NewChar('S',NewChar('s',NewChar('T',NewChar('t',NewChar('U',NewChar( 'u',NewChar('V',NewChar('v',NewChar('W',NewChar('w',NewChar('X', NewChar('x',NewChar('Y',NewChar('y',NewChar('Z',NewChar('z',coEmpty) )))))))))))))))))))))))))))))))))))))))))))))))))))),MakeLanguage( NewRule("yy",NewRule("jj",rEmpty)),NewChar('A',NewChar('a',NewChar( 'B',NewChar('b',NewChar('C',NewChar('c',NewChar('D',NewChar('d', NewChar('E',NewChar('e',NewChar('F',NewChar('f',NewChar('G',NewChar( 'g',NewChar('H',NewChar('h',NewChar('I',NewChar('i',NewChar('J', NewChar('j',NewChar('K',NewChar('k',NewChar('L',NewChar('l',NewChar( 'M',NewChar('m',NewChar('N',NewChar('n',NewChar('O',NewChar('o', NewChar('P',NewChar('p',NewChar('Q',NewChar('q',NewChar('R',NewChar( 'r',NewChar('S',NewChar('s',NewChar('T',NewChar('t',NewChar('U', NewChar('u',NewChar('V',NewChar('v',NewChar('W',NewChar('w',NewChar( 'X',NewChar('x',NewChar('Y',NewChar('y',NewChar('Z',NewChar('z', coEmpty))))))))))))))))))))))))))))))))))))))))))))))))))))),NewItem( MakeItem(MakePair(CorrectWord("car"),CorrectWord("Auto")),false) ,NewItem(MakeItem(MakePair(CorrectWord("car"),CorrectWord("Wagen") ),false),NewItem(MakeItem(MakePair(CorrectWord("frog"),CorrectWord( "Frosch")),false),NewItem(MakeItem(MakePair(CorrectWord("paper") ,CorrectWord("Papier")),false),NewItem(MakeItem(MakePair(CorrectWord( "table"),CorrectWord("Tisch")),false),NewItem(MakeItem(MakePair( CorrectWord("blackboard"),CorrectWord("Tafel")),false),NewItem( MakeItem(MakePair(CorrectWord("table"),CorrectWord("Tabelle")), false),liEmpty)))))))))))),1) : testnativevocsystem (0.000 sec for parse, 51769 rewrites(10.790 sec), 67501 match attempts) \bigskip \noindent {\em We can see our score} \smallskip \noindent \%StudentDictionarySpec $>$ reduce ShowMyScoreInNative(GiveForeignAnswers(AddString("Tafel", AddString("Wrong",lsEmpty)),nativeKnowledgeTest),nativeKnowledgeTest) . \smallskip \noindent -- reduce in % : ShowMyScoreInNative(GiveForeignAnswers(AddString( "Tafel",AddString("Wrong",lsEmpty)),nativeKnowledgeTest),nativeKnowledgeTest) 1 OutOf 6 : Score (0.000 sec for parse, 108253 rewrites(22.250 sec), 141389 match attempts) \bigskip \noindent {\em We can see all the translations contained in the dictionary ordered by foreign order} \noindent \%StudentDictionarySpec $>$ reduce GetAllTranslationsByForeignOrder(testDict) . \smallskip \noindent -- reduce in % : GetAllTranslationsByForeignOrder(testDict) NewPairList(NewPair(MakePair(CorrectWord("car"),CorrectWord("Auto") ),plEmpty),NewPairList(NewPair(MakePair(CorrectWord("frog"),CorrectWord( "Frosch")),plEmpty),NewPairList(NewPair(MakePair(CorrectWord("paper") ,CorrectWord("Papier")),plEmpty),NewPairList(NewPair(MakePair(CorrectWord( "table"),CorrectWord("Tabelle")),plEmpty),NewPairList(NewPair(MakePair( CorrectWord("blackboard"),CorrectWord("Tafel")),plEmpty),NewPairList( NewPair(MakePair(CorrectWord("table"),CorrectWord("Tisch")),plEmpty) ,NewPairList(NewPair(MakePair(CorrectWord("car"),CorrectWord("Wagen") ),plEmpty),lplEmpty))))))) : listofpairlists (0.000 sec for parse, 50669 rewrites(10.870 sec), 67258 match attempts) \bigskip \end{document}