Re: [ProofPower] Trying to Prove my Zed Specifications

2012-08-26 Thread Anthony Hall
Dear All I've just got back from holiday (yes, thank you :-) ) and have been reading the discussion of ProofPower/Z Word Tools with interest. As Rob said, we have been discussing whether and how to integrate the two tools, and we did agree that a first step was to make PP work with Unicode. ZWT e

Re: [ProofPower] Question - Step After Proof Verification?

2012-09-18 Thread Anthony Hall
/papers_on_formal_methods.html, particularly Correctness by Construction: Developing a Commercial Secure System, Anthony Hall and Roderick Chapman, IEEE Software Jan/Feb 2002, pp18-25 and Using Formal Methods to Develop an ATC Information System,Anthony Hall, IEEE Software, March 1996, pp 66-76. Hope this

Re: [ProofPower] Updated Unicode translation scheme

2015-03-30 Thread Anthony Hall
Dear Rob I have just one small query - about the minus sign problem I had a lot of trouble with this, as you might expect, when translating between Spivey latex and standard Z, but it can be done. I don’t know whether translating from Proofpower is more difficult, but it would be nice to

Re: [ProofPower] Updated Unicode translation scheme

2015-03-30 Thread Anthony Hall
Thanks Rob My problem is that I need a lexical translation scheme that is not just specific to Z, but one that makes sense for any of the open-ended set of languages that ProofPower supports. I certainly don’t want to translate ASCII characters to non-ASCII. I just don’t think ISO Z got thi

Re: [ProofPower] Distributed concatenation symbol

2016-11-27 Thread Anthony Hall
Dear Rob I think the changes you suggest are good from the point of view that they bring the mapping into line with the Z standard (which you may not like) and therefore other tools (which you also may not like, but is nevertheless a Good Thing IMO) All the best Anthony From: Pro