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


Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/VDM/VDMPP/webserverPP/ (Beweissystem der NASA Version 6.0.9^©) Datei vom 13.4.2020 mit Größe 109 B

SSL bar.vdmsl Interaktion und
PortierbarkeitVDM

\section{Modelling of a Bar}

\begin{vdm_al}
module BAR
imports

from BAG

types
 Bag;
 Elem = <A> | | <C> | <D> | <E>

functions

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

values
 baga:BAG`Bag;
 bagb: BAG`Bag

exports all

definitions

types
 Drink = BAG`Elem;
 Cellar = BAG`Bag;
 -- i.e. various quantities of various drinks
 Bar = BAG`Bag; -- as cellar
 Supplier = seq of char;
 -- Don't care about representation of suppliers
 Pub = Cellar * Bar;
 -- all that matters is the drink stocks in the pub
 BarLevel = BAG`Bag;
 -- target stocking level of bar
 CellarLevel = BAG`Bag;
 -- target stocking level of cellar
 Stock = BAG`Bag;
 Order = BAG`Bag
\end{vdm_al}

\begin{vdm_al}
functions
 -- Buy an arbitrary amount of stock from
 -- a supplier, assuming they have it
 BuyStock : map Supplier to Stock * Supplier *
 Order * Pub -> Pub
 BuyStock (supps, s, stock, mk_(c,r)) ==
 mk_(BAG`Union (c, stock), r )
 pre s in set dom supps and
 BAG`SubBag( stock, supps(s));

 -- Given a level of bar stocking,
 -- try refilling the bar from the cellar,
 -- doing the best possible
 RestockBar : Pub * BarLevel -> Pub
 RestockBar (mk_(c,r), bl) ==
 let missing = BAG`Difference(bl, r)
 in
 let can_restock = BAG`Intersection(missing, c)
 in
 mk_(BAG`Difference(c, can_restock),
 BAG`Union(r, can_restock));

 -- A patron buys a round (list) of drinks from the bar
 Round : seq of Drink * Pub -> Pub
 Round (sold, mk_(c,r)) ==
 mk_(c,
 BAG`Difference(r, BAG`SeqToBag(sold))
 )
 pre BAG`SubBag(BAG`SeqToBag(sold), r);
\end{vdm_al}

\begin{vdm_al}
 -- Given a map of suppliers and what they have,
 -- work through the list of suppliers until either
 -- filled requirements of cellar level or run out
 -- of suppliers
 RestockCellar : CellarLevel * Pub *
 map Supplier to Stock -> Pub
 RestockCellar (cl, mk_(c, r), sb) ==
 if sb = { |-> }
 then mk_(c, r)
 else
 let s in set dom sb
 in
 let missing = BAG`Difference(cl, c)
 in
 if BAG`Size(missing) > 0
 then
 let can_restock = BAG`Intersection(missing, sb(s))
 in
 RestockCellar(cl,
 mk_(BAG`Union(c, can_restock), r),
 {s} <-: sb)
 else
 mk_(c, r)
 measure CardCellar;

 CardCellar: CellarLevel * Pub *
 map Supplier to Stock -> nat
 CardCellar(-,-,sb) ==
 card dom sb;

 -- Sell one drink to a patron
 Drink1 : Drink * Pub -> Pub
 Drink1 (dr, mk_(c,r)) ==
 mk_(c,
 BAG`Remove(dr, r))
 pre BAG`In(dr, r);

 -- The pub is devoid of alcohol
 Disaster : Pub -> bool
 Disaster (mk_(c,r)) ==
 c = BAG`Empty() and r = BAG`Empty();

 -- Return by a patron of an unopenned bottle
 Unwanted : Drink * Pub -> Pub
 Unwanted (dr, mk_(c,r)) ==
 mk_(c,
 BAG`Add(dr, r));

 -- Work out the highest single stock for
 -- each kind of drink
 HighestStock : map Supplier to Stock -> BAG`Bag
 HighestStock (supps) ==
 if dom supps = {}
 then BAG`Empty()
 else
 let s in set dom supps
 in
 BAG`Join(supps(s), HighestStock({s} <-: supps))
 measure CardDom;

 CardDom: map Supplier to Stock -> nat CardDom(m) ==
 card dom m;

 -- How many drinks are there in the pub
 TotalDrinks : Pub -> nat
 TotalDrinks (mk_(c,r)) ==
 BAG`Size(c) + BAG`Size(r)

values -- introduced for the purposes of testing
 cellarlevel1 = {<A> |-> 5, |-> 5, <C> |-> 3};
 barlevel1 = {<A> |-> 2, |-> 2, <C> |-> 5};
 cellar1 = {<A> |-> 8, |-> 5, <C> |-> 4};
 cellar2 = { |-> 1, <C> |-> 4};
 bar1 = {<A> |-> 2, |-> 3, <C> |-> 6};
 bar2 = {<A> |-> 3, <C> |-> 2};
 bar3 = {<A> |-> 3, |-> 3};
 pub1 = mk_(cellar1, bar1);
 pub2 = mk_(cellar1, bar2);
 pub3 = mk_(cellar2, bar1);
 pub4 = mk_(cellar2, bar2);
 pub5 = mk_(cellar1, bar3);
 supps1 = {"Fizz" |-> {<A> |-> 10},
 "Real" |-> { |-> 10, <C> |-> 2},
 "Scrumpy" |-> { |-> 1, <C> |-> 10}};
 supps2 = {"Fizz" |-> {<A> |-> 10},
 "Real" |-> { |-> 1, <C> |-> 5},
 "Scrumpy" |-> { |-> 1, <C> |-> 10}}

end BAR
\end{vdm_al}

quality100%

¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.10Angebot Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤

*Eine klare Vorstellung vom Zielzustand

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.