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