Overture Tool

Formal Modelling in VDM

Overture Tool

Go to our GitHub Profile

Follow @overturetool

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)