The global system specification

Specification of a type list

loose pspec LIST(sort el)

import el;

sorts freely generated

list;

opns:

constr []: -> list;

constr add: el x list -> list;

_._: list x list -> list;
length: list -> nat;

_ in _ : el x list -> bool;
reduceList: list -> list;

vars:

l, m : list

e1, e2 : el

axioms:

[].l = l;
l.[] = l;
add(e1, l).m = add(e1,l.m);

length([]) = 0;
length(add(e1, l)) = succ(length(l));

e1 in [] = false;
e1 in add(e2, l) = (e1 == e2) or e1 in l;

reduceList([]) = [];

reduceList(add(e1, l)) =
    if e1 in l then reduceList(l)
    else add(e1,reduceList(l));

end spec

Specification of the types string and pair

loose pspec STRING(sort char)

import char;

import (LIST(char) rename sort list opns [] to sort string, opn "");

end spec

loose pspec PAIR(sort el1, el2)

import el1;

import el2;

sorts freely generated pair;

opns:

constr [_,_]: el1 x el2 -> pair;

first: pair -> el1;

second: pair -> el2;

vars:

a: el1;

b: el2;

axioms:

first([a, b]) = a;

second([a, b]) = b;

end spec

An Extended Vocabulary System

pspec VOCABULARY-SYSTEM(sort natChar, forChar)

first we import all necessary datatypes and do some renaming the vocabulary is a list of pairs native words and foreign words. All datatypes we need are strings, lists and pairs

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);

next we define the operations on the vocabulary system

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

the hidden operations are for internal use only

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

vars:

native: nativeString;

foreign: foreignString;

on: nativeList;

of: foreignList;

voc: vocabulary;

for1: foreignString;

nat1: nativeString;

rest: vocabulary;

natAnswers: nativeList;

forAnswers: foreignList;

natTransl: nativeList;

forTransl: foreignList;

restn: nativeList;

restf: foreignList;

axioms:

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;

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

TranslateNative(native, []) = [];
TranslateNative(native, Add([nat1, for1], rest) =
   if native == nat1 then
      add(nat1, TranslateNative(native, rest))
   else
      TranslateNative(native, rest)
   endif;

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;

SortForeign([]) = [];
SortForeign(add([native, foreign], voc)) =
   InsertPairSortedForeign([native, foreign], SortForeign(voc));

InsertPairSortedForeign([native, foreign], []) =     add([native, foreign], []);

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

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

TestNative(native, forAnswers, voc) =
   [NumberOfCorrectAnswersF(reduceList(ForAnswers), TranslateNative(Native, voc)), NumberOfPossibleAnswersNative(native, voc)];

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

NumberOfPossibleAnswersN(native, voc) =
   length(TranslateNative(native, voc));

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

NumberOfCorrectAnswersF([], forTransl) = 0
NumberOfCorrectAnswersF(add(foreign, restf), forTransl) =
   if foreign in forTransl then
      succ(NumberOfCorrectAnswersF(restf, forTransl))
   else
      NumberOfCorrectAnswersF(restf, forTransl)
   endif;

end spec