| products/Sources/formale Sprachen/VDM/VDMSL/barSL/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: cdr005.cob Sprache: VDMUntersuchung 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} ¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.36Angebot Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤ |
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
ZieleEntwicklung einer Software für die statische QuellcodeanalyseBot Zugriff |
