Topdown analysis

The vocabulary system is a list of pairs of strings, namely native and foreign words while the set of all possible native and foreign words are given by thvocabulary finite concatenations of native or foreign characters. This system will only considers those words which are orthographically correct and actually belong to the language according to the given set OrthoNative and OrthoForeign.

• The signature of the specification starting with importing all necessary datatypes and doing some renaming.

  pspec VOCABULARY-SYSTEM(sort NatChar ForChar)
  import NAT-CHAR;
  import FOR-CHAR;
  import NAT-AND-BOOL;
  import (STRING(NatChar) rename string to nativeString);
  import (STRING(ForChar) rename string to foreignString);
  import (PAIR(nativeString, foreignString) rename pair to entry);
  import (LIST(nativeString) rename list to nativelist);
  import (LIST(foreignString) rename list to ForeignList);
  import (PAIR(nat, nat) rename pair to score);
  import (LIST(entry) rename list to vocabulary);
  freely generated sorts vocabulary;

• The operators can be divided into the visible operations and the hidden operations which are only for internal use.

  opns:

  InsertNewEntry: entry x foreignList x nativeList x vocabulary -> vocabulary
  TranslateForeign: foreignString x vocabulary -> nativeList
  TranslateNative: nativeString x vocabulary -> foreignList
  SortNative: vocabulary -> vocabulary
  SortForeign: vocabulary -> vocabulary
  TestForeign: foreignString x nativeList x vocabulary -> score
  TestNative: nativeString x foreignList x vocabulary -> score
  OrthoNative: -> nativeList
  OrthoForeign: -> foreignList

  hidden opns:

  InsertPairSortedNative: entry x vocabulary -> vocabulary
  InsertPairSortedForeign: entry x vocabulary -> vocabulary
  NumberOfCorrectAnswersN: nativeList x nativeList -> nat
  NumberOfPossibleAnswersN: nativeString x vocabulary -> nat
  NumberOfCorrectAnswersF: foreignList x foreignList -> nat
  NumberOfPossibleAnswersF: foreignString x vocabulary -> nat

  The overloading of operaters is possible in order to avoid extensive use of rename which does not provide any essential information for the solution of this problem.

• The axioms can be divide into those axioms for

  1. New entering:

     InsertNewEntry([native, foreign], on, of, voc) =
            if [native, foreign] in voc then voc
           else
                  if native in on and foreign in of then
                         add([native, foreign], voc)
                  else
                        voc
                  endif
           endif;
     

  2. Translations: (for example, Foreign -> Native)

     TranslateForeign(foreign, []) = [];
     TranslateForeign(foreign, Add([nat1, for1], rest) =
            if foreign == for1 then
                  add(nat1, TranslateForeign(foreign, rest))
           else
                  translateForeign(foreign, rest)
           endif;

  3. Sorting: (for example, Sort Nativeword list)

     SortNative([]) = [];
     SortNative(add([native, foreign], voc)) =
            InsertPairSortedNative([native, foreign], SortNative(voc));

     InsertPairSortedNative([native, foreign], []) =
            add([native, foreign], []);
     InsertPairSortedNative([native, foreign], add([nat1, for1], voc)) =
            if native <= nat1 then
                  add([native, foreign], add([nat1, for1], voc))
           else
                  add([nat1, for1], InsertPairSortedNative([native, foreign], voc))
           endif;

  4. Testing:

     TestForeign(foreign, natAnswers, voc) =
            [NumberOfCorrectAnswersN(reduceList(natAnswers), TranslateForeign(foreign, voc)), NumberOfPossibleAnswersForeign(foreign, voc)];

     NumerbOfPossibleAnswersF(foreign, voc) =
            length(TranslateForeign(foreign, voc));

     NumberOfCorrectAnswersN([], natTransl) =0;
     NumberOfCorrectAnswersN(add(native, restn), natTransl)=
            if native in natTransl        then
                  succ(NumberOfCorrectAnswersN(restn, natTransl))
           else
                  NumberOfCorrectAnswersN(restn, natTransl)
           endif;