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 <jal...@bucknell.edu> 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 <phil.clay...@lineone.net>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<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<http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com>
>>
>
>

Attachment: 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

Reply via email to