Thank you Rob, I just tried this and it works perfectly! It is a testament to the quality of the design of ProofPower that it is so versatile and adaptable. I see you got QCheck to work too; It looks very promising to create unit tests easily. I hadn't known that you could choose to run different interpreters in xpp! Great program; I will use it this next semester in my computer science classes. I am not sure how far I can get with "proofs" for the beginning intro to cs classes, but at the very least, I can use it to introduce literate, functional programming.
I used Object-Z in my OOP classes last semester using this tool: ------------------------ quote from Kenny Hunt (http://charity.cs.uwlax.edu): Toze: The Object Z EditorI have worked with Kasi Periyasamy and Tim Parker to develop a graphical editor for Object Z specifications. The application is rolled into a single executable jar file. Download the toze-2.0.2.jar file and then double-click on it once you've got it on your desktop. ------------------------ It was fairly successful for most students, and demonstrated the value of unambiguous specifications. I am hoping to use zed within ProofPower for similar reasons if I can get up to speed on it soon enough. -Dave Topham (http://dev2.ohlone.edu/people/dtopham/) On Mon, Dec 29, 2014 at 9:00 AM, <proofpower-requ...@lemma-one.com> wrote: > Send Proofpower mailing list submissions to > proofpower@lemma-one.com > > To subscribe or unsubscribe via the World Wide Web, visit > http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com > or, via email, send a message with subject or body 'help' to > proofpower-requ...@lemma-one.com > > You can reach the person managing the list at > proofpower-ow...@lemma-one.com > > When replying, please edit your Subject line so it is more specific > than "Re: Contents of Proofpower digest..." > > > Today's Topics: > > 1. Re: Can QCheck work in xpp? (Rob Arthan) > 2. Re: Can QCheck work in xpp? (Rob Arthan) > > > ---------------------------------------------------------------------- > > Message: 1 > Date: Mon, 29 Dec 2014 15:16:53 +0000 > From: Rob Arthan <r...@lemma-one.com> > To: ProofPower List <proofpower@lemma-one.com> > Cc: David Topham <dtop...@gmail.com> > Subject: Re: [ProofPower] Can QCheck work in xpp? > Message-ID: <51b6efb9-323d-442e-800e-d0b4ef267...@lemma-one.com> > Content-Type: text/plain; charset="windows-1252" > > David, > > On 28 Dec 2014, at 05:08, David Topham <dtop...@gmail.com> wrote: > > > I am not sure if this is a bug in xpp or if it is a user (me!) error, > but I am trying to use a unit test framework named QCheck within xpp and it > fails. I have attached the doc file and the sml and pdf file produced via > docsml. In the files, I have shown where the error occurs. Since it works > ok in poly, then I expected it to also work within xpp so I am asking if > anyone has tried this; or sees why it may not work as I expect. > > > > The problem is not with xpp but with the extensions to Standard ML that > ProofPower uses > to provide object language quotations and support an extended character > set for use in forming > ML names (so we can use mathematical symbols to form ML names). The > extended language is > called ProofPower-ML. When you run xpp with a command line something like: > > xpp -d hol > or > xpp UT.doc -d zed > > xpp just spawns a process running the command ?pp -d hol? or ?pp -d zed? > which invokes > a session on the hol or zed database and communicates with that process > via a > UN*X pseudo-terminal. Unless you do something special, ?pp -d XYZ? will > run the ProofPower-ML read-eval-print loop. ProofPower-ML is implemented by > a pre-processor that encodes it into ASCII Standard ML and a > post-processor > that converts the ASCII output from the ML compiler?s eval-print function > into the extended character set. > > Your problem is then occurring because we use ?Q? to encode > non-ASCII characters, ?Q? itself being encoded as ?QQQQ?. So somewhat > bizarrely, you will find that: > > size ?QCheck? > > evaluates to 9 in ProofPower-ML. PolyML.make expects a Standard ML > string, rather than a ProofPower-ML string, so it can?t find the file and > raises an error. > > If you just want to use xpp as a user interface to Poly/ML and you don?t > want > the ProofPower specification and theorem-proving tools, then you can > ask xpp to run a different command line. E.g., > > xpp -c poly > > or > > xpp -f UT.doc -c poly > > will bring up xpp talking to a poly session (and editing a new empty file > in the first case and the file UT.doc in the second). (Note that for > not very good reasons, the command line requires -f before the > name of the file to edit when you use -c.) > > (You can actually change the command line within one xpp session if you > like using Tools/Options, but I don?t think you are likely to want that.) > > If you want the ProofPower tools, then you can reverse the encoding > using the function translate_for_output: > > PolyML.make(translate_for_output ?QCheck?); > > or you can switch between ProofPower-ML and Standard ML using > the commands abandon_reader_writer() (ProofPower-ML -> Standard ML) > and use_terminal() (Standard ML -> ProofPower-ML). > > However, I don?t get much further with QCheck. Even when I try to load > it directly from poly, I get the following error message: > > > PolyML.make "QCheck"; > Making QCheck > Making QCheckVersion > Created structure QCheckVersion > structure QCheckVersion : > sig val context : string val version : int * int end > Error- in 'QCheck.sml', line 14. > Structure (RandGen) has not been declared Found near RandGen > > Did you have to do something else to QCheck to get it to work? > > Regards, > > Rob. > > -------------- next part -------------- > An HTML attachment was scrubbed... > URL: < > http://lemma-one.com/pipermail/proofpower_lemma-one.com/attachments/20141229/0525fc59/attachment-0001.html > > > > ------------------------------ > > Message: 2 > Date: Mon, 29 Dec 2014 16:04:26 +0000 > From: Rob Arthan <r...@lemma-one.com> > To: ProofPower List <proofpower@lemma-one.com> > Cc: David Topham <dtop...@gmail.com> > Subject: Re: [ProofPower] Can QCheck work in xpp? > Message-ID: <66badeb3-e677-47d5-afae-37d6cf398...@lemma-one.com> > Content-Type: text/plain; charset="windows-1252" > > > On 29 Dec 2014, at 15:16, Rob Arthan <r...@lemma-one.com> wrote: > > > David, > > > > On 28 Dec 2014, at 05:08, David Topham <dtop...@gmail.com> wrote: > > > ...However, I don?t get much further with QCheck. Even when I try to load > > it directly from poly, I get the following error message: > > > > > PolyML.make "QCheck"; > > Making QCheck > > Making QCheckVersion > > Created structure QCheckVersion > > structure QCheckVersion : > > sig val context : string val version : int * int end > > Error- in 'QCheck.sml', line 14. > > Structure (RandGen) has not been declared Found near RandGen > > > > Did you have to do something else to QCheck to get it to work? > > I don?t know what was going on here. The above error occurred repeatedly > before I made this posting but I can no longer reproduce it. Here, for > the record, is ProofPower-ML code to build QCheck and run David?s > example: > > OS.FileSys.chDir "/Users/rda/bld/qcheck/qcheck-1.0/src?; (* change as > appropriate *) > structure PPList = List; > structure List = SML97BasisLibrary.List; > PolyML.make (translate_for_output "QCheck"); (* or PolyML.make > "%Q%Check"; *) > open %Q%Check; > fun checkSum n = n = n ; > val int = (Gen.Int.int, SOME Int.toString) ; > checkGen int ("unit test", pred checkSum) ; > > In the above ?%Q%? lets you generate something whose underlying Standard ML > representation is single Q. The only additional wrinkle is that ProofPower > overwrites the Basis Library binding for the structure List, but it also > keeps > a copy of the original so you can get it back again if you need it > > Regards, > > Rob. > > > -------------- next part -------------- > An HTML attachment was scrubbed... > URL: < > http://lemma-one.com/pipermail/proofpower_lemma-one.com/attachments/20141229/2bc14cdd/attachment-0001.html > > > > ------------------------------ > > Subject: Digest Footer > > _______________________________________________ > Proofpower mailing list > Proofpower@lemma-one.com > http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com > > > ------------------------------ > > End of Proofpower Digest, Vol 88, Issue 8 > ***************************************** >
_______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
