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 <[email protected]> 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 <[email protected]>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 >> [email protected] >> http://lemma-one.com/mailman/**listinfo/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 [email protected] http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
