Prev Up
Go backward to Specification on lists, pairs and strings
Go up to The Vocabulary system

The global system specification

Specification of a type list
Specification of the types string and pair
An Extended Vocabulary System

Specification of a type list

loose pspec LIST(sort el)
import el;
sorts freely generated
constr []: -> list;
constr add: el x list -> list;
_._: list x list -> list;
length: list -> nat;
_ in _ : el x list -> bool;
reduceList: list -> list;
l, m : list
e1, e2 : el
[].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;


constr [_,_]: el1 x el2 -> pair;
first: pair -> el1;
second: pair -> el2;
a: el1;
b: el2;
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
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
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;
InsertNewEntry([native, foreign], on, of, voc) =
   if [native, foreign] in voc then voc
      if native in on and foreign in of then
          add([native, foreign], voc)
TranslateForeign(foreign, []) = [];
TranslateForeign(foreign, Add([nat1, for1], rest) =
   if foreign == for1 then
      add(nat1, TranslateForeign(foreign, rest))
      translateForeign(foreign, rest)
TranslateNative(native, []) = [];
TranslateNative(native, Add([nat1, for1], rest) =
   if native == nat1 then
      add(nat1, TranslateNative(native, rest))
      TranslateNative(native, rest)
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))
      add([nat1, for1], InsertPairSortedNative([native, foreign], voc))
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))
      add([nat1, for1], InsertPairSortedForeign([native, foreign], voc))
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))
      NumberOfCorrectAnswersN(restn, natTransl)
NumberOfCorrectAnswersF([], forTransl) = 0
NumberOfCorrectAnswersF(add(foreign, restf), forTransl) =
   if foreign in forTransl then
      succ(NumberOfCorrectAnswersF(restf, forTransl))
      NumberOfCorrectAnswersF(restf, forTransl)
end spec

Hong Gu (,
Christian Mittermaier (,
Igor Rents (
February 10, 1999

Prev Up