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
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
Generally it is a good idea to try and structure the
specification so that the size of signatures does not get
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
In ProofPower is can lead to performance problems, and may
lead to hard to understand diagnostics from the type
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