Overture Tool
Formal Modelling in VDM
soccerSL
Author: Yves Ledru
This tutorial example is taken out of a VDM course given to the students of the Diplôme d’Etudes Supérieures Spécialisées en Génie Informatique (5th year) at the Université Joseph Fourier. A first version uses the implicit style of specification of VDM-SL and thus may not be executed with VDMTools. An explicit version is given as an appendix.
| Properties | Values |
|---|---|
| Language Version: | classic |
| Entry point : | SOCCER_EXPL`SUBSTITUTION(3,15) |
soccer.vdmsl
module SOCCER_IMPL
exports all
definitions
values gk_subs_max : nat1 = 1;
fp_subs_max : nat1 = 2
types player = nat1
state R_Book of
on_field_players : set of player
potential_substitutes : set of player
goalkeeper : player
nb_gk_subs : nat
nb_fp_subs : nat
inv mk_R_Book(ofp,ps,gk, ngk, nfp) ==
leq_eleven_players(ofp) and
within_allowed_limits(ngk,nfp) and
gk not in set ps and
ofp inter ps = {}
init r == r =
mk_R_Book({1,2,3,4,5,6,7,8,9,10,11},
{12,13,14,15,16},1,0,0)
end
functions
leq_eleven_players : set of player +> bool
leq_eleven_players(f) == (card f) <= 11
;
within_allowed_limits : nat * nat +> bool
within_allowed_limits (ngk , nfp ) ==
(ngk <= gk_subs_max) and (nfp <= fp_subs_max)
operations
RED_CARD (p : player)
ext wr on_field_players : set of player
wr potential_substitutes : set of player
pre p in set on_field_players or p in set potential_substitutes
post on_field_players = on_field_players~ \ {p}
and potential_substitutes = potential_substitutes~ \ {p}
;
CHANGE_GOALKEEPER (p : player)
ext wr goalkeeper : player
rd on_field_players : set of player
pre p in set on_field_players
post goalkeeper = p
;
SUBSTITUTION (pl : player, subs: player)
ext wr on_field_players : set of player
wr potential_substitutes : set of player
wr goalkeeper : player
wr nb_gk_subs : nat
wr nb_fp_subs : nat
pre pl in set on_field_players and subs in set potential_substitutes
and (pl = goalkeeper => within_allowed_limits(nb_gk_subs+1,nb_fp_subs))
and (pl <> goalkeeper => within_allowed_limits(nb_gk_subs,nb_fp_subs+1))
post on_field_players = on_field_players~ union {subs} \ {pl}
and potential_substitutes = potential_substitutes~ \ {subs}
and (pl = goalkeeper~ =>
((goalkeeper = subs)
and (nb_gk_subs = nb_gk_subs~ +1 )
and (nb_fp_subs = nb_fp_subs~)))
and (pl <> goalkeeper~ =>
((goalkeeper = goalkeeper~)
and (nb_gk_subs = nb_gk_subs~)
and (nb_fp_subs = nb_fp_subs~ +1)))
;
SUBSTITUTION_GK (pl : player, subs: player)
ext wr on_field_players : set of player
wr potential_substitutes : set of player
wr goalkeeper : player
wr nb_gk_subs : nat
rd nb_fp_subs : nat
pre pl in set on_field_players and subs in set potential_substitutes
and pl = goalkeeper and within_allowed_limits(nb_gk_subs+1,nb_fp_subs)
post on_field_players = on_field_players~ union {subs} \ {pl}
and potential_substitutes = potential_substitutes~ \ {subs}
and goalkeeper = subs and nb_gk_subs = nb_gk_subs~ +1
;
SUBSTITUTION_FP (pl : player, subs: player)
ext wr on_field_players : set of player
wr potential_substitutes : set of player
rd goalkeeper : player
rd nb_gk_subs : nat
wr nb_fp_subs : nat
pre pl in set on_field_players and subs in set potential_substitutes
and pl <> goalkeeper and within_allowed_limits(nb_gk_subs,nb_fp_subs+1)
post on_field_players = on_field_players~ union {subs} \ {pl}
and potential_substitutes = potential_substitutes~ \ {subs}
and nb_fp_subs = nb_fp_subs~ +1
;
SUBSTITUTION_EXPL : player * player ==> ()
SUBSTITUTION_EXPL (pl , subs)
== if pl = goalkeeper then SUBSTITUTION_GK(pl,subs)
else SUBSTITUTION_FP(pl,subs)
pre (pl = goalkeeper =>
pre_SUBSTITUTION_GK(pl,subs,
mk_R_Book(on_field_players,potential_substitutes,
goalkeeper,nb_gk_subs, nb_fp_subs)))
and (pl <> goalkeeper =>
pre_SUBSTITUTION_FP(pl,subs,
mk_R_Book(on_field_players,potential_substitutes,
goalkeeper,nb_gk_subs,nb_fp_subs)))
end SOCCER_IMPL
module SOCCER_EXPL
exports all
definitions
values gk_subs_max : nat1 = 1;
fp_subs_max : nat1 = 2
types player = nat1
state R_Book of
on_field_players : set of player
potential_substitutes : set of player
goalkeeper : player
nb_gk_subs : nat
nb_fp_subs : nat
inv mk_R_Book(ofp,ps,gk, ngk, nfp) ==
leq_eleven_players(ofp) and
within_allowed_limits(ngk,nfp) and
gk not in set ps and
ofp inter ps = {}
init r == r = mk_R_Book({1,2,3,4,5,6,7,8,9,10,11}, {12,13,14,15,16}, 1, 0, 0)
end
functions
leq_eleven_players : set of player +> bool
leq_eleven_players(f) == (card f) <= 11
;
within_allowed_limits : nat * nat +> bool
within_allowed_limits (ngk , nfp ) ==
(ngk <= gk_subs_max) and (nfp <= fp_subs_max)
operations
RED_CARD : player ==> ()
RED_CARD (p) ==
(
on_field_players := on_field_players \ {p};
potential_substitutes := potential_substitutes \ {p}
)
pre p in set on_field_players or p in set potential_substitutes
post on_field_players = on_field_players~ \ {p}
and potential_substitutes = potential_substitutes~ \ {p}
;
CHANGE_GOALKEEPER : player ==> ()
CHANGE_GOALKEEPER (p) ==
(
goalkeeper := p
)
pre p in set on_field_players
post goalkeeper = p
;
SUBSTITUTION : player * player ==> ()
SUBSTITUTION (pl, subs) ==
( on_field_players := on_field_players union {subs} \ {pl};
potential_substitutes := potential_substitutes \ {subs};
if pl = goalkeeper
then (goalkeeper := subs;
nb_gk_subs := nb_gk_subs +1)
else nb_fp_subs := nb_fp_subs +1
)
pre pl in set on_field_players and subs in set potential_substitutes
and (pl = goalkeeper => within_allowed_limits(nb_gk_subs+1,nb_fp_subs))
and (pl <> goalkeeper => within_allowed_limits(nb_gk_subs,nb_fp_subs+1))
post on_field_players = on_field_players~ union {subs} \ {pl}
and potential_substitutes = potential_substitutes~ \ {subs}
and (pl = goalkeeper~ =>
((goalkeeper = subs)
and (nb_gk_subs = nb_gk_subs~ +1 )
and (nb_fp_subs = nb_fp_subs~)))
and (pl <> goalkeeper~ =>
((goalkeeper = goalkeeper~)
and (nb_gk_subs = nb_gk_subs~)
and (nb_fp_subs = nb_fp_subs~ +1)))
;
SUBSTITUTION_GK : player * player ==> ()
SUBSTITUTION_GK (pl , subs) ==
(
on_field_players := on_field_players union {subs} \ {pl};
potential_substitutes := potential_substitutes \ {subs};
goalkeeper := subs;
nb_gk_subs := nb_gk_subs +1
)
pre pl in set on_field_players and subs in set potential_substitutes
and pl = goalkeeper and within_allowed_limits(nb_gk_subs+1,nb_fp_subs)
post on_field_players = on_field_players~ union {subs} \ {pl}
and potential_substitutes = potential_substitutes~ \ {subs}
and goalkeeper = subs and nb_gk_subs = nb_gk_subs~ +1
;
SUBSTITUTION_FP : player *player ==> ()
SUBSTITUTION_FP (pl , subs) ==
(
on_field_players := on_field_players union {subs} \ {pl};
potential_substitutes := potential_substitutes \ {subs};
nb_fp_subs := nb_fp_subs +1
)
pre pl in set on_field_players and subs in set potential_substitutes
and pl <> goalkeeper and within_allowed_limits(nb_gk_subs,nb_fp_subs+1)
post on_field_players = on_field_players~ union {subs} \ {pl}
and potential_substitutes = potential_substitutes~ \ {subs}
and nb_fp_subs = nb_fp_subs~ +1
;
SUBSTITUTION_EXPL : player * player ==> ()
SUBSTITUTION_EXPL (pl , subs) ==
if pl = goalkeeper
then SUBSTITUTION_GK(pl,subs)
else SUBSTITUTION_FP(pl,subs)
pre (pl = goalkeeper =>
pre_SUBSTITUTION_GK(pl,subs,
mk_R_Book(on_field_players,potential_substitutes,
goalkeeper,nb_gk_subs, nb_fp_subs)))
and (pl <> goalkeeper =>
pre_SUBSTITUTION_FP(pl,subs,
mk_R_Book(on_field_players,potential_substitutes,
goalkeeper,nb_gk_subs,nb_fp_subs)))
end SOCCER_EXPL