Rob Arthan wrote:
On 5 Jun 2011, at 12:10, Phil Clayton wrote:

I suppose this is a good opportunity to raise item 219, i.e.

1. Should the Spivey-Z schema decoration S' be supported in ProofPower-Z? I believe Standard-Z requires one of

 (S)'
 S '

to decorate a schema reference S. This avoids the question of what happens when both S and S' are global variable names.


Yes. Horrible isn't it. The space is barbaric by usual mathematical typographical standards and is an incompatibility with Spivey Z.

Horrible, it is, and I am in favour of supporting Spivey-Z except as in point 2 below.


2. Should ProofPower-Z allow S ' to be interpreted as the name S', i.e. ignoring space between the two tokens and taking them as one token? I would never expect e.g. abc def to be taken as the name abcdef.

Apart from the above comment about _mathematical_ typography rather than programming language practice, I really don't want to get into a debate about why it should or should not be as it is, since I went into this kind of question very carefully and at some length during the Z standardisation process (see the document Issues for Concrete Syntax at http://www.lemma-one.com/zstan_docs/zstan_docs.html). ProofPower-Z implements the scheme described there that is backwards compatible with Spivey in all but very obscure cases. This was a typical case where one existing tool implemented a thought-through approach which gave the desired new semantics using a syntax that was designed to be compatible with Spivey at least in typical cases, but, while no other tool supported either the desired semantics or the syntax, the standards committee chose a different and incompatible approach.

On practical grounds, I'm not a huge fan of the choice made (Decor.3) either.

I'll just summarize my point in relation to Spivey-Z. Lexing S ' as two separate tokens in ProofPower-Z would cause ' to be parsed as a schema decoration so type checking would require S to have schema type. This would:

1. Rule out Spivey-Z specifications where identifiers contain white space before any decoration, e.g.
  x '
which would need to be written as
  x'
Hopefully nobody does or would want to write identifiers in such a way. I think it's really horrible to see x ' for the identifier x' where the ' has no special significance - just the last character of the name. In fact, it doesn't even have to be on the same line:
  0 < x
  '

2. Give compatibility with Standard-Z in the following obscure case:

Note that when both S and S' are global variable names, S ' is a reference to S' in ProofPower-Z, not the schema decoration of S. Not only is this surprising, it is different to Standard-Z. (Section 7.3 in Z Standard.)

Of course, only the seriously crazed declare global variables with decoration on them.

I agree, it's best avoided.


Currently, my thinking is that a separate Standard-Z compatible parser would be a useful adjunct to ProofPower-Z, but I am still much interested in some level of backwards compatibility with Spivey Z, because all the significant specs I have come across in industry are in Spivey Z. So I have no plans to throw away the existing parser.

I don't think the impact on Spivey-Z is too bad but understand your reasons for keeping it this way. I'm not hell bent on conforming to the Standard though - I really don't like the way the language allows an identifier to be input containing white space!

Phil




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

Reply via email to