class GroupPhase

values

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

types

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;

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

Score :: team : Team
won : ℕ
drawn : ℕ
lost : ℕ
points : ℕ

inv sc \underline{△} sc.points = 3 × sc.won + sc.drawn

instance variables

gps : GroupName →^{m} Score-set := {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 ∀ gp ∈ rng gps ·

(card gp = 4 ∧ ∀ sc ∈ gp · sc.won + sc.lost + sc.drawn ≤ 3)

functions

sc-init : Team-set → Score-set sc-init (ts) \underline{△}

{mk-Score (t, 0, 0, 0, 0) | t ∈ ts}; clear-winner : Score-set → 𝔹 clear-winner (scs) \underline{△}

∃ sc ∈ scs · ∀ sc′ ∈ scs \ {sc} · sc.points > sc′.points; winner-by-more-wins : Score-set → 𝔹 winner-by-more-wins (scs) \underline{△}

∃ sc ∈ scs ·

∀ sc′ ∈ scs \ {sc} · (sc.points > sc′.points) ∨ (sc.points = sc′.points ∧ sc.won > sc′.won)

operations

Win : Team × Team →^{o} () Win (wt, lt) \underline{△}

let gp ∈ dom gps be st {wt, lt} ⊆ {sc.team | sc ∈ gps (gp)} in gps := gps † {gp ↦

{if sc.team = wt then μ (sc, won ↦ sc.won + 1,

points ↦ sc.points + 3)

else if sc.team = lt then μ (sc, lost ↦ sc.lost + 1) else sc | sc ∈ gps (gp)}}

pre ∃ gp ∈ dom gps · {wt, lt} ⊆ {sc.team | sc ∈ gps (gp)} ; Win2 (wt, lt : Team)ext wr gps : GroupName →^{m} Score-set

pre ∃ gp ∈ dom gps · {wt, lt} ⊆ {sc.team | sc ∈ gps (gp)} post ∃ gp ∈ dom gps · {wt, lt} ⊆ {sc.team | sc ∈ gps (gp)} ∧

gps = \begin{matrix}↼− \\ gps \end{matrix} †

{gp ↦

{if sc.team = wt then μ (sc, won ↦ sc.won + 1,

points ↦ sc.points + 3)

else if sc.team = lt then μ (sc, lost ↦ sc.lost + 1) else sc | sc ∈ gps (gp)}};

GroupWinner (gp:GroupName) t:Teamext rd gps : GroupName →^{m} Score-set

pre gp ∈ dom gps post t ∈ {sc.team | sc ∈ gps (gp)} ∧ let sct = ι sc ∈ gps (gp) · sc.team = t in ∀ sc ∈ gps (gp) ·

sc.team ≠ t ⇒ sct.points > sc.points ∨ sct.points = sc.points ∧ sct.won > sc.won;

GroupRunnerUp (gp:GroupName) t:Teamext rd gps : GroupName →^{m} Score-set pre gp ∈ dom gps post let sc′ ∈ gps (gp) in

t ∈ {sc.team | sc ∈ gps (gp) \ {sc′}} ∧

let sct = ι sc ∈ gps (gp) \ {sc′} · sc.team = t in ∀ sc ∈ gps (gp) \ {sc′} ·

sc.team ≠ t ⇒ sct.points > sc.points ∨ sct.points = sc.points ∧ sct.won > sc.won;

GroupWinner-expl : GroupName →^{o} Team GroupWinner-expl (gp) \underline{△}

let sc ∈ gps (gp) be st

∀ sc′ ∈ gps (gp) \ {sc} · (sc.points > sc′.points) ∨ (sc.points = sc′.points ∧ sc.won > sc′.won) in

return sc.team pre gp ∈ dom gps ; GroupRunnerUp-expl : GroupName →^{o} Team GroupRunnerUp-expl (gp) \underline{△}

def t = GroupWinner (gp) in

let sct = ι sc ∈ gps (gp) · sc.team = t in

let sc ∈ gps (gp) \ {sct} be st

∀ sc′ ∈ gps (gp) \ {sc, sct} · (sc.points > sc′.points) ∨ (sc.points = sc′.points ∧ sc.won > sc′.won) in

return sc.team pre gp ∈ dom gps ; SecondRound-expl : () →^{o} (Team × Team)^{∗} SecondRound-expl () \underline{△}

def winners = {gp ↦ GroupWinner-expl (gp) | gp ∈ dom gps};

runners-up = {gp ↦ GroupRunnerUp-expl (gp) | gp ∈ dom gps}

in

return ([mk- (winners (secondRoundWinners (i)), runners-up (secondRoundRunnersUp (i))) | i ∈ {1, …, 8}]);

Win-sd : Team × Team →^{o} () Win-sd (wt, lt) \underline{△}

let gp ∈ dom gps be st {wt, lt} ⊆ {sc.team | sc ∈ gps (gp)} in gps(gp) := {if sc.team = wt

then μ (sc, won ↦ sc.won + 1,

points ↦ sc.points + 3)

else if sc.team = lt then μ (sc, lost ↦ sc.lost + 1) else sc | sc ∈ gps (gp)}

pre ∃ gp ∈ dom gps · {wt, lt} ⊆ {sc.team | sc ∈ gps (gp)} ; GroupWinner-if : GroupName →^{o} Team GroupWinner-if (gp) \underline{△}

if clear-winner (gps (gp))

then return ((ι sc ∈ gps (gp) ·

∀ sc′ ∈ gps (gp) \ {sc} ·

sc.points > sc′.points).team)

else if winner-by-more-wins (gps (gp))

then return ((ι sc ∈ gps (gp) ·

∀ sc′ ∈ gps (gp) \ {sc} · (sc.points > sc′.points) ∨ (sc.points = sc′.points∧sc.won > sc′.won)).team)

else RandomElement({sc.team | sc ∈ gps (gp) ·

∀ sc′ ∈ gps (gp) ·

sc′.points ≤ sc.points})

pre gp ∈ dom gps ; RandomElement : Team-set →^{o} Team RandomElement (ts) \underline{△}

( dcl t : Team := let t′ ∈ ts in

t′;

return (t) );

GroupWinner-cases : GroupName →^{o} Team GroupWinner-cases (gp) \underline{△}

cases true:

(clear-winner (gps (gp))) → return ((ι sc ∈ gps (gp) ·

∀ sc′ ∈ gps (gp) \ {sc} ·

sc.points > sc′.points).team),

(winner-by-more-wins (gps (gp))) → return ((ι sc ∈ gps (gp) ·

∀ sc′ ∈ gps (gp) \ {sc} · (sc.points > sc′.points) ∨ (sc.points = sc′.points∧sc.won > sc′.won)).team),

others → RandomElement({sc.team | sc ∈ gps (gp) ·

∀ sc′ ∈ gps (gp) ·

sc′.points ≤ sc.points})

end

pre gp ∈ dom gps ; GroupWinners : () →^{o} Team-set GroupWinners () \underline{△}

( dcl winners : Team-set := {}; for all gp ∈ dom gps do ( dcl winner : Team := GroupWinner (gp);

winners := winners ∪ {winner} ) ;

return winners )

end GroupPhase