So after some serious thought the last couple of days, and after having
some discussions with my advisers, and comparing the pros and cons of the
various options I have at accomplishing the goal I want to achieve, I have
decided to move everything that is static in my state schemas to axioms
like you had mentioned. It definitely is the best option and accomplishes
the goal I need, along with further placing realistic constraints on the
system. Once I get it all written up, I will send you a copy so you can
look at it and maybe provide further advice. Once this is all wrapped up I
got to get back to the init operations and get those proven.


On Tue, Oct 2, 2012 at 4:23 AM, Roger Bishop Jones <> wrote:

> 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
> variables.
> > 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
> schema.
> 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
> thing.
> 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).
> Roger
Proofpower mailing list

Reply via email to