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 natAnswers : NativeList
var forAnswers : ForeignList
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, []) = [] .
ceq TranslateForeign(foreign, addE([nat1, for1], rest)) =
add(nat1, TranslateForeign(foreign, rest))
if string=(foreign, for1) .
ceq TranslateForeign(foreign, addE([nat1, for1], rest)) =
TranslateForeign(foreign, rest)
if not string=(foreign, for1) .
eq TranslateNative(native, []) = [] .
ceq TranslateNative(native, addE([nat1, for1], rest)) =
add(for1, TranslateNative(native, rest))
if string=(native, nat1) .
ceq TranslateNative(native, addE([nat1, for1], rest)) =
TranslateNative(native, rest)
if not string=(native, nat1) .
eq SortNative([]) = [] .
eq SortNative(addE([native, foreign], voc)) =
InsertPairSortedNative([native, foreign],
SortNative(voc)) .
eq InsertPairSortedNative([native, foreign], []) =
addE([native, foreign], []) .
ceq InsertPairSortedNative([native, foreign], addE([nat1, for1],
voc)) =
addE([native, foreign], addE([nat1, for1], voc))
if string<=(native, nat1) .
ceq InsertPairSortedNative([native, foreign], addE([nat1, for1],
voc)) =
addE([nat1, for1], InsertPairSortedNative([native,
foreign], voc))
if not string<=(native, nat1) .
eq SortForeign([]) = [] .
eq SortForeign(addE([native, foreign], voc)) =
InsertPairSortedForeign([native, foreign],
SortForeign(voc)) .
eq InsertPairSortedForeign([native, foreign], []) =
addE([native, foreign], []) .
ceq InsertPairSortedForeign([native, foreign], addE([nat1, for1],
voc)) =
addE([native, foreign], addE([nat1, for1], voc))
if string<=(foreign, for1) .
ceq InsertPairSortedForeign([native, foreign], addE([nat1, for1],
voc)) =
addE([nat1, for1], InsertPairSortedForeign([native,
foreign], voc))
if not string<=(foreign, for1) .
eq TestForeign(foreign, natAnswers, voc) =
[NumberOfCorrectAnswersN(reduceList(natAnswers),
TranslateForeign(foreign,voc)),
NumberOfPossibleAnswersF(foreign, voc)] .
eq NumberOfCorrectAnswersN([], natTransl) = 0 .
ceq NumberOfCorrectAnswersN(add(native, restn), natTransl) =
1 + NumberOfCorrectAnswersN(restn, natTransl)
if native in natTransl .
ceq NumberOfCorrectAnswersN(add(native, restn), natTransl) =
NumberOfCorrectAnswersN(restn, natTransl)
if not (native in natTransl) .
eq NumberOfPossibleAnswersN(foreign, voc) = length(TranslateForeign(foreign, voc)) .
eq TestNative(native, forAnswers, voc) =
[NumberOfCorrectAnswersF(reduceList(forAnswers),
TranslateNative(nativen,voc)),
NumberOfPossibleAnswersN(native, voc)] .
eq NumberOfCorrectAnswersF([], forTransl) = 0 .
ceq NumberOfCorrectAnswersF(add(foreign, restf), forTransl) =
1 + NumberOfCorrectAnswersF(restf, forTransl)
if foreign in forTransl .
ceq NumberOfCorrectAnswersF(add(foreign, restf), forTransl) =
NumberOfCorrectAnswersF(restf, forTransl)
if not (foreign in forTransl) .
eq NumberOfPossibleAnswersF(native, voc) = length(TranslateNative(native, voc)) .