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 -t> bool
CW_INVARIANT(gr,val,wait) ==
val inter wait = {} 
and WORDS(gr) subset (val union wait)
and wait subset WORDS(gr)
;

WORDS : grid -t> set of word
WORDS(g) == HOR_WORDS(g) union VER_WORDS(g)
;

HOR_WORDS : grid -t> set of word
HOR_WORDS(g) == dunion { WORDS_OF_SEQ(LINE(i,g)) | i in set {1,...,size}}
;
VER_WORDS : grid -t> set of word
VER_WORDS(g) == dunion { WORDS_OF_SEQ(COL(i,g)) | i in set {1,...,size}}
;

LINE : pos *  grid -t> seq of char
LINE(i,g) == [g(mk_position(i,c)) | c in set {1,...,size}]
;
COL : pos *  grid -t> seq of char
COL(i,g) == [g(mk_position(l,i)) | l in set {1,...,size}]
;

WORDS_OF_SEQ : seq of char -t> 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 -t> 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 -t> 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 -t> 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)