On Friday 28 Sep 2012 22:26, Jon Lockhart wrote:

> I have two questions on that then. First, from a since
> and style standpoint, if I wanted to make everything
> neat in the spec I would place the no changing sets in
> the axiom after the state schema, but for functionality
> standpoint, if I wanted to use them in the predicate
> section of the schema they would need to go before it.
> So what would you see as being the better option? The
> second is would I prove their consistency just like I
> did the global variables?

First I should repeat my caveat. This is not a style of 
specification which I have used or studied, so my views on 
this may be eccentric.

If you are using ProofPower you have to present the 
specification so that every global variable is specified 
before it is used.  There may be tools which can reorder the 
specification for you, but ProofPower doesn't.
I'm not entirely sure what you meant by "in the axiom after 
the state schema", I hope you didn't mean in the predicate 
of the state schema!

Yes, consistency proofs are the same as the ones you have 
been doing.
When you say "just like the global variables", you do them 
like global variables because they will actually be global 

> I do see a problem though in that I don't want those sets
> to be accessed by anyone, only if the schema is included
> in the beginning of the operation.

It won't be possible to change them, but they will be global 
variables so any part of the specification after they have 
been introduced could access them.

> Could we resolve this
> matter by using the schema paragraphs? So we would
> create two schema descriptions of Button_State for
> example and then the first contains the static and the
> second the dynamic sets.

I think that is a good way of organising this material.
But the nub of the original suggestion was that they might 
be taken out of the signature of the operations, and in 
order for them to be accessible in defining the operations on 
the state they would have to be made into global variables 
(which is appropriate for something the specification regards 
as fixed in value).

So if you did define a schema containing what one might 
consider configuration data, you would have to use that 
schema to introduce the names in its signature as global 
variables so that they could then be accessed in you 
operation specifications (or in your definition of state).

> Then when accessing an
> operation the static or does not change symbol is placed
> in front of the static Button_State schema, allowing
> access to the sets, but not allowing change, and this
> way only when the name is provided in the description is
> the information accessible. Would that work to
> accomplish the same goal?

You could do something like this, though its not what I 
intended to suggest.
If I understand you correctly you are suggesting that the 
signature of the operation contains certain fixed data as 
well as the components  which are subject to change (and any 
input or output values).

I have never seen this done, and so I imagine this is a 
larger departure from normal practice than I was advocating.
It has some disadvantages relative to the method I intended 
to suggest.

Generally it is a good idea to try and structure the 
specification so that the size of signatures does not get 
very large.
It is a disadvantage of Z that the syle of specification 
encourages all the state of the system to be represented in 
the flat signature of a single state schema,
You can split this up into many parts and use schema 
inclusion to make this seem better structured in the 
specification, but when you come to reasoning with it you 
will be reasoning with objects which have very large 
signatures, and this make comprehension of what's going on 
more difficult.
In ProofPower is can lead to performance problems, and may 
lead to hard to understand diagnostics from the type 
inference system.

Another problem which may arise is in the schema calculus.
I have not looked into it, but operations like composition 
may not do the right thing with the extra components in the 

You could of course put the configuration variables in the 
state with an equivalence operator, then you would be back 
with something more standard (perhaps that's what you 
intended).  Schema composition would then do the right 

I suspect that this conversation is a little to intricate to 
work very well by email, since the misunderstandings which 
arise in such a discussion take to long to resolve.
If you want to talk about this we could have a Skype 
conversation, you can find me on skype from my email address.
(we would have to agree a time by email).


Proofpower mailing list

Reply via email to