Re: [ProofPower] Trying to Prove my Zed Specifications

2012-09-13 Thread Phil Clayton 

Jon,

On 13/09/12 04:16, Jon Lockhart wrote:

Are you saying then for the Boolean block I have to just replace it with
the one that you have provided in the email?


Not only would you have to replace the Boolean block but also remove the 
integer comparison around the references to Boolean global variables. 
For example, the predicate


  masterStop = 0

must be changed to either

  ¬ masterStop

or

  masterStop = False



Seems odd to be to just
through True and False in there like that where I am describing sets but
if it works, then I am all for it, I just need to see or understand how
to use it properly.


To use this is very simple for the most part.  In a predicate context, 
just treat Boolean expressions as though they were predicates.  In an 
expression context, Boolean expressions can be combined to give other 
Boolean expressions as you would expect, e.g. a ∧ b.  However, to create 
a Boolean expression from a predicate p, you need to write


  [ | p]

It is probably worth understanding what is going on at least once.  It 
is easiest to think in terms of sets.  A schema is just a set of 
bindings.  The empty schema [], which is the same as [ | true], is a set 
containing just the empty binding, i.e. {()}.  So [] is much like the 
SML type 'unit', a type that has only one value.  Thus Boolean is the 
set {{}, {()}} where {} represents false and {()} represents true, hence 
our definition of True and False.  So an expression of type Boolean is a 
schema.  When a schema S is used as a predicate, the predicate is θS ∈ 
S.  For one of our Boolean expressions B as a predicate, the predicate 
is θB ∈ B which is equivalent to () ∈ B.  So you can see how the 
corresponding predicate is derived.




As for the version of ProofPower, I have version 2.9.1w2, which is what
you were saying does not support ==. Looks like I might have to update
here when the latest stable version is released on the site.


If you feel inclined to try the latest patch, it is here, with instructions:
http://www.lemma-one.com/ProofPower/patches/patches.html

I'm fairly familiar with the installation process, so it only takes me a 
few minutes to build a patched version.  However, a new release may be 
around the corner - I don't know what Rob's plans are there.




What I was saying on the masterStop / masterReset axiom, along with the
minNumberFloors, maxNumberFloors, etc axioms, since I am using those as
global variables essentially, is how do I prove them and preconditions
on them like I have down for my States so far? Is is necessary too, or
if I just get the spec of them they are already shown to be theorems?


I see what you mean.  Yes, for an axiomatic description, one wants to be 
sure that it is not introducing a contradiction into the theory, making 
the theory inconsistent.  ProofPower has a mode of operation where it 
does not assume such axioms are consistent until they have been proved 
consistent.  This works by showing that each axiom is a conservative 
extension to the theory, i.e. does not introduce an inconsistency.


For Z, at the start of your theory, you would do

  set_flag ("z_use_axioms", false);

Note, then, that z_get_spec does not simply give you the axiom as a 
theorem.  After an axiomatic description paragraph, start a consistency 
proof with e.g.


  z_push_consistency_goal %SZT%minNumberFloors%>%;

See section 5.3, page 93, of usr011.dvi for examples.

Phil


___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Re: [ProofPower] Best platform for ProofPower?

2012-09-13 Thread Jon Lockhart 
Roger,

Yes I had noticed that the message that Phil replied too had not gone to
the list yet. I hit the reply all button in my message chain and it
selected several people that i had been replying to previously and the
list. I received an email in return saying it had to be reviewed by the
moderator, which I assume is Rob, before it could be released since the
attachment sizes were over the limit.

As soon as it gets approved it should be released to the list.

Thanks,
Jon

On Thu, Sep 13, 2012 at 3:59 AM, Roger Bishop Jones  wrote:

> Jon,
>
> On Wednesday 12 Sep 2012 21:09, you wrote:
>
> > I am running ProofPower on Debian. More specifically
> > Wheezy, which is the testing version of Debian. I have
> > not run into any problems yet.
>
> Thanks jon, I will probably give Debian a try (depending on
> what anyone else says).
> I have a netinstall disc for the latest stable version ready
> to go.
>
> BTW, were you aware that the post which Phil responded to
> never went to the list?
>
> Also, as far as the ProofPower releases go, there isn't
> really a distinction between stable and others.
> The version which fixes your problem is probably just the
> incorporation of a patch and will be as stable as the one
> you are using (though the "maths_egs" package is changed
> more substantially, but still quite stable).
> This is more like getting a security update for a stable
> release of Linux (though I suppose it should be called a
> "testing" version).
> I didn't get any problems running all my work (apart from
> the maths_egs issues) through it, though I don't actually
> use Z these days.
>
> Roger
>
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Re: [ProofPower] Best platform for ProofPower?

2012-09-13 Thread Phil Clayton 

On 12/09/12 21:05, Roger Bishop Jones wrote:

I'm having bad luck lately getting suitable environments for
running ProofPower.

My laptop is on Ubuntu 10.4, and that is fine for ProofPower,
but is now so out of date that I can't upgrade it, I would
have to install a more recent version of Ubuntu from
scratch.

So I revived an old server to try out a more up-to-date
context for running ProofPower.
(my efforts in the amazon cloud ran into the buffers some time
ago).

So far I'm not having much success on Ubuntu 12.04 (the
PolyML build doesn't seem to work for me).


What error message do you get?  I ask because David Matthews is about to 
release 5.5 so it would be worth resolving any issue there.




I'm interested to know what people are actually running
ProofPower on these days?


I'm using Fedora 16.  Generally I've had no issue installing on the 
Fedora series of Linux provided that all the prerequisite packages are 
installed - achieved with the following yum/rpm commands:


yum install \
  gcc-c++ \
  polyml \
  texlive-latex \
  libXp-devel \
  libXext-devel \
  libXmu-devel \
  libXt-devel \
  xorg-x11-fonts-misc

rpm -ivh \

http://motif.ics.com/sites/default/files/openmotif-2.3.3-1.fc12.x86_64.rpm \

http://motif.ics.com/sites/default/files/openmotif-devel-2.3.3-1.fc12.x86_64.rpm

The key bindings 'just work' with AltGr and Left Window as the modifiers.

However, many new distributions use Gnome 3 which causes screen redraw 
problems for Xpp (and Motif applications generally).  One simple 
work-around for Gnome 3 is to run in 'fallback mode' which avoids 
hardware acceleration.  That's what I do.  (There appear to be various 
discussions out there about this issue so it may be resolved now.)


Phil


P.S.  Also, I have an issue when using X in Depth30 mode, i.e. 10 bits 
per colour.  Unless Xpp is run as root, it fails to start.  Probably not 
an Xpp-specific issue.  I haven't bothered reporting that yet.  For now 
I just use Depth24, which is what most people without fancy displays are 
using.


___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Re: [ProofPower] Best platform for ProofPower?

2012-09-13 Thread Rob Arthan 
Jon,

On 13 Sep 2012, at 18:10, Jon Lockhart wrote:

> Roger,
> 
> Yes I had noticed that the message that Phil replied too had not gone to the 
> list yet. I hit the reply all button in my message chain and it selected 
> several people that i had been replying to previously and the list. I 
> received an email in return saying it had to be reviewed by the moderator, 
> which I assume is Rob, before it could be released since the attachment sizes 
> were over the limit. 
> 
> As soon as it gets approved it should be released to the list.

Please repost it _without_ the PDF attachment. If you need to reference a large 
file then please post a link to a file on a website of your choosing or a 
Dropbox public file  or similar.

Regards,

Rob.
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Re: [ProofPower] Best platform for ProofPower?

2012-09-13 Thread Jon Lockhart 
Ok will do for the future Rob.

-Jon


On Thu, Sep 13, 2012 at 3:59 PM, Rob Arthan  wrote:

> Jon,
>
> On 13 Sep 2012, at 18:10, Jon Lockhart wrote:
>
> > Roger,
> >
> > Yes I had noticed that the message that Phil replied too had not gone to
> the list yet. I hit the reply all button in my message chain and it
> selected several people that i had been replying to previously and the
> list. I received an email in return saying it had to be reviewed by the
> moderator, which I assume is Rob, before it could be released since the
> attachment sizes were over the limit.
> >
> > As soon as it gets approved it should be released to the list.
>
> Please repost it _without_ the PDF attachment. If you need to reference a
> large file then please post a link to a file on a website of your choosing
> or a Dropbox public file  or similar.
>
> Regards,
>
> Rob.
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Re: [ProofPower] Trying to Prove my Zed Specifications

2012-09-13 Thread Jon Lockhart 
Phil,

I tried performing the change you prescribed in my ProofPower spec and it
fails to parse. I have included the attachment for your reference.

Thanks,
Jon


On Thu, Sep 13, 2012 at 2:38 PM, Jon Lockhart  wrote:

> Phil,
>
> Attached is an updated version of my spec making the changes you
> suggested, minus having the changes provided in my natural language
> description. You were right in that FUZZ does not like using that since it
> is based off Spivey's Z guide and I don't think he allowed setting
> Boolean's like you discussed, and would be why when I tried implementing
> them as described in "The Way of Zed" the checker failed. However CZT,
> which is built on the Z Standard, does allow for it, so I am perfectly good
> there. CZT is a stricter type checker anyways.
>
> So I will go and get those changes made in my ProofPower version as well.
>
> Thanks for the info on the axiom checking and the patch. I did find that
> page, which I had remembered reading, and I will start there in trying to
> check my axioms.
>
> I will continue to move forward and there should probably be more emails
> from me here in the short term, as even with all that I have learned from
> the tutorials I am still learning, as there is a lot to ProofPower.
>
> Regards,
> Jon
>
>
>
> On Thu, Sep 13, 2012 at 9:05 AM, Phil Clayton wrote:
>
>> Jon,
>>
>>
>> On 13/09/12 04:16, Jon Lockhart wrote:
>>
>>> Are you saying then for the Boolean block I have to just replace it with
>>> the one that you have provided in the email?
>>>
>>
>> Not only would you have to replace the Boolean block but also remove the
>> integer comparison around the references to Boolean global variables. For
>> example, the predicate
>>
>>   masterStop = 0
>>
>> must be changed to either
>>
>>   ¬ masterStop
>>
>> or
>>
>>   masterStop = False
>>
>>
>>
>>  Seems odd to be to just
>>> through True and False in there like that where I am describing sets but
>>> if it works, then I am all for it, I just need to see or understand how
>>> to use it properly.
>>>
>>
>> To use this is very simple for the most part.  In a predicate context,
>> just treat Boolean expressions as though they were predicates.  In an
>> expression context, Boolean expressions can be combined to give other
>> Boolean expressions as you would expect, e.g. a ∧ b.  However, to create a
>> Boolean expression from a predicate p, you need to write
>>
>>   [ | p]
>>
>> It is probably worth understanding what is going on at least once.  It is
>> easiest to think in terms of sets.  A schema is just a set of bindings.
>>  The empty schema [], which is the same as [ | true], is a set containing
>> just the empty binding, i.e. {()}.  So [] is much like the SML type 'unit',
>> a type that has only one value.  Thus Boolean is the set {{}, {()}} where
>> {} represents false and {()} represents true, hence our definition of True
>> and False.  So an expression of type Boolean is a schema.  When a schema S
>> is used as a predicate, the predicate is θS ∈ S.  For one of our Boolean
>> expressions B as a predicate, the predicate is θB ∈ B which is equivalent
>> to () ∈ B.  So you can see how the corresponding predicate is derived.
>>
>>
>>
>>  As for the version of ProofPower, I have version 2.9.1w2, which is what
>>> you were saying does not support ==. Looks like I might have to update
>>> here when the latest stable version is released on the site.
>>>
>>
>> If you feel inclined to try the latest patch, it is here, with
>> instructions:
>> http://www.lemma-one.com/**ProofPower/patches/patches.**html
>>
>> I'm fairly familiar with the installation process, so it only takes me a
>> few minutes to build a patched version.  However, a new release may be
>> around the corner - I don't know what Rob's plans are there.
>>
>>
>>
>>  What I was saying on the masterStop / masterReset axiom, along with the
>>> minNumberFloors, maxNumberFloors, etc axioms, since I am using those as
>>> global variables essentially, is how do I prove them and preconditions
>>> on them like I have down for my States so far? Is is necessary too, or
>>> if I just get the spec of them they are already shown to be theorems?
>>>
>>
>> I see what you mean.  Yes, for an axiomatic description, one wants to be
>> sure that it is not introducing a contradiction into the theory, making the
>> theory inconsistent.  ProofPower has a mode of operation where it does not
>> assume such axioms are consistent until they have been proved consistent.
>>  This works by showing that each axiom is a conservative extension to the
>> theory, i.e. does not introduce an inconsistency.
>>
>> For Z, at the start of your theory, you would do
>>
>>   set_flag ("z_use_axioms", false);
>>
>> Note, then, that z_get_spec does not simply give you the axiom as a
>> theorem.  After an axiomatic description paragraph, start a consistency
>> proof with e.g.
>>
>>   z_push_consistency_goal %SZT%minNumberFloors%>%;
>>

Re: [ProofPower] Best platform for ProofPower?

2012-09-13 Thread Roger Bishop Jones 
On Thursday 13 Sep 2012 19:37, Phil Clayton wrote:
> On 12/09/12 21:05, Roger Bishop Jones wrote:

> > So far I'm not having much success on Ubuntu 12.04 (the
> > PolyML build doesn't seem to work for me).
> 
> What error message do you get?  I ask because David
> Matthews is about to release 5.5 so it would be worth
> resolving any issue there.

The build seemed to have gone through OK, though I couldn't 
actually find any instructions so who knows whether I did the 
right thing!

I ran ./configure a few times, installing whatever it 
complained of the absence of, and the ran make.

When I invoked poly it complained that it couldn't find some 
libraries.

Unfortunately I am now building Debian so Ubuntu 12.04 is 
history and I can't check exactly what the complaint was.

> > I'm interested to know what people are actually running
> > ProofPower on these days?
> 
> I'm using Fedora 16.  Generally I've had no issue
> installing on the Fedora series of Linux provided that
> all the prerequisite packages are installed - achieved
> with the following yum/rpm commands:

Thanks for the info about Fedora 16 I will give that a go if 
I don't get on with Debian. (which was suggested by jon).

Roger


___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Re: [ProofPower] Trying to Prove my Zed Specifications

2012-09-13 Thread Phil Clayton 

On 13/09/12 21:32, Jon Lockhart wrote:

I tried performing the change you prescribed in my ProofPower spec and
it fails to parse. I have included the attachment for your reference.


I think the attachment has a strange compression format or has been 
corrupted - gunzip reports "unexpected end of file".  I managed to 
extract enough by renaming to .xz and extracting with 7za though.  (How 
did you create the .gz file?)


The issue is that there can only be one abbreviation definition per 
paragraph.  You can't lump BOOLEAN, True and False all together into one 
paragraph.  Apologies if I misled you with my email presentation.


Phil


___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Re: [ProofPower] Trying to Prove my Zed Specifications

2012-09-13 Thread Jon Lockhart 
Phil,

I see now, I did not know that. You can lump them together in the Word
document when I am using those tools but that is b/c when it is parsed each
is separated into its own paragraph on the back end. I will be sure to
correct that and see where I can get from there. Thanks for the help.

As for the zipped file I used the gzip command, which is short for gunzip.
Was the first couple I sent you corrupted?

Thanks,
Jon


On Thu, Sep 13, 2012 at 6:25 PM, Phil Clayton wrote:

> On 13/09/12 21:32, Jon Lockhart wrote:
>
>> I tried performing the change you prescribed in my ProofPower spec and
>> it fails to parse. I have included the attachment for your reference.
>>
>
> I think the attachment has a strange compression format or has been
> corrupted - gunzip reports "unexpected end of file".  I managed to extract
> enough by renaming to .xz and extracting with 7za though.  (How did you
> create the .gz file?)
>
> The issue is that there can only be one abbreviation definition per
> paragraph.  You can't lump BOOLEAN, True and False all together into one
> paragraph.  Apologies if I misled you with my email presentation.
>
>
> Phil
>
>
> __**_
> Proofpower mailing list
> Proofpower@lemma-one.com
> http://lemma-one.com/mailman/**listinfo/proofpower_lemma-one.**com
>
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Re: [ProofPower] Trying to Prove my Zed Specifications

2012-09-13 Thread Phil Clayton 

On 13/09/12 23:48, Jon Lockhart wrote:

I see now, I did not know that. You can lump them together in the Word
document when I am using those tools but that is b/c when it is parsed
each is separated into its own paragraph on the back end. I will be sure
to correct that and see where I can get from there. Thanks for the help.


You're welcome.  By the way, I don't think any dialect of Z allows 
multiple horizontal definitions in one paragraph.




As for the zipped file I used the gzip command, which is short for
gunzip. Was the first couple I sent you corrupted?


No, all the other GZ attachments have been fine - it must have been 
corrupted somewhere.


Phil


___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Re: [ProofPower] Trying to Prove my Zed Specifications

2012-09-13 Thread Jon Lockhart 
Phil,

Moving them all to there own paragraph worked great. Now I am up to proving
the consistency of the axioms, which is where I am run into my next
stumbling block. Got the spec load and the consistency goal using the
commands no problem. This generates a sub goal which looks relatively
straight forward. It using the "there exist" symbol at the front of the
goal, so my initial assumption is to use the z_"there exists"_tac, as seen
in the provided spec. Unfortunately just giving it masterStop is not
enough, and I can't feed it a list of masterStop and masterReset. Next
thought was there should be some tactic like this that also has list in it,
but I can't seem to find one. So that is where I am at right now.

Thanks,
Jon


On Thu, Sep 13, 2012 at 7:30 PM, Phil Clayton wrote:

> On 13/09/12 23:48, Jon Lockhart wrote:
>
>> I see now, I did not know that. You can lump them together in the Word
>> document when I am using those tools but that is b/c when it is parsed
>> each is separated into its own paragraph on the back end. I will be sure
>> to correct that and see where I can get from there. Thanks for the help.
>>
>
> You're welcome.  By the way, I don't think any dialect of Z allows
> multiple horizontal definitions in one paragraph.
>
>
>
>  As for the zipped file I used the gzip command, which is short for
>> gunzip. Was the first couple I sent you corrupted?
>>
>
> No, all the other GZ attachments have been fine - it must have been
> corrupted somewhere.
>
>
> Phil
>
>
> __**_
> Proofpower mailing list
> Proofpower@lemma-one.com
> http://lemma-one.com/mailman/**listinfo/proofpower_lemma-one.**com
>


elevatorSpecV5_P1.doc.gz
Description: GNU Zip compressed data
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com