Anforderungen  |   Konzepte  |   Entwurf  |   Entwicklung  |   Qualitätssicherung  |   Lebenszyklus  |   Steuerung
 
 
 
 


Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei:   Sprache: VDM

Untersuchung VDM©

class GroupPhase

values

secondRoundWinners = [<A>,<B>,<C>,<D>,<E>,<F>,<G>,<H>];
secondRoundRunnersUp = [<B>,<A>,<D>,<C>,<F>,<E>,<H>,<G>]


types

public Team = <Brazil> | <Norway> | <Morocco> | <Scotland> |
       <Italy> | <Chile> | <Austria> | <Cameroon> |
       <France> | <Denmark> | <SouthAfrica> | <SaudiArabia> | 
       <Nigeria> | <Paraguay> | <Spain> | <Bulgaria> |
       <Holland> | <Mexico> | <Belgium> | <SouthKorea> |
       <Germany> | <Yugoslavia> | <Iran> | <UnitedStates> |
       <Rumania> | <England> | <Colombia> | <Tunisia> |
       <Argentina> | <Croatia> | <Jamaica> | <Japan>;

public GroupName = <A> | <B> | <C> | <D> | <E> | <F> | <G> | <H>;
       

Score :: team : Team
         won : nat
         drawn : nat
         lost : nat
         points : nat
inv sc == sc.points = 3 * sc.won + sc.drawn;





instance variables
  gps : map GroupName to set of Score :=
        { <A> |-> sc_init ({<Brazil>, <Norway>, <Morocco>, <Scotland>}),
          <B> |-> sc_init ({<Italy>, <Chile>, <Austria>, <Cameroon>}),
          <C> |-> sc_init ({<France>, <Denmark>, <SouthAfrica>,<SaudiArabia>}),
          <D> |-> sc_init ({ <Nigeria>, <Paraguay>, <Spain>, <Bulgaria>}),
          <E> |-> sc_init ({ <Holland>, <Mexico>, <Belgium>, <SouthKorea>}),
          <F> |-> sc_init ({<Germany>, <Yugoslavia>, <Iran>, <UnitedStates>}),
          <G> |-> sc_init ({<Rumania>, <England>, <Colombia>, <Tunisia>}),
          <H> |-> sc_init ({<Argentina>, <Croatia>, <Jamaica>, <Japan>})};
inv forall gp in set rng gps & 
      (card gp = 4 and
       forall sc in set gp & sc.won + sc.lost + sc.drawn <= 3)

functions

sc_init : set of Team -> set of Score
sc_init (ts) ==
  { mk_Score (t,0,0,0,0) | t in set ts };

clear_winner : set of Score -> bool
clear_winner (scs) ==
  exists sc in set scs & 
    forall sc' in set scs \ {sc} & sc.points > sc'.points;

winner_by_more_wins : set of Score -> bool
winner_by_more_wins (scs) ==
  exists sc in set scs &
    forall sc' in set scs \ {sc} &
      (sc.points > sc'.points) or
      (sc.points = sc'.points and sc.won > sc'.won)



operations

public Win : Team * Team ==> ()
Win (wt,lt) ==
  let gp in set dom gps be st {wt,lt} subset {sc.team | sc in set gps(gp)}
  in gps := gps ++ { gp |-> 
                         { if sc.team = wt
                           then mu(sc, won |-> sc.won + 1,
                                       points |-> sc.points + 3)
                           else if sc.team = lt
                           then mu(sc, lost |-> sc.lost + 1)
                           else sc 
                                   | sc in set gps(gp)}}
pre exists gp in set dom gps & {wt,lt} subset {sc.team | sc in set gps(gp)};

Win2 (wt,lt: Team)
ext wr gps : map GroupName to set of Score
pre exists gp in set dom gps & 
        {wt,lt} subset {sc.team | sc in set gps(gp)}
post exists gp in set dom gps &
       {wt,lt} subset {sc.team | sc in set gps(gp)}
       and gps = gps~ ++ 
                     { gp |-> 
                       {if sc.team = wt
                        then mu(sc, won |-> sc.won + 1,
                                    points |-> sc.points + 3)
                        else if sc.team = lt
                        then mu(sc, lost |-> sc.lost + 1)
                        else sc 
                   | sc in set gps(gp)}};

GroupWinner (gp:GroupName) t:Team
ext rd gps : map GroupName to set of Score
pre gp in set dom gps
post t in set {sc.team | sc in set gps(gp)} and
     let sct = iota sc in set gps(gp) & sc.team = t 
     in 
       forall sc in set gps(gp) &
         sc.team <> t => sct.points > sc.points or
                         sct.points = sc.points and sct.won > sc.won;

GroupRunnerUp (gp:GroupName) t:Team
ext rd gps : map GroupName to set of Score
pre gp in set dom gps
post let sc' in set gps(gp) be st
       true --post_GroupWinner(gp,sc'.team,gps,gps)
     in t in set {sc.team | sc in set gps(gp) \ {sc'}} and
        let sct = iota sc in set gps(gp) \ {sc'} & sc.team = t
        in forall sc in set gps(gp) \ {sc'} &
         sc.team <> t => sct.points > sc.points or
                         sct.points = sc.points and sct.won > sc.won;

-- let stmt - lots of examples presumably
GroupWinner_expl : GroupName ==> Team
GroupWinner_expl (gp) ==
  let sc in set gps(gp) be st
     forall sc' in set gps(gp) \ {sc} &
        (sc.points > sc'.points) or
        (sc.points = sc'.points and sc.won > sc'.won)
  in return sc.team
pre gp in set dom gps;

GroupRunnerUp_expl : GroupName ==> Team
GroupRunnerUp_expl (gp) ==
  def t = GroupWinner(gp)
  in let sct = iota sc in set gps(gp) & sc.team = t
     in 
       let sc in set gps(gp) \ {sct} be st
         forall sc' in set gps(gp) \ {sc,sct} &
           (sc.points > sc'.points) or
           (sc.points = sc'.points and sc.won > sc'.won)
       in return sc.team
pre gp in set dom gps;

-- def stmt
SecondRound_expl : () ==> seq of (Team * Team)
SecondRound_expl () ==
  def winners = { gp |-> GroupWinner_expl(gp) | gp in set dom gps };
      runners_up = { gp |-> GroupRunnerUp_expl(gp) | gp in set dom gps}
  in return ([mk_(winners(secondRoundWinners(i)),
                  runners_up(secondRoundRunnersUp(i))) | i in set {1,...,8}]);


-- assignment to state designator
--  c.f. earlier version of Win
Win_sd : Team * Team ==> ()
Win_sd (wt,lt) ==
  let gp in set dom gps be st {wt,lt} subset {sc.team | sc in set gps(gp)}
  in gps(gp) := { if sc.team = wt
                  then mu(sc, won |-> sc.won + 1,
                              points |-> sc.points + 3)
                  else if sc.team = lt
                  then mu(sc, lost |-> sc.lost + 1)
                  else sc 
                      | sc in set gps(gp)}
pre exists gp in set dom gps & {wt,lt} subset {sc.team | sc in set gps(gp)};


-- conditional statements

GroupWinner_if : GroupName ==> Team
GroupWinner_if (gp) ==
  if clear_winner(gps(gp))
  then return ((iota sc in set gps(gp) &
                 forall sc' in set gps(gp) \ {sc} &
                   sc.points > sc'.points).team)
  else if winner_by_more_wins(gps(gp))
       then return ((iota sc in set gps(gp) &
                 forall sc' in set gps(gp) \ {sc} &
                   (sc.points > sc'.points) or
                   (sc.points = sc'.points and sc.won > sc'.won)).team)
  else RandomElement ( {sc.team | sc in set gps(gp) &
                         forall sc' in set gps(gp) &
                          sc'.points <= sc.points} )
pre gp in set dom gps;

RandomElement : set of Team ==> Team
RandomElement (ts) ==
  (dcl t:Team := let t' in set ts in t';
   return (t));

public GroupWinner_cases : GroupName ==> Team
GroupWinner_cases (gp) ==
  cases true:
    (clear_winner(gps(gp))) -> 
         return ((iota sc in set gps(gp) &
                   forall sc' in set gps(gp) \ {sc} &
                    sc.points > sc'.points).team),

    (winner_by_more_wins(gps(gp))) ->
         return ((iota sc in set gps(gp) &
                   forall sc' in set gps(gp) \ {sc} &
                     (sc.points > sc'.points) or
                     (sc.points = sc'.points and sc.won > sc'.won)).team),

    others -> RandomElement ( {sc.team | sc in set gps(gp) &
                                forall sc' in set gps(gp) &
                                 sc'.points <= sc.points} )
  end
pre gp in set dom gps;

-- for loops
GroupWinners: () ==> set of Team
GroupWinners () ==
  (dcl winners : set of Team := {};
   for all gp in set dom gps do
     (dcl winner: Team := GroupWinner(gp);
      winners := winners union {winner}
     );
   return winners
   );

end GroupPhase
class UseGP

instance variables

  gp : GroupPhase := new GroupPhase()

traces

    InitBeforePlay : 
    let t1 in set {<Brazil>, <Norway>, <Morocco>, <Scotland>}
    in
      let t2 in set {<Brazil>, <Norway>, <Morocco>, <Scotland>} \ {t1}
      in
        let t3 in set {<Brazil>, <Norway>, <Morocco>, <Scotland>} \ {t1,t2}
        in
          let t4 in set {<Brazil>, <Norway>, <Morocco>, <Scotland>} \ {t1,t2,t3}
          in
            (gp.Win(t1,t2);gp.Win(t1,t3);gp.Win(t1,t4);gp.Win(t2,t3);
             gp.Win(t2,t4);gp.Win(t3,t4);gp.GroupWinner_cases(<A>)
            )
            

end UseGP

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





Kontakt
Drucken
Kontakt
Hier finden Sie eine Liste der Produkte des Unternehmens

Mittel




schauen Sie vor die Tür

Fenster


Die Firma ist wie angegeben erreichbar.

Entwicklung einer Software für die statische Quellcodeanalyse


Bot Zugriff



                                                                                                                                                                                                                                                                                                                                                                                                     


Neuigkeiten

     Aktuelles
     Motto des Tages

Software

     Produkte
     Quellcodebibliothek

Aktivitäten

     Artikel über Sicherheit
     Anleitung zur Aktivierung von SSL

Muße

     Gedichte
     Musik
     Bilder

Jenseits des Üblichen ....
    

Besucherstatistik

Besucherstatistik