I am having a little trouble getting the axioms created, moving the static
portions of the Button_State to an axiom from the schema. I can't seem to
get the proof to operate properly. Any suggestions?

As always the zip is attached.


On Thu, Oct 4, 2012 at 3:08 PM, Jon Lockhart <> wrote:

> Roger,
> 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.
> Regards,
> Jon
> 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

Attachment: elevatorSpecV5_P1.doc.gz
Description: GNU Zip compressed data

Proofpower mailing list

Reply via email to