Go up to Implementation on CafeOBJ
Go forward to Definitions on the vocabulary

## Implementations

module! ENTRY
principal-sort Entry

imports
protecting (STRING)

signature
[ Entry ]
op [_, _] : String String -> Entry constr
op first : Entry -> String
op second : Entry -> String

axioms
vars s1, s2 : String
- -----------
eq first([s1,s2]) = s1 .
eq second([s1,s2]) = s2 .

module! NATIVE-LIST
principal-sort NativeList

imports
protecting (STRING)
protecting (NAT)

signature
[ NativeList ]
op [] : -> NativeList constr
op add : String NativeList -> NativeList constr
op length : NativeList -> Nat
op _in_ : String NativeList -> Bool
op reduceList : NativeList -> NativeList

axioms
var l : NativeList
vars e1, e2 : String
- -----------
eq length([]) = 0 .
eq length(add(e1, l)) = 1 + length(l) .
eq e1 in [] = false .
eq e1 in add(e2, l) = string=(e1, e2) or (e1 in l) .
eq reduceList([]) = [] .
ceq reduceList(add(e1, l)) = reduceList(l) if (e1 in l) .
ceq reduceList(add(e1, l)) = add(e1, reduceList(l)) if not (e1 in l) .

module! FOREIGN-LIST
principal-sort ForeignList

imports
protecting (STRING)
protecting (NAT)

signature
[ ForeignList ]
op [] : -> ForeignList constr
op add : String ForeignList -> ForeignList constr
op length : ForeignList -> Nat
op _in_ : String ForeignList -> Bool
op reduceList : ForeignList -> ForeignList

axioms
var l : ForeignList
vars e1, e2 : String
- -----------
eq length([]) = 0 .
eq length(add(e1, l)) = 1 + length(l) .
eq e1 in [] = false .
eq e1 in add(e2, l) = string=(e1, e2) or (e1 in l) .
eq reduceList([]) = [] .
ceq reduceList(add(e1, l)) = reduceList(l) if (e1 in l) .
ceq reduceList(add(e1, l)) = add(e1, reduceList(l)) if not (e1 in l) .

module! SCORE
principal-sort Score

imports
protecting (NAT)

signature
[ Score ]
op [_, _] : Nat Nat -> Score constr
op first : Score -> Nat
op second : Score -> Nat

axioms
vars s1, s2 : Nat
- -----------
eq first([s1,s2]) = s1 .
eq second([s1,s2]) = s2 .

module! VOCABULARY
principal-sort Vocabulary

imports
protecting (STRING)
protecting (NATIVE-LIST)
protecting (FOREIGN-LIST)
protecting (ENTRY)
protecting (SCORE)
protecting (NAT)

signature

op [] : -> Vocabulary constr
op addE : Entry Vocabulary -> Vocabulary constr
op InsertNewEntry : Entry ForeignList NativeList Vocabulary -> Vocabulary
op TranslateForeign : String Vocabulary -> NativeList
op TranslateNative : String Vocabulary -> ForeignList
op SortNative : Vocabulary -> Vocabulary
op SortForeign : Vocabulary -> Vocabulary
op TestForeign : String NativeList Vocabulary -> Score
op TestNative : String ForeignList Vocabulary -> Score
op OrthoNative : -> NativeList
op OrthoForeign : -> ForeignList
op MyVoc : -> Vocabulary
- hidden operations
op InsertPairSortedNative : Entry Vocabulary -> Vocabulary
op InsertPairSortedForeign : Entry Vocabulary -> Vocabulary
op NumberOfCorrectAnswersN : NativeList NativeList -> Nat
op NumberOfCorrectAnswersF : ForeignList ForeignList -> Nat
op NumberOfPossibleAnswersN : String Vocabulary -> Nat
op NumberOfPossibleAnswersF : String Vocabulary -> Nat

axioms
var native : String
var foreign : String
var on : NativeList
var of : ForeignList
var voc : Vocabulary
var for1 : String
var nat1 : String
var rest : Vocabulary
var natTransl : NativeList
var forTransl : ForeignList
var restn : NativeList
var restf : ForeignList
- -----------------
ceq InsertNewEntry([native, foreign] , of , on , voc) =
addE([native, foreign], voc) if (native in on) and
(foreign in of) .
ceq InsertNewEntry([native, foreign], of, on, voc) = voc
if not (native in on and foreign in of) .

eq TranslateForeign(foreign, []) = [] .
if string=(foreign, for1) .
ceq TranslateForeign(foreign, addE([nat1, for1], rest)) = TranslateForeign(foreign, rest)
if not string=(foreign, for1) .

eq TranslateNative(native, []) = [] .
if string=(native, nat1) .
ceq TranslateNative(native, addE([nat1, for1], rest)) = TranslateNative(native, rest)
if not string=(native, nat1) .

eq SortNative([]) = [] .
InsertPairSortedNative([native, foreign], SortNative(voc)) .

eq InsertPairSortedNative([native, foreign], []) = addE([native, foreign], []) .
ceq InsertPairSortedNative([native, foreign], addE([nat1, for1], voc)) =
if string<=(native, nat1) .
ceq InsertPairSortedNative([native, foreign], addE([nat1, for1], voc)) =
if not string<=(native, nat1) .

eq SortForeign([]) = [] .
InsertPairSortedForeign([native, foreign], SortForeign(voc)) .

eq InsertPairSortedForeign([native, foreign], []) = addE([native, foreign], []) .
ceq InsertPairSortedForeign([native, foreign], addE([nat1, for1], voc)) =
ceq InsertPairSortedForeign([native, foreign], addE([nat1, for1], voc)) =
if not string<=(foreign, for1) .

eq NumberOfCorrectAnswersN([], natTransl) = 0 .
if not (native in natTransl) .

eq NumberOfPossibleAnswersN(foreign, voc) = length(TranslateForeign(foreign, voc)) .

eq NumberOfCorrectAnswersF([], forTransl) = 0 .