Quellcode-Bibliothek gateway.vdmsl Sprache: VDM

-- A trusted gateway
-- For Chapter 7 (Sequences)

types

  String = seq of char
  inv s == s <> [];

  Message = String
  inv m == len m <= 100;

  Classification = <HI> | <LO>;

  Category = set of String;

  Ports :: high: seq of Message
           low : seq of Message

functions

-- checking whether a substring occur in another string

  Occurs: String * String -> bool
  Occurs(substr,str) ==
    exists i,j in set inds str & substr = str(i,...,j);

-- Classifying messages

  Classify: Message * Category -> Classification
  Classify(m,cat) ==
    if exists hi in set cat & Occurs(hi,m)
    then <HI>
    else <LO>;

-- The main gateway function using recursion

  Gateway: seq of Message * Category -> Ports
  Gateway(ms,cat) ==
    if ms = []
    then mk_Ports([],[])
    else let rest_p = Gateway(tl ms,cat)
         in
           ProcessMessage(hd ms,cat,rest_p)
   measure MesLen;

   MesLen: seq of Message * Category -> nat
   MesLen(list,-) ==
     len list;

-- Classify the message and add to the appropriate port.

  ProcessMessage: Message * Category * Ports -> Ports
  ProcessMessage(m,cat,ps) ==
    if Classify(m,cat) = <HI>
    then mk_Ports([m]^ps.high,ps.low)
    else mk_Ports(ps.high,[m]^ps.low);

-- The main gateway function without using recursion

  Gateway2: seq of Message * Category -> Ports
  Gateway2(ms,cat) ==
    mk_Ports([m|m in seq ms & Classify(m,cat) = <HI>],
             [m|m in seq ms & Classify(m,cat) = <LO>]);

-- Functions illustrating other sequence operators.

  AnyHighClass: seq of Message * Category -> bool
  AnyHighClass(ms,cat) ==
    exists m in seq ms & Classify(m,cat) = <HI>;

  Censor: seq of Message * Category -> seq of Message
  Censor(ms,cat) ==
    [m | m in seq ms & Classify(m,cat) = <LO>];

  FlattenMessages: seq of Message -> Message
  FlattenMessages(ms) ==
    conc ms
  pre len conc ms <= 100

quality100%

¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.0Bemerkung: (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.