** CafeOBJ 1.3.1 ** ** Module specifications for Student Dictionary System (Upper level) ** Import low-level stuff: input lowlevel.mod ** --------------------------------------------- ** Specification of the Vocabulary System sort ** --------------------------------------------- module! DictionarySpec { imports { protecting (ListOfItemsSpec) } signature { [vocsystem] ** The Constructors of the sort: op Dictionary : language language listofitems -> vocsystem { constr } op ErrorNativeWordIsMisspelled : -> vocsystem { constr } op ErrorForeignWordIsMisspelled : -> vocsystem { constr } op AddEntryToDictionary : String String vocsystem -> vocsystem op DeleteEntryFromDictionary : String String vocsystem -> vocsystem ** The other operations: op GetNativeLanguage : vocsystem -> language op GetForeignLanguage : vocsystem -> language op GetItemList : vocsystem -> listofitems op RandomVocItem : vocsystem -> vocitem op ResetFlags : vocsystem -> vocsystem op ResetFlagsRec : listofitems listofitems -> listofitems op SetVocItemFlag : vocitem Bool -> vocitem op SetNativeFlags : word vocsystem -> vocsystem op SetNativeFlagsRec : word listofitems listofitems -> listofitems op SetForeignFlags : word vocsystem -> vocsystem op SetForeignFlagsRec : word listofitems listofitems -> listofitems ** We already provide the translation operations: op TranslateIntoNative : String vocsystem -> listofitems op TranslateIntoForeign : String vocsystem -> listofitems op TranslateIntoNativeRec : String listofitems listofitems -> listofitems op TranslateIntoForeignRec : String listofitems listofitems -> listofitems } axioms { vars l1 l2 : language vars il o : listofitems var p : pair vars f b : Bool var voc : vocsystem vars s1 s2 : String var w : word var vi : vocitem ** We start out with some nice operations: eq GetNativeLanguage(Dictionary(l1,l2,il)) = l1 . eq GetForeignLanguage(Dictionary(l1,l2,il)) = l2 . eq GetItemList(Dictionary(l1,l2,il)) = il . ** The next operation is the addition of elements to the dictionary: ** We first check whether the native word is correctly spelled: ceq AddEntryToDictionary(s1,s2,voc) = ErrorNativeWordIsMisspelled if MakeWord(s1,GetNativeLanguage(voc)) == ErrorMisspelled . ** If this is the case, then we check the foreign spelling: ceq AddEntryToDictionary(s1,s2,voc) = ErrorForeignWordIsMisspelled if not MakeWord(s1,GetNativeLanguage(voc)) == ErrorMisspelled and MakeWord(s2,GetForeignLanguage(voc)) == ErrorMisspelled . ** If both are correct, we continue: ceq AddEntryToDictionary(s1,s2,voc) = Dictionary(GetNativeLanguage(voc),GetForeignLanguage(voc), AddItem( MakeItem( MakePair( MakeWord(s1,GetNativeLanguage(voc)), MakeWord(s2,GetForeignLanguage(voc))), false), GetItemList(voc))) if not MakeWord(s1,GetNativeLanguage(voc)) == ErrorMisspelled and not MakeWord(s2,GetForeignLanguage(voc)) == ErrorMisspelled . ** We allow the user to remove entries from the dictionary as well: eq DeleteEntryFromDictionary(s1,s2,Dictionary(l1,l2,liEmpty)) = Dictionary(l1,l2,liEmpty) . ceq DeleteEntryFromDictionary(s1,s2,Dictionary(l1,l2,NewItem(vi,il))) = Dictionary(l1,l2,il) if s1 == GetNative(GetPair(vi)) and s2 == GetForeign(GetPair(vi)) . ceq DeleteEntryFromDictionary(s1,s2,Dictionary(l1,l2,NewItem(vi,il))) = AddEntryToDictionary(GetNative(GetPair(vi)), GetForeign(GetPair(vi)), DeleteEntryFromDictionary(s1,s2,Dictionary(l1,l2,il))) if not (s1 == GetNative(GetPair(vi)) and s2 == GetForeign(GetPair(vi))) . ** Let us now provide the operations on the flags: eq SetVocItemFlag(vi,b) = MakeItem(GetPair(vi),b) . ** Flags are set recursively: ceq SetNativeFlagsRec(w,il,o) = o if il == liEmpty . ceq SetNativeFlagsRec(w,il,o) = SetNativeFlagsRec(w,Tail(il),AddItem(SetVocItemFlag(Head(il),true),o)) if not il == liEmpty and GetNative(GetPair(Head(il))) == GetString(w) . ceq SetNativeFlagsRec(w,il,o) = SetNativeFlagsRec(w,Tail(il),AddItem(Head(il),o)) if not il == liEmpty and not GetNative(GetPair(Head(il))) == GetString(w) . ceq SetForeignFlagsRec(w,il,o) = o if il == liEmpty . ceq SetForeignFlagsRec(w,il,o) = SetForeignFlagsRec(w,Tail(il),AddItem(SetVocItemFlag(Head(il),true), o)) if not il == liEmpty and GetForeign(GetPair(Head(il))) == GetString(w) . ceq SetForeignFlagsRec(w,il,o) = SetForeignFlagsRec(w,Tail(il),AddItem(Head(il),o)) if not il == liEmpty and not GetForeign(GetPair(Head(il))) == GetString(w) . ** The recursion is always called starting with empty output: eq SetNativeFlags(w,voc) = Dictionary( GetNativeLanguage(voc), GetForeignLanguage(voc), SetNativeFlagsRec(w,GetItemList(voc),liEmpty)) . eq SetForeignFlags(w,voc) = Dictionary( GetNativeLanguage(voc), GetForeignLanguage(voc), SetForeignFlagsRec(w,GetItemList(voc),liEmpty)) . ** We also need to reset the flags when making a new test suite: ceq ResetFlagsRec(il,o) = o if il == liEmpty . ceq ResetFlagsRec(il,o) = ResetFlagsRec(Tail(il), AddItem(SetVocItemFlag(Head(il),false),o)) if not il == liEmpty . eq ResetFlags(voc) = Dictionary(GetNativeLanguage(voc), GetForeignLanguage(voc),ResetFlagsRec(GetItemList(voc),liEmpty)) . ** The only thing missing is the random operation. It is not easy to ** implement a pseudo random function in cafeOBJ, so instead we simply ** walk through the list and take the first vocabulary item that is ** eligible. ceq RandomVocItem(voc) = ErrorOutOfEntries if GetItemList(voc) == liEmpty . ceq RandomVocItem(voc) = Head(GetItemList(voc)) if not GetItemList(voc) == liEmpty and not GetFlag(Head(GetItemList(voc))) . ceq RandomVocItem(voc) = RandomVocItem(Dictionary(GetNativeLanguage(voc), GetForeignLanguage(voc),Tail(GetItemList(voc)))) if not GetItemList(voc) == liEmpty and GetFlag(Head(GetItemList(voc))) . ** Now it is time to implement the translation operations, as they will be ** used in the nativevocsystem sort. ceq TranslateIntoNativeRec(s1,il,o) = o if il == liEmpty . ceq TranslateIntoNativeRec(s1,il,o) = TranslateIntoNativeRec(s1,Tail(il), AddItem(Head(il),o)) if not il == liEmpty and GetForeign(GetPair(Head(il))) == s1 . ceq TranslateIntoNativeRec(s1,il,o) = TranslateIntoNativeRec(s1,Tail(il),o) if not il == liEmpty and not GetForeign(GetPair(Head(il))) == s1 . eq TranslateIntoNative(s1,voc) = TranslateIntoNativeRec(s1,GetItemList(voc),liEmpty) . ceq TranslateIntoForeignRec(s1,il,o) = o if il == liEmpty . ceq TranslateIntoForeignRec(s1,il,o) = TranslateIntoForeignRec(s1,Tail(il), AddItem(Head(il),o)) if not il == liEmpty and GetNative(GetPair(Head(il))) == s1 . ceq TranslateIntoForeignRec(s1,il,o) = TranslateIntoForeignRec(s1,Tail(il),o) if not il == liEmpty and not GetNative(GetPair(Head(il))) == s1 . eq TranslateIntoForeign(s1,voc) = TranslateIntoForeignRec(s1,GetItemList(voc),liEmpty) . } } ** ---------------------------------------------------- ** Specification of the Native Vocabulary System sort ** ---------------------------------------------------- module! PreTestVocSystemSpec { imports { protecting (DictionarySpec) protecting (ListOfListOfItemsSpec) protecting (INT) } signature { [ nativevocsystem foreignvocsystem ] ** ---------------- ** The Native Part: ** ---------------- ** The constructors of the sort: op NewNativeVocSystem : vocsystem -> nativevocsystem { constr } op AddEntryToNativeVocSystem : word nativevocsystem -> nativevocsystem { constr } op ErrorNativeVocExceedsVoc : -> nativevocsystem { constr } op ErrorNoEntriesLeft : -> nativevocsystem { constr } ** The other operations: op _In_ : word nativevocsystem -> Bool op AddToNativeVoc : word nativevocsystem -> nativevocsystem op DeleteNativeEntry : word nativevocsystem -> nativevocsystem op GetVocSystem : nativevocsystem -> vocsystem op RecGenerateNativeVocSystem : nativevocsystem Int vocsystem -> nativevocsystem op GenerateNativeVocSystem : vocsystem Int -> nativevocsystem op GetNativeHead : nativevocsystem -> word op GetNativeTail : nativevocsystem -> nativevocsystem op MaxNativeScore : nativevocsystem -> Nat op GetMaxNative : nativevocsystem word -> word op GetNativeTranslationList : nativevocsystem listoflistofitems -> listoflistofitems op GetOrderedNativeWordList : nativevocsystem nativevocsystem -> nativevocsystem op GetNativeOrderedItemList : nativevocsystem listoflistofitems -> listoflistofitems op GetListOfNativeWords : vocsystem vocsystem -> nativevocsystem ** ----------------- ** The Foreign Part: ** ----------------- ** The constructors of the sort: op NewForeignVocSystem : vocsystem -> foreignvocsystem { constr } op AddEntryToForeignVocSystem : word foreignvocsystem -> foreignvocsystem { constr } op ErrorForeignVocExceedsVoc : -> foreignvocsystem { constr } op ErrorNoForeignEntriesLeft : -> foreignvocsystem { constr } ** The other operations: op _InForeign_ : word foreignvocsystem -> Bool op AddToForeignVoc : word foreignvocsystem -> foreignvocsystem op DeleteForeignEntry : word foreignvocsystem -> foreignvocsystem op GetVocSystem : foreignvocsystem -> vocsystem op RecGenerateForeignVocSystem : foreignvocsystem Int vocsystem -> foreignvocsystem op GenerateForeignVocSystem : vocsystem Int -> foreignvocsystem op GetForeignHead : foreignvocsystem -> word op GetForeignTail : foreignvocsystem -> foreignvocsystem op MaxForeignScore : foreignvocsystem -> Nat op GetMaxForeign : foreignvocsystem word -> word op GetForeignTranslationList : foreignvocsystem listoflistofitems -> listoflistofitems op GetOrderedForeignWordList : foreignvocsystem foreignvocsystem -> foreignvocsystem op GetForeignOrderedItemList : foreignvocsystem listoflistofitems -> listoflistofitems op GetListOfForeignWords : vocsystem vocsystem -> foreignvocsystem } axioms { var nativevoc : nativevocsystem var natout : nativevocsystem var foreignvoc : foreignvocsystem var forout : foreignvocsystem var size : Int var voc : vocsystem vars w v : word var output : word var lst : listoflistofitems var it : vocitem var itlst : listofitems vars l1 l2 : language ** ---------------- ** The Native Part: ** ---------------- eq GetVocSystem(NewNativeVocSystem(voc)) = voc . eq GetVocSystem(AddEntryToNativeVocSystem(w,nativevoc)) = GetVocSystem(nativevoc) . eq DeleteNativeEntry(w,NewNativeVocSystem(voc)) = NewNativeVocSystem(voc) . ceq DeleteNativeEntry(w,AddEntryToNativeVocSystem(v,nativevoc)) = nativevoc if v == w . ceq DeleteNativeEntry(w,AddEntryToNativeVocSystem(v,nativevoc)) = AddEntryToNativeVocSystem(v,DeleteNativeEntry(w,nativevoc)) if not v == w . ceq AddToNativeVoc(w,nativevoc) = nativevoc if w In nativevoc . ceq AddToNativeVoc(w,nativevoc) = AddEntryToNativeVocSystem(w,nativevoc) if not w In nativevoc . eq w In NewNativeVocSystem(voc) = false . ceq w In AddEntryToNativeVocSystem(v,nativevoc) = true if w == v . ceq w In AddEntryToNativeVocSystem(v,nativevoc) = ( w In nativevoc ) if not w == v . ceq RecGenerateNativeVocSystem(nativevoc,size,voc) = ErrorNativeVocExceedsVoc if RandomVocItem(voc) == ErrorOutOfEntries and not size == 0 . ceq RecGenerateNativeVocSystem(nativevoc,size,voc) = nativevoc if not RandomVocItem(voc) == ErrorOutOfEntries and size == 0 . ceq RecGenerateNativeVocSystem(nativevoc,size,voc) = nativevoc if RandomVocItem(voc) == ErrorOutOfEntries and size == 0 . ceq RecGenerateNativeVocSystem(nativevoc,size,voc) = RecGenerateNativeVocSystem( AddEntryToNativeVocSystem( CorrectWord(GetNative(GetPair(RandomVocItem(voc)))), nativevoc), size - 1, SetNativeFlags( CorrectWord(GetNative(GetPair(RandomVocItem(voc)))), voc)) if not RandomVocItem(voc) == ErrorOutOfEntries and not size == 0 . eq GenerateNativeVocSystem(voc,size) = RecGenerateNativeVocSystem( NewNativeVocSystem(voc),size,voc) . eq GetNativeHead(NewNativeVocSystem(voc)) = ErrorNoWordLeft . eq GetNativeHead(AddEntryToNativeVocSystem(w,nativevoc)) = w . eq GetNativeTail(NewNativeVocSystem(voc)) = ErrorNoEntriesLeft . eq GetNativeTail(AddEntryToNativeVocSystem(w,nativevoc)) = nativevoc . eq MaxNativeScore(NewNativeVocSystem(voc)) = 0 . eq MaxNativeScore(AddEntryToNativeVocSystem(w,nativevoc)) = MaxNativeScore(nativevoc) + Length( TranslateIntoForeign(GetString(w),GetVocSystem(nativevoc))) . eq GetMaxNative(NewNativeVocSystem(voc),output) = output . ceq GetMaxNative(AddEntryToNativeVocSystem(w,NewNativeVocSystem(voc)),output) = w if output == DummyValue . ceq GetMaxNative(AddEntryToNativeVocSystem(w,NewNativeVocSystem(voc)),output) = output if not output == DummyValue . ceq GetMaxNative(nativevoc,output) = GetMaxNative( AddEntryToNativeVocSystem(GetNativeHead(nativevoc), GetNativeTail(GetNativeTail(nativevoc))), GetNativeHead(nativevoc)) if not GetNativeHead(nativevoc) == ErrorNoWordLeft and not GetNativeTail(GetNativeTail(nativevoc)) == ErrorNoEntriesLeft and not IsStringSmaller(GetString(GetNativeHead(nativevoc)), GetString(GetNativeHead(GetNativeTail(nativevoc)))) . ceq GetMaxNative(nativevoc,output) = GetMaxNative(GetNativeTail(nativevoc),GetNativeHead(GetNativeTail(nativevoc))) if not GetNativeHead(nativevoc) == ErrorNoWordLeft and not GetNativeTail(GetNativeTail(nativevoc)) == ErrorNoEntriesLeft and IsStringSmaller(GetString(GetNativeHead(nativevoc)), GetString(GetNativeHead(GetNativeTail(nativevoc)))) . ceq GetOrderedNativeWordList(nativevoc,natout) = natout if GetNativeHead(nativevoc) == ErrorNoWordLeft . ceq GetOrderedNativeWordList(nativevoc,natout) = GetOrderedNativeWordList(DeleteNativeEntry( GetMaxNative(nativevoc,DummyValue),nativevoc), AddEntryToNativeVocSystem(GetMaxNative(nativevoc,DummyValue),natout)) if not GetNativeHead(nativevoc) == ErrorNoWordLeft . eq GetNativeTranslationList(NewNativeVocSystem(voc),lst) = lst . eq GetNativeTranslationList(AddEntryToNativeVocSystem(w,nativevoc),lst) = GetNativeTranslationList(nativevoc, AddToItemListsList( TranslateIntoForeign(GetString(w), GetVocSystem(nativevoc)), lst)) . eq GetNativeOrderedItemList(nativevoc,lst) = GetNativeTranslationList( GetOrderedNativeWordList(nativevoc, NewNativeVocSystem(GetVocSystem(nativevoc))), lst) . ** The second vocabulary system is a copy of the original one and keeps all ** data that is lost from the first one as the first vocsystem is emptied ** in order to build the list of all native words . eq GetListOfNativeWords(Dictionary(l1,l2,liEmpty),voc) = NewNativeVocSystem(voc) . eq GetListOfNativeWords(Dictionary(l1,l2,NewItem(it,itlst)),voc) = AddToNativeVoc( CorrectWord( GetNative(GetPair(it))),GetListOfNativeWords(Dictionary(l1,l2,itlst),voc)) . ** ----------------- ** The Foreign Part: ** ----------------- eq GetVocSystem(NewForeignVocSystem(voc)) = voc . eq GetVocSystem(AddEntryToForeignVocSystem(w,foreignvoc)) = GetVocSystem(foreignvoc) . eq DeleteForeignEntry(w,NewForeignVocSystem(voc)) = NewForeignVocSystem(voc) . ceq DeleteForeignEntry(w,AddEntryToForeignVocSystem(v,foreignvoc)) = foreignvoc if v == w . ceq DeleteForeignEntry(w,AddEntryToForeignVocSystem(v,foreignvoc)) = AddEntryToForeignVocSystem(v,DeleteForeignEntry(w,foreignvoc)) if not v == w . ceq AddToForeignVoc(w,foreignvoc) = foreignvoc if w InForeign foreignvoc . ceq AddToForeignVoc(w,foreignvoc) = AddEntryToForeignVocSystem(w,foreignvoc) if not w InForeign foreignvoc . eq w InForeign NewForeignVocSystem(voc) = false . ceq w InForeign AddEntryToForeignVocSystem(v,foreignvoc) = true if w == v . ceq w InForeign AddEntryToForeignVocSystem(v,foreignvoc) = ( w InForeign foreignvoc ) if not w == v . ceq RecGenerateForeignVocSystem(foreignvoc,size,voc) = ErrorForeignVocExceedsVoc if RandomVocItem(voc) == ErrorOutOfEntries . ceq RecGenerateForeignVocSystem(foreignvoc,size,voc) = foreignvoc if not RandomVocItem(voc) == ErrorOutOfEntries and size == 0 . ceq RecGenerateForeignVocSystem(foreignvoc,size,voc) = RecGenerateForeignVocSystem( AddEntryToForeignVocSystem( CorrectWord(GetForeign(GetPair(RandomVocItem(voc)))), foreignvoc), size - 1, SetForeignFlags( CorrectWord(GetForeign(GetPair(RandomVocItem(voc)))), voc)) if not RandomVocItem(voc) == ErrorOutOfEntries and not size == 0 . eq GenerateForeignVocSystem(voc,size) = RecGenerateForeignVocSystem( NewForeignVocSystem(voc),size,voc) . eq GetForeignHead(NewForeignVocSystem(voc)) = ErrorNoWordLeft . eq GetForeignHead(AddEntryToForeignVocSystem(w,foreignvoc)) = w . eq GetForeignTail(NewForeignVocSystem(voc)) = ErrorNoForeignEntriesLeft . eq GetForeignTail(AddEntryToForeignVocSystem(w,foreignvoc)) = foreignvoc . eq MaxForeignScore(NewForeignVocSystem(voc)) = 0 . eq MaxForeignScore(AddEntryToForeignVocSystem(w,foreignvoc)) = MaxForeignScore(foreignvoc) + Length( TranslateIntoNative(GetString(w),GetVocSystem(foreignvoc))) . eq GetMaxForeign(NewForeignVocSystem(voc),output) = output . ceq GetMaxForeign(AddEntryToForeignVocSystem(w,NewForeignVocSystem(voc)),output) = w if output == DummyValue . ceq GetMaxForeign(AddEntryToForeignVocSystem(w,NewForeignVocSystem(voc)),output) = output if not output == DummyValue . ceq GetMaxForeign(foreignvoc,output) = GetMaxForeign( AddEntryToForeignVocSystem(GetForeignHead(foreignvoc), GetForeignTail(GetForeignTail(foreignvoc))), GetForeignHead(foreignvoc)) if not GetForeignHead(foreignvoc) == ErrorNoWordLeft and not GetForeignTail(GetForeignTail(foreignvoc)) == ErrorNoEntriesLeft and not IsStringSmaller(GetString(GetForeignHead(foreignvoc)), GetString(GetForeignHead(GetForeignTail(foreignvoc)))) . ceq GetMaxForeign(foreignvoc,output) = GetMaxForeign(GetForeignTail(foreignvoc),GetForeignHead(GetForeignTail(foreignvoc))) if not GetForeignHead(foreignvoc) == ErrorNoWordLeft and not GetForeignTail(GetForeignTail(foreignvoc)) == ErrorNoEntriesLeft and IsStringSmaller(GetString(GetForeignHead(foreignvoc)), GetString(GetForeignHead(GetForeignTail(foreignvoc)))) . ceq GetOrderedForeignWordList(foreignvoc,forout) = forout if GetForeignHead(foreignvoc) == ErrorNoWordLeft . ceq GetOrderedForeignWordList(foreignvoc,forout) = GetOrderedForeignWordList(DeleteForeignEntry( GetMaxForeign(foreignvoc,DummyValue),foreignvoc), AddEntryToForeignVocSystem(GetMaxForeign(foreignvoc,DummyValue),forout)) if not GetForeignHead(foreignvoc) == ErrorNoWordLeft . eq GetForeignTranslationList(NewForeignVocSystem(voc),lst) = lst . eq GetForeignTranslationList(AddEntryToForeignVocSystem(w,foreignvoc),lst) = GetForeignTranslationList(foreignvoc, AddToItemListsList( TranslateIntoNative(GetString(w), GetVocSystem(foreignvoc)), lst)) . eq GetForeignOrderedItemList(foreignvoc,lst) = GetForeignTranslationList( GetOrderedForeignWordList(foreignvoc, NewForeignVocSystem(GetVocSystem(foreignvoc))), lst) . ** The second vocabulary system is a copy of the original one and keeps all ** data that is lost from the first one as the first vocsystem is emptied ** in order to build the list of all native words . eq GetListOfForeignWords(Dictionary(l1,l2,liEmpty),voc) = NewForeignVocSystem(voc) . eq GetListOfForeignWords(Dictionary(l1,l2,NewItem(it,itlst)),voc) = AddToForeignVoc( CorrectWord( GetForeign(GetPair(it))),GetListOfForeignWords(Dictionary(l1,l2,itlst),voc)) . } } ** ------------------------------------------------ ** Specification of the Test Suite (internal part): ** ------------------------------------------------ module! TestVocSystemSpec { imports { protecting (PreTestVocSystemSpec) protecting (ListOfStringListSpec) protecting (ListOfPairListsSpec) } signature { [ testnativevocsystem testforeignvocsystem ] ** ---------------- ** The Native Part: ** ---------------- op GenerateNativeTest : nativevocsystem Int -> testnativevocsystem { constr } op GetNativeWord : testnativevocsystem -> word op GetMaxNativeScore : testnativevocsystem -> Nat op GetNativeScore : testnativevocsystem -> Int op GetNativeVocSystem : testnativevocsystem -> nativevocsystem op AdaptNativeVocSystem : String testnativevocsystem -> testnativevocsystem op GetNativeStringList : listofitems listofstrings -> listofstrings ** ----------------- ** The Foreign Part: ** ----------------- op GenerateForeignTest : foreignvocsystem Int -> testforeignvocsystem { constr } op GetForeignWord : testforeignvocsystem -> word op GetMaxForeignScore : testforeignvocsystem -> Nat op GetForeignScore : testforeignvocsystem -> Int op GetForeignVocSystem : testforeignvocsystem -> foreignvocsystem op AdaptForeignVocSystem : String testforeignvocsystem -> testforeignvocsystem op GetForeignStringList : listofitems listofstrings -> listofstrings ** ------------------------- ** Miscellaneous Operations: ** ------------------------- op GetPairList : listofitems pairlist -> pairlist op GetListOfPairLists : listoflistofitems listofpairlists -> listofpairlists } axioms { var tnvoc : testnativevocsystem var tfvoc : testforeignvocsystem var nvoc : nativevocsystem var fvoc : foreignvocsystem var pos : Nat var score : Int var str : String var vit : vocitem var ilst : listofitems var illst : listoflistofitems var sllst : listofpairlists var slst : listofstrings var plst : pairlist ** ---------------- ** The Native Part: ** ---------------- eq GetNativeVocSystem(GenerateNativeTest(nvoc,score)) = nvoc . eq GetMaxNativeScore(GenerateNativeTest(nvoc,score)) = MaxNativeScore(nvoc) . eq GetNativeScore(GenerateNativeTest(nvoc,score)) = score . eq GetNativeWord(tnvoc) = GetNativeHead(GetNativeVocSystem(tnvoc)) . ceq AdaptNativeVocSystem(str,tnvoc) = GenerateNativeTest(GetNativeVocSystem(tnvoc), GetNativeScore(tnvoc) - 1) if MakeWord(str,GetForeignLanguage(GetVocSystem(GetNativeVocSystem(tnvoc)))) == ErrorMisspelled . ceq AdaptNativeVocSystem(str,tnvoc) = GenerateNativeTest(GetNativeVocSystem(tnvoc), GetNativeScore(tnvoc) + 1) if not MakeWord(str,GetForeignLanguage(GetVocSystem(GetNativeVocSystem(tnvoc)))) == ErrorMisspelled and MakeItem( MakePair( GetNativeWord(tnvoc), MakeWord(str, GetForeignLanguage(GetVocSystem(GetNativeVocSystem(tnvoc))))), false) in GetItemList(GetVocSystem(GetNativeVocSystem(tnvoc))) . ceq AdaptNativeVocSystem(str,tnvoc) = GenerateNativeTest(GetNativeVocSystem(tnvoc), GetNativeScore(tnvoc) - 1) if not MakeWord(str,GetForeignLanguage(GetVocSystem(GetNativeVocSystem(tnvoc)))) == ErrorMisspelled and not MakeItem( MakePair( GetNativeWord(tnvoc), MakeWord(str, GetForeignLanguage(GetVocSystem(GetNativeVocSystem(tnvoc))))), false) in GetItemList(GetVocSystem(GetNativeVocSystem(tnvoc))) . eq GetNativeStringList(liEmpty,slst) = slst . eq GetNativeStringList(NewItem(vit,ilst),slst) = GetNativeStringList(ilst, AddString(GetNative(GetPair(vit)),slst)) . ** ----------------- ** The Foreign Part: ** ----------------- eq GetForeignVocSystem(GenerateForeignTest(fvoc,score)) = fvoc . eq GetMaxForeignScore(GenerateForeignTest(fvoc,score)) = MaxForeignScore(fvoc) . eq GetForeignScore(GenerateForeignTest(fvoc,score)) = score . eq GetForeignWord(tfvoc) = GetForeignHead(GetForeignVocSystem(tfvoc)) . ceq AdaptForeignVocSystem(str,tfvoc) = GenerateForeignTest(GetForeignVocSystem(tfvoc), GetForeignScore(tfvoc) - 1) if MakeWord(str,GetNativeLanguage(GetVocSystem(GetForeignVocSystem(tfvoc)))) == ErrorMisspelled . ceq AdaptForeignVocSystem(str,tfvoc) = GenerateForeignTest(GetForeignVocSystem(tfvoc), GetForeignScore(tfvoc) + 1) if not MakeWord(str,GetNativeLanguage(GetVocSystem(GetForeignVocSystem(tfvoc)))) == ErrorMisspelled and MakeItem( MakePair( MakeWord(str, GetNativeLanguage(GetVocSystem(GetForeignVocSystem(tfvoc)))), GetForeignWord(tfvoc)), false) in GetItemList(GetVocSystem(GetForeignVocSystem(tfvoc))) . ceq AdaptForeignVocSystem(str,tfvoc) = GenerateForeignTest(GetForeignVocSystem(tfvoc), GetForeignScore(tfvoc) - 1) if not MakeWord(str,GetNativeLanguage(GetVocSystem(GetForeignVocSystem(tfvoc)))) == ErrorMisspelled and not MakeItem( MakePair( MakeWord(str, GetNativeLanguage(GetVocSystem(GetForeignVocSystem(tfvoc)))), GetForeignWord(tfvoc)), false) in GetItemList(GetVocSystem(GetForeignVocSystem(tfvoc))) . eq GetForeignStringList(liEmpty,slst) = slst . eq GetForeignStringList(NewItem(vit,ilst),slst) = GetForeignStringList(ilst, NewString(GetForeign(GetPair(vit)),slst)) . eq GetPairList(liEmpty,plst) = plst . eq GetPairList(NewItem(vit,ilst),plst) = GetPairList(ilst,NewPair(GetPair(vit),plst)) . eq GetListOfPairLists(lliEmpty,sllst) = sllst . eq GetListOfPairLists(NewItemListsList(ilst,illst),sllst) = GetListOfPairLists(illst,NewPairList(GetPairList(ilst,plEmpty),sllst)) . } } ** -------------------------------- ** The Test Suite: ** User Interface. ** ------------------------------- module! StudentDictionarySpec { imports { protecting ( TestVocSystemSpec ) } signature { ** ----------------------------- ** The Score is recorded nicely: ** ----------------------------- [ Score ] op _OutOf_ : Int Nat -> Score { constr } ** -------------------------------------------- ** User Interface for modifying the vocabulary: ** -------------------------------------------- op GenerateDictionary : language language -> vocsystem op AddEntry : String String vocsystem -> vocsystem op DeleteEntry : String String vocsystem -> vocsystem ** ---------------------- ** Translation Utilities: ** ---------------------- op GiveNativeTranslation : String vocsystem -> listofstrings op GiveForeignTranslation : String vocsystem -> listofstrings ** ------------------ ** Display Utilities: ** ------------------ op GetAllTranslationsByNativeOrder : vocsystem -> listofpairlists op GetAllTranslationsByForeignOrder : vocsystem -> listofpairlists ** ------------------- ** Selftest Utilities: ** ------------------- op TestMyNativeKnowledge : Nat vocsystem -> testnativevocsystem op TestMyForeignKnowledge : Nat vocsystem -> testforeignvocsystem op GiveNativeAnswers : listofstrings testforeignvocsystem -> testforeignvocsystem op GiveForeignAnswers : listofstrings testnativevocsystem -> testnativevocsystem op ShowMyScoreInNative : testnativevocsystem testnativevocsystem -> Score op ShowMyScoreInForeign : testforeignvocsystem testforeignvocsystem -> Score } axioms { vars l1 l2 : language vars s1 s2 : String var lst : listofstrings var sdic : vocsystem var no : Nat var tnvoc : testnativevocsystem var nansw : testnativevocsystem var tfvoc : testforeignvocsystem var fansw : testforeignvocsystem eq GenerateDictionary(l1,l2) = Dictionary(l1,l2,liEmpty) . eq AddEntry(s1,s2,sdic) = AddEntryToDictionary(s1,s2,sdic) . eq DeleteEntry(s1,s2,sdic) = DeleteEntryFromDictionary(s1,s2,sdic) . eq GiveNativeTranslation(s1,sdic) = GetNativeStringList(TranslateIntoNative(s1,sdic),lsEmpty) . eq GiveForeignTranslation(s1,sdic) = GetForeignStringList(TranslateIntoForeign(s1,sdic),lsEmpty) . eq GetAllTranslationsByNativeOrder(sdic) = GetListOfPairLists( GetNativeOrderedItemList( GetListOfNativeWords(sdic,sdic), lliEmpty),lplEmpty) . eq GetAllTranslationsByForeignOrder(sdic) = GetListOfPairLists( GetForeignOrderedItemList( GetListOfForeignWords(sdic,sdic), lliEmpty),lplEmpty) . eq TestMyNativeKnowledge(no,sdic) = GenerateNativeTest(GenerateNativeVocSystem(sdic,no),0) . eq TestMyForeignKnowledge(no,sdic) = GenerateForeignTest(GenerateForeignVocSystem(sdic,no),0) . eq GiveNativeAnswers(lsEmpty,tfvoc) = GenerateForeignTest( DeleteForeignEntry( GetForeignHead( GetForeignVocSystem(tfvoc)), GetForeignVocSystem(tfvoc)), GetForeignScore(tfvoc)) . eq GiveNativeAnswers(NewString(s1,lst),tfvoc) = GiveNativeAnswers( lst,AdaptForeignVocSystem(s1,tfvoc)) . eq GiveForeignAnswers(lsEmpty,tnvoc) = GenerateNativeTest( DeleteNativeEntry( GetNativeHead( GetNativeVocSystem(tnvoc)), GetNativeVocSystem(tnvoc)), GetNativeScore(tnvoc)) . eq GiveForeignAnswers(NewString(s1,lst),tnvoc) = GiveForeignAnswers( lst,AdaptNativeVocSystem(s1,tnvoc)) . eq ShowMyScoreInNative(nansw,tnvoc) = GetNativeScore(nansw) OutOf GetMaxNativeScore(tnvoc) . eq ShowMyScoreInForeign(fansw,tfvoc) = GetForeignScore(fansw) OutOf GetMaxForeignScore(tfvoc) . } } ** end of module Specifications ** Testing the implemented modules: open StudentDictionarySpec op EnglishRules : -> rules . eq EnglishRules = AddToRules("qx",AddToRules("uu",rEmpty)) . op GermanRules : -> rules . eq GermanRules = AddToRules("yy",AddToRules("jj",rEmpty)) . op myAlphabet : -> charorder . eq myAlphabet = 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)))))))))))))))))))))))))))))))))))))))))))))))))))) . op German : -> language . eq German = MakeLanguage(GermanRules,myAlphabet) . op English : -> language . eq English = MakeLanguage(EnglishRules,myAlphabet) . op myWord : -> word . eq myWord = MakeWord("hello", English) . op wrongWord : -> word . eq wrongWord = MakeWord("helqxo", English) . op myVocList : -> listofitems . eq myVocList = AddItem(MakeItem(MakePair(MakeWord("hello", English),MakeWord("hallo", German)), false), AddItem(MakeItem(MakePair(MakeWord("bye", English),MakeWord("tschuess", German)), false),liEmpty)) . op English2German : -> vocsystem . eq English2German = AddEntryToDictionary("bye", "servus", AddEntryToDictionary("hello", "hallo", AddEntryToDictionary("bye", "tschuess", Dictionary(English, German, liEmpty)))) . op WrongEnglish2German : -> vocsystem . eq WrongEnglish2German = AddEntryToDictionary("helqxo", "halljjo", AddEntryToDictionary("hello", "hallo", AddEntryToDictionary("bye", "tschuess", Dictionary(English, German, liEmpty)))) . op AnotherWrongEnglish2German : -> vocsystem . eq AnotherWrongEnglish2German = AddEntryToDictionary("hello", "halljjo", AddEntryToDictionary("hello", "hallo", AddEntryToDictionary("bye", "tschuess", Dictionary(English, German, liEmpty)))) . op Entry : -> vocitem . eq Entry = RandomVocItem(English2German) . op ListOfEnglishWords : -> nativevocsystem . eq ListOfEnglishWords = GetListOfNativeWords(English2German,English2German) . op OrderedEnglish2German : -> listoflistofitems . eq OrderedEnglish2German = GetNativeOrderedItemList(ListOfEnglishWords,lliEmpty) . op Maximum : -> word . eq Maximum = GetMaxNative(ListOfEnglishWords,DummyValue) . op Reduced : -> nativevocsystem . eq Reduced = DeleteNativeEntry(CorrectWord("hello"),ListOfEnglishWords) . op MaxScore : -> Nat . eq MaxScore = MaxNativeScore(ListOfEnglishWords) . op NativeTest : -> testnativevocsystem . eq NativeTest = TestMyNativeKnowledge(2,English2German) . op DontKnowFirstAnswer : -> testnativevocsystem . eq DontKnowFirstAnswer = GiveForeignAnswers(lsEmpty,NativeTest) . op AlwaysCheckYourSpelling : -> testnativevocsystem . eq AlwaysCheckYourSpelling = GiveForeignAnswers(AddString("halliio",lsEmpty),NativeTest) . op FirstWordAnsweredCorrect : -> testnativevocsystem . eq FirstWordAnsweredCorrect = GiveForeignAnswers(AddString("hallo",lsEmpty),NativeTest) . op testDict : -> vocsystem . 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)))))))) . op nativeKnowledgeTest : -> testnativevocsystem . eq nativeKnowledgeTest = TestMyNativeKnowledge(4,testDict) . op foreignKnowledgeTest : -> testforeignvocsystem . eq foreignKnowledgeTest = TestMyForeignKnowledge(5,testDict) .