Overture Tool
Formal Modelling in VDM
crosswordSL
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. This example uses the implicit style of specification of VDM-SL and thus may not be executed with the Overture debugger.
| Properties | Values |
|---|---|
| Language Version: | classic |
crossword.vdmsl
values size : nat = 8;
letters : set of char =
{'a','b','c','d','e','f','g','h',
'i','j','k','l','m','n','o','p',
'q','r','s','t','u','v','w','x','y','z'};
black : char = '*';
white : char = '_'
types word = seq of char
inv w == elems(w) subset letters
and len w >= 2 ;
pos = nat1
inv pos_v == pos_v <= size;
position :: h : pos
v : pos;
grid = map position to char
inv gr == rng gr subset (letters union {white, black}) and
dom gr = {mk_position(i,j) | i in set {1,...,size},
j in set {1,...,size}};
HV = <H> | <V>
state crosswords of
cwgrid : grid
valid_words : set of word
waiting_words : set of word
inv mk_crosswords(gr,val,wait) ==
CW_INVARIANT(gr,val,wait)
init mk_crosswords(gr,val,wait) ==
val = { } and wait = { } and
forall i in set {1,...,size} &
forall j in set {1,...,size} &
gr(mk_position(i,j)) = white
end
functions
CW_INVARIANT: grid * set of word * set of word +> bool
CW_INVARIANT(gr,val,wait) ==
val inter wait = {}
and WORDS(gr) subset (val union wait)
and wait subset WORDS(gr)
;
WORDS : grid +> set of word
WORDS(g) == HOR_WORDS(g) union VER_WORDS(g)
;
HOR_WORDS : grid +> set of word
HOR_WORDS(g) == dunion { WORDS_OF_SEQ(LINE(i,g)) | i in set {1,...,size}}
;
VER_WORDS : grid +> set of word
VER_WORDS(g) == dunion { WORDS_OF_SEQ(COL(i,g)) | i in set {1,...,size}}
;
LINE : pos * grid +> seq of char
LINE(i,g) == [g(mk_position(i,c)) | c in set {1,...,size}]
;
COL : pos * grid +> seq of char
COL(i,g) == [g(mk_position(l,i)) | l in set {1,...,size}]
;
WORDS_OF_SEQ : seq of char +> set of word
WORDS_OF_SEQ(s) == {w | w : word &
exists s1, s2 : seq of char &
s = s1 ^ w ^ s2
and (s1 = [] or s1(len s1) = black or s1(len s1) = white)
and (s2 = [] or s2(1) = black or s2(1) = white)}
;
COMPATIBLE : grid * word * position * HV +> bool
COMPATIBLE (g, w, p, d ) ==
(d = <H> =>
(p.h + len w -1 <= size)
and forall i in set inds w &
g(mk_position(p.h + i -1, p.v)) = white
or g(mk_position(p.h + i -1, p.v)) = w(i)
)
and
(d = <V> =>
(p.v + len w -1 <= size)
and forall i in set inds w &
g(mk_position(p.h, p.v + i -1)) = white
or g(mk_position(p.h, p.v + i -1)) = w(i))
;
IS_LOCATED : grid * word * position * HV +> bool
IS_LOCATED (g, w, p, d ) ==
(d = <H> =>
forall i in set inds w &
g(mk_position(p.h + i -1, p.v)) = w(i))
and
(d = <V> =>
forall i in set inds w &
g(mk_position(p.h, p.v + i -1)) = w(i))
;
IN_WORD: grid * position * HV +> bool
IN_WORD(g,p,d) ==
(d = <H> =>
exists i,j : pos &
i <= p.h and j >= p.h and i < j and
forall k in set {i,..., j} &
g(mk_position(k,p.v)) in set letters)
and
(d = <V> =>
exists i,j : pos &
i <= p.v and j >= p.v and i < j and
forall k in set {i,..., j} &
g(mk_position(p.h,k)) in set letters)
operations
VALIDATE_WORD (w : word)
ext wr valid_words : set of word
wr waiting_words : set of word
pre w in set waiting_words
post valid_words = valid_words~ union {w}
and waiting_words = waiting_words~ \ {w}
;
ADD_WORD (w : word, p : position, d : HV)
ext wr cwgrid : grid
rd valid_words : set of word
wr waiting_words : set of word
pre COMPATIBLE(cwgrid, w, p, d)
post (d = <H> =>
cwgrid = cwgrid~ ++ {mk_position(p.h + i - 1, p.v) |-> w(i)
| i in set inds w})
and
(d = <V> =>
cwgrid = cwgrid~ ++ {mk_position(p.h, p.v + i - 1) |-> w(i)
| i in set inds w})
and
CW_INVARIANT(cwgrid, valid_words,waiting_words)
;
ADD_BLACK ( p : position)
ext wr cwgrid : grid
pre cwgrid(p) = white
post cwgrid = cwgrid~ ++ { p |-> black }
;
DELETE_BLACK ( p : position)
ext wr cwgrid : grid
pre cwgrid(p) = black
post cwgrid = cwgrid~ ++ { p |-> white }
;
STRONG_DELETE (w : word, p : position, d : HV)
ext wr cwgrid : grid
rd valid_words : set of word
wr waiting_words : set of word
pre IS_LOCATED(cwgrid, w, p, d)
post (d = <H> =>
cwgrid = cwgrid~ ++ {mk_position(p.h + i - 1, p.v) |-> white
| i in set inds w})
and
(d = <V> =>
cwgrid = cwgrid~ ++ {mk_position(p.h, p.v + i - 1) |-> white
| i in set inds w})
and
CW_INVARIANT(cwgrid,valid_words, waiting_words)
;
SOFT_DELETE (w : word, p : position, d : HV)
ext wr cwgrid : grid
rd valid_words : set of word
wr waiting_words : set of word
pre IS_LOCATED(cwgrid, w, p, d)
post (d = <H> =>
cwgrid = cwgrid~ ++
{mk_position(p.h + i - 1, p.v) |-> white
| i in set inds w
& not IN_WORD(cwgrid~,mk_position(p.h + i - 1, p.v),<V>) })
and
(d = <V> =>
cwgrid = cwgrid~ ++
{mk_position(p.h, p.v + i - 1) |-> white
| i in set inds w
& not IN_WORD(cwgrid~,mk_position(p.h, p.v + i - 1),<H>) })
and
CW_INVARIANT(cwgrid,valid_words, waiting_words)