Overture Tool

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)