Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/Sources/formale Sprachen/VDM/VDMSL/barSL/ (Wiener Entwicklungsmethode ^©) Datei vom 13.4.2020 mit Größe 3 kB

Quelle bag.vdmsl Sprache: 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}

quality99%

¤ Dauer der Verarbeitung: 0.12 Sekunden (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.