Quellcode-Bibliothek Alphabet.vdmpp

class Alphabet

instance variables
  alph : seq of char := [];

inv AlphabetInv(alph)

functions
  AlphabetInv: seq of char -> bool
  AlphabetInv (palph) ==
    len palph mod 2 = 0 and
    card elems palph = len palph

operations
  public Alphabet: seq of char ==> Alphabet
  Alphabet (pa) == alph := pa
  pre AlphabetInv(pa);

  public GetChar: nat ==> char
  GetChar (pidx) == return alph(pidx)
  pre pidx in set inds alph;

  public GetIndex: char ==> nat
  GetIndex (pch) ==
    let pidx in set {i | i in set inds alph
                       & alph(i) = pch} in
      return pidx
  pre pch in set elems alph;

  pure public GetIndices: () ==> set of nat
  GetIndices () == return inds alph;

  public GetSize: () ==> nat
  GetSize () == return len alph;

  public Shift: nat * nat ==> nat
  Shift (pidx, poffset) ==
    if pidx + poffset > len alph
    then return pidx + poffset - len alph
    else return pidx + poffset
  pre pidx in set inds alph and
      poffset <= len alph;

  public Shift: nat ==> nat
  Shift (pidx) == Shift(pidx, 1)
end Alphabet