Z Specification for Othello

quinnd6

Hi I have to develop a specification for an othello board game using z specification.
Im finding it to difficult to find anything useful about Z anywhere.
There doesn't seem to be any good help forums for it either.

Its not really a programming question but please if anyone knows of any useful websites, where I could find some tutorials or help forums on Z could you let me know.

theone

heres a few links
info on it
fm europe

This book is pretty good if your a newcomer to z like I was.
book
D. Lightfoot, “Formal Specification Using Z”, 2nd edition, Palgrave, Grassroots series, ISBN 0-333-76327-0, 2001

Thats the link to a hardcover version the softcover version is alot cheaper,if you can't get it out of a library you can buy it easy enough.

If your new to it it's tough starting off but once you get into it your grand.

quinnd6

Ok Iv defined a schema which (I think) states when 2 positions are next to each other.

What I want to say is if a black is next to one white position or a series of white positions then the player places a black next to the whites and all whe whites become blacks.

So basically
eg.1
on the board we have
going from left to right

black, white

Player places down a black piece we get

black, white, black

2 blacks are surrounding the white so it becomes

black, black, black

eg.2
on the board we have going from left to right a black and a number of whites

black,white,white,white

Player places down a black

black, white,white,white ,black

all whites become blacks

black, black, black, black, black.



How would I model this.
Would I use sequence for to state that we have black followed by one or more whites?
How do I state we have ONE OR MORE white positions after the black so as to have a valid move for the black player.

elvis2002

haven't thought too much about your question but maybe you could use a SEQ.
"If the head of SEQ is black & tail elements are all white then do ......"

is_that_so

Try searching for "formal specifications"
A few links that came up. To my shame I can remember very little of it.

http://www.softwaresystems.org/specification.html
http://vl.fmnet.info/z/
http://www.zuser.org/zbook/

and some more detailed ones
here

theone

this is hard to explain but I'll give it a go,

a sequence allows duplicates and it imposes ordering in them.
so that’s perfect for how you want to order your black and white pieces.

if your using a sequence you can check the head(checks the first element in the sequence)
last checks the last element of the sequence

so if you have a sequence

pieces = <black, black ,black, white>

head pieces
"gets the piece coloured black"

last pieces
"gets the pieces coloured white"

so if you have a sequence like you described <black, white>
you insert a black piece say at the start
then you check the first and last of the sequence first and last are black so the whole sequence becomes black.

you do this by saying that the sequence pieces is filtered to elements in the white sequence (I think)

so it's like performing a range restriction and squashing up the sequence to make up for the missing elements
so in that case getting rid of the white element and replacing it with a black one
or just making the sequence all black and just getting rid of the white element


have a separate schema for the reverse of this with white.


There is lots of different ways of doing it ,lots of better ways of doing it I mean