Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: bag.vdmsl Sprache: VDM

Original von: VDM^©

\section{Modelling of Bags}

\begin{vdm_al}
module BAG

exports

types
  struct Bag;
  struct Elem

functions

  Empty: () -> Bag;
  Add: Elem * Bag -> Bag;
  Remove: Elem * Bag -> Bag;
  Count: Elem * Bag -> nat;
  In: Elem * Bag -> bool;
  Join: Bag * Bag -> Bag;
  Union: Bag * Bag -> Bag;
  SubBag: Bag * Bag -> bool;
  Difference: Bag * Bag -> Bag;
  Size: Bag -> nat;
  Intersection: Bag * Bag -> Bag;
  SeqToBag: seq of Elem -> Bag

values
  baga,bagb: Bag

definitions

types
  Elem = <A> | <B> | <C> | <D> | <E>;
  Bag = map Elem to nat1

functions
  -- Support Functions

  -- Minimum value of a pair of two integers
  Min : nat * nat -> nat
  Min (i, j) ==
    if i < j
    then i
    else j;

  -- Maximum value of a pair of two integers
  Max : nat * nat -> nat
  Max (i, j) ==
    if i > j
    then i
    else j;

  -- Add a sequence of elements, s, to a bag, b,
  -- by adding the head of s,
  -- and making a recursive call
  AuxSeqToBag : seq of Elem * Bag -> Bag
  AuxSeqToBag (s, b) ==
    cases s :
    []         -> b,
    [e] ^ rest -> AuxSeqToBag(rest, Add(e, b))
    end
  measure LenPar1;

  LenPar1 : seq of Elem * Bag -> nat
  LenPar1(list,-) ==
    len list;
\end{vdm_al}

\begin{vdm_al}
  -- Functions Required by Customer
  -- These as described by the user document
  -- (Exercise 7)

  Empty : () -> Bag
  Empty () ==
    { |-> };

  Add : Elem * Bag -> Bag
  Add (e, b) ==
    if e in set dom b
    then b ++ {e |-> b(e) + 1}
    else b ++ {e |-> 1};

  Remove : Elem * Bag -> Bag
  Remove (e, b) ==
    if e in set dom b
    then if b(e) = 1
         then {e} <-: b
         else b ++ {e |-> b(e) - 1}
    else b;

  Count : Elem * Bag -> nat
  Count (e, b) ==
    if e in set dom b
    then b(e)
    else 0;
  -- from given examples, if not in bag then
  -- count = 0, not an error

  In : Elem * Bag -> bool
  In (e, b) ==
    e in set dom b;

  Join : Bag * Bag -> Bag
  Join (b1, b2) ==
    { e |-> Max( Count(e, b1),  Count(e, b2)) |
      e in set (dom b1 union dom b2) };

  Union : Bag * Bag -> Bag
  Union (b1, b2) ==
    {e |-> Count (e, b1) + Count (e, b2) |
     e in set (dom b1 union dom b2)};

  SubBag : Bag * Bag -> bool
  SubBag (b1, b2) ==
    forall e in set dom b1 &
      Count(e, b1) <= Count(e, b2);

  Difference : Bag * Bag -> Bag
  Difference (b1, b2) ==
    {e |-> Count(e, b1) - Count(e, b2)
     |
     e in set dom b1
     &
     Count(e, b1) > Count(e, b2)
    };

  Size : Bag -> nat
  Size (b) ==
    if b = { |-> }
    then 0
    else let e in set dom b
         in
         b(e) + Size ({e} <-: b)
   measure CardDom;

   CardDom: Bag -> nat
   CardDom(b) ==
     card dom b;
\end{vdm_al}

\begin{vdm_al}
  Intersection : Bag * Bag -> Bag
  Intersection (b1, b2) ==
    {e |-> Min (Count(e, b1), Count(e, b2)) |
        -- Design note: Min(...,...) is > 0
        -- as use inter in next line
        -- to ensure both Counts are at least 1
     e in set (dom b1 inter dom b2)
    };

  SeqToBag : seq of Elem -> Bag
  SeqToBag (s) ==
    AuxSeqToBag(s, Empty())

values
  -- The values requested by the customer for tests
  baga : Bag = { <A> |-> 3, <B> |-> 2, <C> |-> 4};
  bagb : Bag = { <A> |-> 1, <C> |-> 5, <D> |-> 4,
                 <E> |-> 1}

end BAG
\end{vdm_al}

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.