czt-devel — For programmers using the CZT code

Re: [CZT-Devel] theorem environment - comments pls?

[Tim M. <tm...@un...>]

On 24/06/11 03:44, Anthony Hall wrote:
> Hmm, that's something that hadn't occurred to me. Certainly you can input
> ─
> X==ℙ ℕ
> N == 10
> └
>
> quite happily into CZT. But I agree, looking at the standard, it's not obvious that this should be allowed. (But it would be catastrophic for backward compatibity if it weren't)
>
> Can anyone more knowledgeable about the standard explain this?
>
The standard does not allow this, but yes, I designed the CZT parser to 
support it. It will accept any valid Z specification as defined by the 
standard, plus a few additions such as this for backward compatibility

Leo wrote:
>> The issue with Theorem is the same, but slightly worse because ConjPara may appear both within "unboxed para list" or as
>> "\begin{theorem}" environments (e.g., they both render as ZEDCHAR)... Does this make sense? How to reconcile those?
>
I think this was the reason for the theorem environments right? To 
remove this problem? The details are hazy for me though...

Cheers,
Tim

Re: [CZT-Devel] theorem environment - comments pls?

[Anthony H. <an...@an...>]

Leo

> Anthony, I don't have access to the ISO-Z doc or corrigendum :-( ; I'd love to > have a copy of it, please...
 
The standard and corrigendum are available free from 
http://www.iso.org/iso/iso_catalogue/catalogue_tc/catalogue_detail.htm?csnumber=21573 (It's not quite obvious - you have to click the link on the note under the Media and Price section.) Let me know if you need me to forward them.
 
> Thanks for reminding me about the UNICODE/LaTeX functionalities, and yes, you > are right. 
> 
> Trouble is, that as it stands, (I think) there is already such a 
> differentiation in some places. For example:
> 
> 
> \begin{zed}
>     X == \power \nat 
>     \\
>     N == 10 
> \end{zed}
> 
> after parsing gets printed as
> 
> \begin{zed}
> X == \power \nat
> \end{zed}
> \begin{zed}
> N == 10
> \end{zed}
> 
> I think that's because the parsing transforms the "unboxed para list" as
> ZEDCHAR Para 1 END  ZEDCHAR Para2 END etc.
> In this case, Unicode is "more expressive"(?) than LaTeX, given the problem
> doesn't happen there, and both of the above is just
> 
> └ ─ X == ℙ ℕ 
> └ ─ N == 10 

Hmm, that's something that hadn't occurred to me. Certainly you can input
─
X==ℙ ℕ
N == 10
└
 
quite happily into CZT. But I agree, looking at the standard, it's not obvious that this should be allowed. (But it would be catastrophic for backward compatibity if it weren't) 

Can anyone more knowledgeable about the standard explain this?
 
> The issue with Theorem is the same, but slightly worse because ConjPara may appear both within "unboxed para list" or as
> "\begin{theorem}" environments (e.g., they both render as ZEDCHAR)... Does this make sense? How to reconcile those?

Are you saying that in the LaTeX you don't have to use the theorem environment? 

> I would say, for \begin{theorem}, we should have something like a THEOREMCHAR (or CONJECTURECHAR, rather).

I'm not sure whether that's really necessary - we can after all recognise it from the vdash (unless it could get mixed up with other paragraphs between the same start/end symbols).

Good luck!

Anthony

 

Re: [CZT-Devel] theorem environment - comments pls?

[<rd...@le...>]

Oops, My mistake!

> Hi everyone,
>
>> ------
>> The standard is also flawed in not supporting generic formal parameters
>> on
>> conjectures, so most useful conjectures about generics cannot be
>> expressed.
>> ProofPower-Z allows the predicate to the right of the conjecture symbol
>> to
>> be preceded by a generic formal parameter list. Does CZT offer any
>> workaround for this?
>>
> I'm not entirely sure what the above means. Rob, do you mean that the
> standard does not support the following?
>
> \begin{zed}
>    [X,Y,Z] \vdash? some_predicate(X,Y,Z)
> \end{zed}
>
> This is most definitely supporting by the Z standard -- at least the
> early releases that CZT was built from. But perhaps I'm reading your
> meaning correctly?
>

I misread the grammar.

Regards,

Rob.

Re: [CZT-Devel] theorem environment - comments pls?

[Tim M. <tm...@un...>]

Hi everyone,

> ------
> The standard is also flawed in not supporting generic formal parameters on
> conjectures, so most useful conjectures about generics cannot be expressed.
> ProofPower-Z allows the predicate to the right of the conjecture symbol to
> be preceded by a generic formal parameter list. Does CZT offer any
> workaround for this?
>
I'm not entirely sure what the above means. Rob, do you mean that the 
standard does not support the following?

\begin{zed}
   [X,Y,Z] \vdash? some_predicate(X,Y,Z)
\end{zed}

This is most definitely supporting by the Z standard -- at least the 
early releases that CZT was built from. But perhaps I'm reading your 
meaning correctly?

Cheers,
Tim

Re: [CZT-Devel] theorem environment - comments pls?

[Leo F. <leo...@ne...>]

Hi,

Thanks for this. I've looked into PPZ on this as well (see the last posts wiht ref to 
http://www.lemma-one.com/zstan_docs/wrk036.ps).

Rob, yes, I got the idea from PPZ (e.g., generic actuals prior to the \vdash? symbol)
and played with it as a parsing rule like

THEOREM name:n optNL optFormalParameters:ofp CONJECTURE predicate:p

Anthony, I don't have access to the ISO-Z doc or corrigendum :-( ; I'd love to have a copy of it, please...
Thanks for reminding me about the UNICODE/LaTeX functionalities, and yes, you are right. 

Trouble is, that as it stands, (I think) there is already such a differentiation in some places. For example:

\begin{zed}
    X == \power \nat 
    \\
    N == 10 
\end{zed}

after parsing gets printed as

\begin{zed}
X == \power \nat
\end{zed}
\begin{zed}
N == 10
\end{zed}

I think that's because the parsing transforms the "unboxed para list" as ZEDCHAR Para 1 END  ZEDCHAR Para2 END etc.
In this case, Unicode is "more expressive"(?) than LaTeX, given the problem doesn't happen there, and both of the above is just

└ ─ X == ℙ ℕ 
└ ─ N == 10 

The issue with Theorem is the same, but slightly worse because ConjPara may appear both within "unboxed para list" or as
"\begin{theorem}" environments (e.g., they both render as ZEDCHAR)... Does this make sense? How to reconcile those?

I would say, for \begin{theorem}, we should have something like a THEOREMCHAR (or CONJECTURECHAR, rather).
About a symbol, I don't know. Looking into Unicode charts, I think the ones from http://www.unicode.org/charts/PDF/U2500.pdf
are the closest (?), and there is 2520 or 2523 or  ....????

Once again many thanks for the feedback.

Best,
Leo

On 23 Jun 2011, at 09:05, Anthony Hall wrote:

> Leo
> 
> I should also say that I have been talking to Rob Arthan about this, partly
> because I am hoping to offer ProofPower support in ZWT. He wrote the
> following:
> 
> ------
> The ProofPower concrete syntax for conjectures has an optional name at the
> beginning which can be used to retrieve the conjecture, e.g., to start a
> proof of it.
> 
> Historically, the issue was that a lot of texts used the turnstile as part
> of a notation for writing down a theorem with a list of predicates to the
> left of the turnstile denoting assumptions of the theorem. Since the
> assumption list is often just a single schema reference, you'd need some
> extra syntactic sugar to distinguish a name to identify the theorem.
> Typicallly this usage was in writing proofs and the standard committee
> agreed not to try to standardise notations for proofs. We did want to give a
> facility for stating potential theorems, i.e., conjectures, as this was
> (rightly in my view) perceived as a specification activity just as much as a
> proof activity. There is no loss of generality in requiring conjectures to
> be stated with any assumptions given as antecedents of an implication (say)
> on the right, so there is no need for an assumption list to the left of the
> conjecture symbol and you can reserve that position for a name to identify
> the conjecture. But the optional name didn't make it into the concrete
> syntax in the standard.
> 
> The standard is also flawed in not supporting generic formal parameters on
> conjectures, so most useful conjectures about generics cannot be expressed.
> ProofPower-Z allows the predicate to the right of the conjecture symbol to
> be preceded by a generic formal parameter list. Does CZT offer any
> workaround for this?
> ------
> 
>> Is this what you are referring to? Or is there another source with more
> explanations?
> 
> I was actually talking about the Technical Corrigendum to the Standard,
> which you can get from the ISO site. I'll send you a copy if you want.
> 
>> By the way, what's the veiew/need for the "\vdash?" within a >
> \begin{theorem}{NAME} PRED \end{theorem} environment?
>> I mean, I can see the need for its presence because of it appearing within
> 
>> unboxed paragraphs, but within a \begin{theorem}, I can't.
> 
> Right, but in the unicode you would need it. 
> 
>> Also,  I was thinking about how to pass the "options" (e.g., rewrite rule,
> type judgement,
> elimination rule, etc) to it and am still going around it.
> 
> Ah, I don't know about that - perhaps that's more a matter for the proof
> tool.
> 
>> The printing is indeed a pain, given the fact ZEDCHAR would break the
> parse-print-parse cycle... :-(
> Perhaps I  will add a "tag" to say a conjecture come from a 'begin{theorem};
> 
> I think it would be better if you could avoid that, because it would
> preserve the fact that the LaTeX markup was richer than the unicode.
> 
> I think allowing an optional name before the vdash would be a small and
> reasonable extension to the standard. I don't know about Rob's point about
> generics - perhaps the name could include generic parameters like a schema
> name? Incidentally, do you know how it \begin{theorem}{name} should render?
> I'd like to make the Z Word Tools version look nice.
> 
> Anthony
> 
> 

Re: [CZT-Devel] theorem environment - comments pls?

[Anthony H. <an...@an...>]

Leo

I should also say that I have been talking to Rob Arthan about this, partly
because I am hoping to offer ProofPower support in ZWT. He wrote the
following:

------
The ProofPower concrete syntax for conjectures has an optional name at the
beginning which can be used to retrieve the conjecture, e.g., to start a
proof of it.

Historically, the issue was that a lot of texts used the turnstile as part
of a notation for writing down a theorem with a list of predicates to the
left of the turnstile denoting assumptions of the theorem. Since the
assumption list is often just a single schema reference, you'd need some
extra syntactic sugar to distinguish a name to identify the theorem.
Typicallly this usage was in writing proofs and the standard committee
agreed not to try to standardise notations for proofs. We did want to give a
facility for stating potential theorems, i.e., conjectures, as this was
(rightly in my view) perceived as a specification activity just as much as a
proof activity. There is no loss of generality in requiring conjectures to
be stated with any assumptions given as antecedents of an implication (say)
on the right, so there is no need for an assumption list to the left of the
conjecture symbol and you can reserve that position for a name to identify
the conjecture. But the optional name didn't make it into the concrete
syntax in the standard.

The standard is also flawed in not supporting generic formal parameters on
conjectures, so most useful conjectures about generics cannot be expressed.
ProofPower-Z allows the predicate to the right of the conjecture symbol to
be preceded by a generic formal parameter list. Does CZT offer any
workaround for this?
------

> Is this what you are referring to? Or is there another source with more
explanations?

I was actually talking about the Technical Corrigendum to the Standard,
which you can get from the ISO site. I'll send you a copy if you want.

> By the way, what's the veiew/need for the "\vdash?" within a >
\begin{theorem}{NAME} PRED \end{theorem} environment?
> I mean, I can see the need for its presence because of it appearing within

> unboxed paragraphs, but within a \begin{theorem}, I can't.

Right, but in the unicode you would need it. 

>Also,  I was thinking about how to pass the "options" (e.g., rewrite rule,
type judgement,
elimination rule, etc) to it and am still going around it.

Ah, I don't know about that - perhaps that's more a matter for the proof
tool.

> The printing is indeed a pain, given the fact ZEDCHAR would break the
parse-print-parse cycle... :-(
Perhaps I  will add a "tag" to say a conjecture come from a 'begin{theorem};

I think it would be better if you could avoid that, because it would
preserve the fact that the LaTeX markup was richer than the unicode.

I think allowing an optional name before the vdash would be a small and
reasonable extension to the standard. I don't know about Rob's point about
generics - perhaps the name could include generic parameters like a schema
name? Incidentally, do you know how it \begin{theorem}{name} should render?
I'd like to make the Z Word Tools version look nice.

Anthony

Re: [CZT-Devel] theorem environment - comments pls?

[Leo F. <leo...@ne...>]

Hi Anthony,

Thanks for this. I found the document

ftp://ftp.cs.york.ac.uk/hise_reports/cadiz/ZSTAN/defects/begintheorem.pdf

Is this what you are referring to? Or is there another source with more explanations?

By the way, what's the veiew/need for the "\vdash?" within a \begin{theorem}{NAME} PRED \end{theorem} environment?
I mean, I can see the need for its presence because of it appearing within unboxed paragraphs, but within a \begin{theorem}, I can''t.
Also,  I was thinking about how to pass the "options" (e.g., rewrite rule, type judgement,
elimination rule, etc) to it and am still going around it.

The printing is indeed a pain, given the fact ZEDCHAR would break the parse-print-parse cycle... :-(
Perhaps I  will add a "tag" to say a conjecture come from a 'begin{theorem};

Thanks,
Leo

On 22 Jun 2011, at 21:00, Anthony Hall wrote:

Mark wrote


The first step is to define a way of passing the theorem name through the unicode representation (and then into the AST).  (I think that was put in the too-hard-right-now basket when the theorem environment was added to the standard).
I’ve just looked at the technical corrigendum to the standard, and it is quite extraordinary. It includes a latex markup \begin{theorem}{name} and then makes the absurd rule that “The mark-up \begin{theorem}{name} shall be converted to a ZEDCHAR character”

What on earth was the idea of that? Why lose the name? It is complete nonsense since the unicode is supposed  to be the canonical representation, isn’t it?

Anyway, Leo, if you do come up with some simple rule (what’s wrong with “everything up to the first newline is the name”?) I will restore theorem paragraphs to the Z word tools and export them to CZT.

Anthony
<ATT00001..txt><ATT00002..txt>

Re: [CZT-Devel] theorem environment - comments pls?

[Leo F. <leo...@ne...>]

Hi Tim,

If I remember correctly, at the time, there was discussion about this feature being non-standard.
The "begin{theorem} environment was added, so long as it was scanned as 

ZEDCHAR *whatever \vdash? PRED END or NL

I've added this rule to cope with names, but it wasn't there originally. The \begin{theorem} environment
scans it this way. (ignoring names). I decided to add the rule to play around and see what to do. 
As you noticed, I don't change ConjPara structure itself, but add the name as an attribute, if one exists.
I've stopped there. There is also printing of theorem environments as plain ZEDCHAR (I don't recall, but
I think I didn't do this bit), so that parse-print-parse wouldn't give you the begin{theorem}{name} anymore.

I knew this was a half-backed solution, but given the standard status and our conformance plea, I kept it experimental.
I think it was meant (if not originally added like) a <add:circus> extension only.

\begin{theorem}{NAME} is scanned with "{NAME}" as the theorem name, which is obviously unsatisfactory.

I will look into this and sort it out more thoroughly soon. The solution I envisage is as follows:

a) keep the ASTs as-is for now (e.g., do not change ConjPara to have a ZName)
b) if names are present in ZED NAME \vdash?, add then as Term Anns wth auxiliary methods for access
c) \begin{theorem} *must* always have a NAME
c) fix the parsing / lexing  rules. 
d) printing \begin{theorem} is a problem given it doesn't have it's own "THEOREM" token, but just ZED.

For this, I will add another annotation to the conjecture to say it came from a "theorem" environment. A simpler
solution would be perhaps to just have \begin{theorem} for ConjPara with names, and \vdash? otherwise... Will see...

I will look into this soon and come back to you. As Tim says, I don't think it will be hard.

Many thanks for all the comments.

Best,
Leo

On 23 Jun 2011, at 00:19, Tim Miller wrote:

> Just glancing at the CZT grammar, there is a rule:
> 
> THEOREM name:n optNL optFormalParameters:ofp CONJECTURE predicate:p
> 
> The name "n" is annotated to the conjecture paragraph that is produced. 
> However, it appears the corresponding scanner rule is commented out, 
> which means there should be an error thrown if the parser encounters 
> this. There also appears to get a "name" attribute in the ConjPara 
> class. It indicates that someone (I don't think it was me!) has partly 
> implemented some of this in the past.
> 
> Leo, do you know why the scanner rule has been commented out? More 
> importantly, how is a paragraph such as "\begin{theorem}{NAME}" being 
> parsed at the moment? (I don't have time to investigate at the moment).
> 
> It doesn't appear that implementing this is the grammar would be difficult.
> 
> Cheers,
> Tim
> 
> 
> Anthony Hall wrote:
>> Mark wrote
>> 
>> 
>> 
>> 
>> The first step is to define a way of passing the theorem name through 
>> the unicode representation (and then into the AST).  (I think that was 
>> put in the too-hard-right-now basket when the theorem environment was 
>> added to the standard).
>> 
>> I’ve just looked at the technical corrigendum to the standard, and it is 
>> quite extraordinary. It includes a latex markup \begin{theorem}{name} 
>> and then makes the absurd rule that “The mark-up \begin{theorem}{name} 
>> shall be converted to a ZEDCHAR character”
>> 
>> 
>> 
>> What on earth was the idea of that? Why lose the name? It is complete 
>> nonsense since the unicode is supposed  to be the canonical 
>> representation, isn’t it?
>> 
>> 
>> 
>> Anyway, Leo, if you do come up with some simple rule (what’s wrong with 
>> “everything up to the first newline is the name”?) I will restore 
>> theorem paragraphs to the Z word tools and export them to CZT.
>> 
>> 
>> 
>> Anthony
>> 
>> 
>> ------------------------------------------------------------------------
>> 
>> ------------------------------------------------------------------------------
>> Simplify data backup and recovery for your virtual environment with vRanger.
>> Installation's a snap, and flexible recovery options mean your data is safe,
>> secure and there when you need it. Data protection magic?
>> Nope - It's vRanger. Get your free trial download today.
>> http://p.sf.net/sfu/quest-sfdev2dev
>> 
>> 
>> ------------------------------------------------------------------------
>> 
>> _______________________________________________
>> CZT-Devel mailing list
>> CZT...@li...
>> https://lists.sourceforge.net/lists/listinfo/czt-devel
> 
> 
> ------------------------------------------------------------------------------
> Simplify data backup and recovery for your virtual environment with vRanger.
> Installation's a snap, and flexible recovery options mean your data is safe,
> secure and there when you need it. Data protection magic?
> Nope - It's vRanger. Get your free trial download today.
> http://p.sf.net/sfu/quest-sfdev2dev
> _______________________________________________
> CZT-Devel mailing list
> CZT...@li...
> https://lists.sourceforge.net/lists/listinfo/czt-devel

Re: [CZT-Devel] theorem environment - comments pls?

[Tim M. <tm...@un...>]

Just glancing at the CZT grammar, there is a rule:

THEOREM name:n optNL optFormalParameters:ofp CONJECTURE predicate:p

The name "n" is annotated to the conjecture paragraph that is produced. 
However, it appears the corresponding scanner rule is commented out, 
which means there should be an error thrown if the parser encounters 
this. There also appears to get a "name" attribute in the ConjPara 
class. It indicates that someone (I don't think it was me!) has partly 
implemented some of this in the past.

Leo, do you know why the scanner rule has been commented out? More 
importantly, how is a paragraph such as "\begin{theorem}{NAME}" being 
parsed at the moment? (I don't have time to investigate at the moment).

It doesn't appear that implementing this is the grammar would be difficult.

Cheers,
Tim


Anthony Hall wrote:
> Mark wrote
> 
>  
> 
> 
> The first step is to define a way of passing the theorem name through 
> the unicode representation (and then into the AST).  (I think that was 
> put in the too-hard-right-now basket when the theorem environment was 
> added to the standard).
> 
> I’ve just looked at the technical corrigendum to the standard, and it is 
> quite extraordinary. It includes a latex markup \begin{theorem}{name} 
> and then makes the absurd rule that “The mark-up \begin{theorem}{name} 
> shall be converted to a ZEDCHAR character”
> 
>  
> 
> What on earth was the idea of that? Why lose the name? It is complete 
> nonsense since the unicode is supposed  to be the canonical 
> representation, isn’t it?
> 
>  
> 
> Anyway, Leo, if you do come up with some simple rule (what’s wrong with 
> “everything up to the first newline is the name”?) I will restore 
> theorem paragraphs to the Z word tools and export them to CZT.
> 
>  
> 
> Anthony
> 
> 
> ------------------------------------------------------------------------
> 
> ------------------------------------------------------------------------------
> Simplify data backup and recovery for your virtual environment with vRanger.
> Installation's a snap, and flexible recovery options mean your data is safe,
> secure and there when you need it. Data protection magic?
> Nope - It's vRanger. Get your free trial download today.
> http://p.sf.net/sfu/quest-sfdev2dev
> 
> 
> ------------------------------------------------------------------------
> 
> _______________________________________________
> CZT-Devel mailing list
> CZT...@li...
> https://lists.sourceforge.net/lists/listinfo/czt-devel

Re: [CZT-Devel] theorem environment - comments pls?

[Anthony H. <an...@an...>]

Mark wrote

 


The first step is to define a way of passing the theorem name through the
unicode representation (and then into the AST).  (I think that was put in
the too-hard-right-now basket when the theorem environment was added to the
standard).

I've just looked at the technical corrigendum to the standard, and it is
quite extraordinary. It includes a latex markup \begin{theorem}{name} and
then makes the absurd rule that "The mark-up \begin{theorem}{name} shall be
converted to a ZEDCHAR character"

 

What on earth was the idea of that? Why lose the name? It is complete
nonsense since the unicode is supposed  to be the canonical representation,
isn't it?

 

Anyway, Leo, if you do come up with some simple rule (what's wrong with
"everything up to the first newline is the name"?) I will restore theorem
paragraphs to the Z word tools and export them to CZT.

 

Anthony

Re: [CZT-Devel] theorem environment - comments pls?

[Anthony H. <an...@an...>]

Apologies, this bit of my last post wasn't very sensible:

 

...  (what's wrong with "everything up to the first newline is the name"?)
....

 

because of course we don't even know it's a theorem para till we get to the
vdash. Sorry. 

Perhaps since the standard doesn't allow an antecedent one could take
everything between the ZED and the vdash? as the name?

 

Anthony

Re: [CZT-Devel] theorem environment - comments pls?

[Leo F. <leo...@ne...>]

Hi Mark,

Thanks for that. I will look into it and try to take into account possible varieties as much as possible.
I tried to find the new version of the standard online, but could only get the "usual" one.

Looking further I found this discussion by Rob Arthan

http://www.lemma-one.com/zstan_docs/wrk036.ps

which is quite positive /straightforward (see Sec. 10).

I will start on it soon, and come back to you when I've got something...

Best,
Leo

On 21 Jun 2011, at 00:07, Mark Utting wrote:

Leo

You wrote:
Looking around CZT I've seen not much is used / taken advantage for the {theorem} environments.
So, I thought to revisit its implementation / discuss the topic, given I will need some solution to the
problem above, even if just locally coded...


Good idea.

The first step is to define a way of passing the theorem name through the unicode representation (and then into the AST).  (I think that was put in the too-hard-right-now basket when the theorem environment was added to the standard).

 Cheers
Mark

Re: [CZT-Devel] theorem environment - comments pls?

[Mark U. <ma...@cs...>]

Leo

You wrote:

> Looking around CZT I've seen not much is used / taken advantage for the
> {theorem} environments.
> So, I thought to revisit its implementation / discuss the topic, given I
> will need some solution to the
> problem above, even if just locally coded...
>
>
Good idea.

The first step is to define a way of passing the theorem name through the
unicode representation (and then into the AST).  (I think that was put in
the too-hard-right-now basket when the theorem environment was added to the
standard).

 Cheers
Mark

[CZT-Devel] theorem environment - comments pls?

[Leo F. <leo...@ne...>]

Hi guys,

I am writing up a tool that parses a Z spec with theorem information to be processed for (meta-)reasoning about proofs
(e.g., load Z sections with theorems and proofs in order to try and *learn/deduce* proofs / patterns from them).

I then hit a few problems because of the shape of the Theorem environment. The Std has ConjPara as part of a unboxed
paragraph, and the "\vdash?" as "tagging" to know this is a predicate for a conjecture. 

When we added "theorem" environments to the scanner (Revision 5047), this was to tokenise the environments as

\begin{theorem} .... \end{theorem}

Because the standard doesn't have it per se, the theorem "NAME" was left out as part of the token "theorem" itself. 
The parser "accepts" both

\begin{theorem}{NAME}  .... \end{theorem} and \begin{theorem} \end{theorem}

Another small issue the "\vdash?" tokens within the "theorem" environment: it's kind of pointless, we know it's a conjecture :-)
 
===

My problem is that this "half-way" solution is neither Z Standard, nor as useful to theorem prover(s). Without the name,
and other tags needed (e.g., rewrite rule, type judgement, etc; or ability as in take as enabled/disabled/elimination/introduction rule etc),
these are kind of a missed opportunity.  

There are four theorem proving environments for Z (that I am aware) of:
a) CadiZ			b) HOL-Z 	c) ProofPowerZ		d) Z/Eves		

I guess all of them (I've never used CadiZ), there are ways to declare and "tag" conjectures in different forms for different purposes;
all of them have a name for referencing within proof, say.

Looking around CZT I've seen not much is used / taken advantage for the {theorem} environments.
So, I thought to revisit its implementation / discuss the topic, given I will need some solution to the 
problem above, even if just locally coded...

Comments?

Best,
Leo

 

Re: [CZT-Devel] inner + outer syntax

[Leo F. <leo...@ne...>]

Hi Mark,

Hum, I see. Perhaps naively, what I had in mind was simple(r): multi-pass parsing on specific productions tagged as "outer",
then, if those are fine, on the remaining (or the reminder / all) productions tagged as "inner".

ex:
OUTER:
Section ; Sect Header ; whole Para-subtree
INNER:
Anything within Para-subtree (e.g., Decl, Pred, Expr)

In this way, I would only check the para-subtree on a first pass, then the whole spec(?) or the inner parts on a second pass.

Here are some motivations: Circus, differently from Z, is an evolving language; we get things like time, OO, pointers,
synchronicity, etc added. As time passed, this leads to small (and sometimes complicated) changes. Yet, the changes
are almost always within the Para-subtree, and never at the "outer" level per se. On Z, I sometimes get requests / questions
regarding "spec-holes" (e.g., like jokers but not quite) for Expr and Pred at certain places, where they need to be "consumed"
as is, and just "warned" about type uncertainty.

I am now looking into VDM tools (and somewhat Event-B tools) and seeing that business of inner/outer quite handy in their case.
I will think this more thoroughly. Thanks for the comments :-)

Best,
Leo

On 17 Jun 2011, at 03:05, Mark Utting wrote:

Leo,

On 17 June 2011 01:10, Leo Freitas <leo...@ne...<mailto:leo...@ne...>> wrote:
Hi,

Tools in other methods (e.g., Rodin for Event-B and VDMTools/Overture for VDM) have an interesting separation
between so-called inner and outer syntax. This makes parsing/typechecking error messages, when the error is
somewhat hidden quite neatly clear / easy to understand. Another advantage is that it creates language "categories",
which can then be "extended" (e.g., outer syntax - structure - is fixed, yet inner syntax - details - can change, in Event-B).

A common way of doing this is to unfold some of the concrete (outer) syntax into more primitive notions (abstract syntax) internally, so that your internal syntax is simpler than the external.

Having different inner and outer syntax sounds like it would make it *harder* to get good error messages (Because you'd have to translate inner syntax into outer syntax).  But it might have the advantage of allowing more change to the inner syntax (of course, that still requires rewriting/updating all the tools that manipulate the inner syntax, which is enough to make such changes impractical!).

I don't really see any advantage to having separate inner and outer syntax, unless you expect one of them to change a lot.


Is there anything like that for Z somewhere? It would be nice to have something like it I guess... Any comments?


There's not really anything like that in CZT.  The CZT abstract syntax (inner) is quite close to the concrete syntax.  The goal was to make it as abstract as possible, while still retaining an isomorphism between the AST and the concrete syntax.  So typically, several concrete structures are mapped onto one AST structure, with a flag/enum to say which of the concrete representations it came from.

Cheers
Mark

<ATT00001..txt><ATT00002..txt>

Re: [CZT-Devel] inner + outer syntax

[Mark U. <ma...@cs...>]

Leo,

On 17 June 2011 01:10, Leo Freitas <leo...@ne...> wrote:

> Hi,
>
> Tools in other methods (e.g., Rodin for Event-B and VDMTools/Overture for
> VDM) have an interesting separation
> between so-called inner and outer syntax. This makes parsing/typechecking
> error messages, when the error is
> somewhat hidden quite neatly clear / easy to understand. Another advantage
> is that it creates language "categories",
> which can then be "extended" (e.g., outer syntax - structure - is fixed,
> yet inner syntax - details - can change, in Event-B).
>

A common way of doing this is to unfold some of the concrete (outer) syntax
into more primitive notions (abstract syntax) internally, so that your
internal syntax is simpler than the external.

Having different inner and outer syntax sounds like it would make it
*harder* to get good error messages (Because you'd have to translate inner
syntax into outer syntax).  But it might have the advantage of allowing more
change to the inner syntax (of course, that still requires
rewriting/updating all the tools that manipulate the inner syntax, which is
enough to make such changes impractical!).

I don't really see any advantage to having separate inner and outer syntax,
unless you expect one of them to change a lot.


> Is there anything like that for Z somewhere? It would be nice to have
> something like it I guess... Any comments?
>


There's not really anything like that in CZT.  The CZT abstract syntax
(inner) is quite close to the concrete syntax.  The goal was to make it as
abstract as possible, while still retaining an isomorphism between the AST
and the concrete syntax.  So typically, several concrete structures are
mapped onto one AST structure, with a flag/enum to say which of the concrete
representations it came from.

Cheers
Mark

[CZT-Devel] inner + outer syntax

[Leo F. <leo...@ne...>]

Hi,

Tools in other methods (e.g., Rodin for Event-B and VDMTools/Overture for VDM) have an interesting separation
between so-called inner and outer syntax. This makes parsing/typechecking error messages, when the error is
somewhat hidden quite neatly clear / easy to understand. Another advantage is that it creates language "categories",
which can then be "extended" (e.g., outer syntax - structure - is fixed, yet inner syntax - details - can change, in Event-B).

Is there anything like that for Z somewhere? It would be nice to have something like it I guess... Any comments?

Best,
Leo

[CZT-Devel] Fwd: [czt - Help] RE: About the 1.5.0 CZT Circus Parser

[Leo F. <leo...@ne...>]

Hi Samuel,

Right. I am pleased it worked out for you. By the way, it's quick/easier/nicer to have these messages/questions in the CZT mailing list (CC'ed).

A few tips about what you say on process names and on ProcessSignature/BasicProcess. As I said, Circus.xsd explains the structure of BasicProcess,
and why it has changed over time, which you can check under SVN logs.

For what you want (seems to)/need, the place to look is "getOnTheFlyPara()". Structurally, a basic process contains just a list of paragraphs, some
of which are "special" (e.g., main action, state schema, and on-the-fly actions). To keep the structure as abstract as possible (e.g., having explicit 
fields / methods for each "type/kind" leads to more programming when coding visitors on all tools!). So, the underlying structure is just a ZParaList,
which is itself a list of list of paragraphs. Perhaps one day, Circus shall be simplified to impose more specific / fixing structure-ordering. There are
pro/cons arguments to that effect: e.g., refinement calculation tools that rearrange/rewrite things on the fly and give it back to the user lead to this flexibility need, say.

Regarding BasicProcess structure, things get tricky. Circus, like Z, accepts loads of ways to define the same thing. For instance, a state schema can be given 
in 3 (or more) different ways: as a horizontal or boxed schema that could be generic or not; and could be named or on the fly; and it can have process parameters 
involved, etc (!!!) Many combinations are possible. Similarly, for the main action (nearly as varied). Also, the order of things is not quite sequential: an on-the-fly 
paragraph/action or various other parts might appear before the state schema, and after. Only the main action usually comes at the end. But, for stateless processes, 
even the state comes at the end as a dummy empty state element.  So, the underlying data structures are rather "loose".  This leads to a *rather inneficient implementation*
of BasicProcess interface. Imposing an "order" internally would mean loosing the original order (e.g., say when "printing it back" after parsing; counters/markers could
be added, say). Yet, so far, performance is acceptable. 

For the naming convention, "$$" simply means an "internal name", given the parser won't recognise such names (e.g., the user cannot/usually do not have a name with "$$").
That's all. The idea is that It's reserved for tool builders to have their own actions/processes/whatever written.

Best,
Leo

Begin forwarded message:

> From: "SourceForge.net" <no...@so...>
> Date: 11 May 2011 02:45:19 GMT+01:00
> To: no...@so...
> Subject: [czt - Help] RE: About the 1.5.0 CZT Circus Parser
> 
> 
> Read and respond to this message at: 
> https://sourceforge.net/projects/czt/forums/forum/295268/topic/4522055
> By: samuellincoln
> 
> Hi Leo
> 
> "Regarding your question, could I ask what is it you are changing it to? The
> "isMainActionValid" is an invariant guaranteeing that only one main action exist,
> which is sensible, since Circus has no semantics for processes with multiple
> main actions. If your change is making it == false, you must be doing something
> wrong in the process."
> 
> Yes, you're probably right. Probably the reason for the failure is something
> which is wrong in the process... During the change of the process to be changed,
> I have to copy a version of the main action of another process to the process
> to be changed, with it's name prefixed with "Previous". Thus, I add an action
> to a basic process called "Previous$$mainAction_...", or something like it.
> Maybe the "$$" is a kind of sub-sequence that identifies main actions.
> 
> I am going to check it now, but I am quite confident that your clues will help
> me to fix this problem.
> 
> Thank you very much
> 
> Samuel
> 
> _____________________________________________________________________________________
> You are receiving this email because you elected to monitor this topic or entire forum.
> To stop monitoring this topic visit: 
> https://sourceforge.net/projects/czt/forums/forum/295268/topic/4522055/unmonitor
> To stop monitoring this forum visit: 
> https://sourceforge.net/projects/czt/forums/forum/295268/unmonitor

[CZT-Devel] Z Word Tools now support ISO Standard Z

[Anthony H. <an...@an...>]

I'm pleased to announce the release of Version 2.0 of the Z Word Tools. The main new feature in this release is that you can write ISO Standard Z and typecheck your specification using a built in interface to the Community Z Tools (http://czt.sourceforge.net/) typechecker. I'm very grateful to Tim Miller, of the CZT project, for help with this. 

Of course Z Word Tools continues to support Spivey Z using fuzz and there need be no change to existing documents.

In addition there are other improvements especially for large specifications.

The new version is available at http://sourceforge.net/projects/zwordtools/ where there are full release notes.

I hope you find the new version useful. Please do let me know of any problems or comments


Anthony Hall

22 Hayward Road
Oxford OX2 8LW
UK

+44 (0) 7779 255147
an...@an...
www.anthonyhall.org

[CZT-Devel] Z printer (error?) with NL_AND

[Leo F. <leo...@ne...>]

Hi guys,

I just found a curious error(?) in the Z printer for NL_AND situations.
I had the following theorem.... Never mind the details, the point is that 
there is a " \\ " right after the "\emptyset" for what looks like a NL_AND.

There is also a missing closing parenthesis (or a parenthesis closed 
not quite in the right place). Still, the underlying AST does have the 
correct structure (phew...).... But you can imagine how this caused panic
at first: the generated VC is wrong? Or is there something being parsed funny?
Neither. 

Any suggestions on how to fix it? 

The trouble seems like in the printer and the way it needs to handle
NL_AND (e.g., context sensitive and).  Personally, I do think these many
versions of AND are unnecessary during a proof (e.g., they only make sense
within schemas for clarity). That is, one (easy) solution would be to always 
print the \land markup for NL_AND (and other fancy syntactic sugar like it). 

VC108 for line 1156 column 1 start 41205 length 739 in "tokeneer"
\begin{zed}
theorem~Admin\_ vc\_ dc108 \vdash ? \\
   \t2 \forall rolePresent : \Optional ADMINPRIVILEGE ; availableOps : \power ADMINOP ; \\
      \t5 currentAdminOp : \Optional ADMINOP | true @ \\
    \t3 ( rolePresent = \Nil \implies availableOps =~\emptyset \implies \\
      \t5 rolePresent \neq \Nil \implies \The \appliesTo rolePresent ) \land \\
     \t4 ( ( rolePresent = \Nil \implies availableOps =~\emptyset \\                  <======== HERE =======
       \t6 ( rolePresent \neq \Nil \land \The rolePresent = guard ) \implies \\
        \t7 availableOps = \{ overrideLock \} ) \implies \\
      \t5 rolePresent \neq \Nil \implies \The \appliesTo rolePresent ) \land \\
     \t4 ( ( rolePresent = \Nil \implies availableOps =~\emptyset \\
       \t6 ( rolePresent \neq \Nil \land \The rolePresent = guard ) \implies \\
        \t7 availableOps = \{ overrideLock \} \\
       \t6 ( rolePresent \neq \Nil \land \The rolePresent = auditManager ) \implies \\
        \t7 availableOps = \{ archiveLog \} ) \implies \\
      \t5 rolePresent \neq \Nil \implies \The \appliesTo rolePresent ) \land \\
     \t4 ( ( rolePresent = \Nil \implies availableOps =~\emptyset \\
       \t6 ( rolePresent \neq \Nil \land \The rolePresent = guard ) \implies \\
        \t7 availableOps = \{ overrideLock \} \\
       \t6 ( rolePresent \neq \Nil \land \The rolePresent = auditManager ) \implies \\
        \t7 availableOps = \{ archiveLog \} \\
       \t6 ( rolePresent \neq \Nil \land \The rolePresent = securityOfficer ) \implies \\
        \t7 availableOps = \{ updateConfigData , shutdownOp \} ) \implies \\
      \t5 currentAdminOp \neq \Nil \implies \The \appliesTo currentAdminOp )
\end{zed}

PS:
The VC is "right", as in accordance with the VC rules for domain checking conditions.
It is also "right" if diff'ed through the same VC in Z/Eves' output.

Best,
Leo

Re: [CZT-Devel] Old LaTeX printing problem

[Petra M. <Pet...@ec...>]

Hi Leo,

You wrote:
> So, for the Unicode2Latex, I do not add anything from "fuzz_toolkit" to the map,
> whereas Unicode2OldLatex does (?).

Yes, setting up the directive map as you want it to be for printing
could be a solution.

> Finally, there is one more issue: in Fuzz, there are a lot of common markup for
> different LaTeXx commands. That means, the problem is still there, if one wants
> to be "selective" (or indeed faithful to the original Old Tex file). That is, only the
> last one entered will be the one printed, even in Old LaTex...

Yes, and I don't really see an easy way of recording which LaTeX command
has been used originally.

> By the way, why there is an extra mapping there for \\num to ARITHMOS? Why isn't
> this in fuzz_toolkit itself?

I can't really remember but I think num is considered a built in type
(but I am just guessing).

Cheers,
Petra

Re: [CZT-Devel] Old LaTeX printing problem

[Leo F. <leo...@gm...>]

Hi Petra,

Yep... I see... this is a tricky one... Here is the thought process behind it --- if not yet a solution...

The source is indeed in LatexMarkupFunction
(e.g., commandToDirective map has 210 elements whereas unicodeToDirective
map has 180 elements when fuzz toolkit is around --- 30 of such "repetitions").

A "solution" per se isn't in trying to avoid the duplication at LatexMarkupFunction
(e.g., I tried that and it doesn't quite work as I expected - and leads to stack overflow).
Debugging this is very hard because the LMF get s created during CUP-parsing :-(

On the other hand, thinking about where the problem manifest itself = only when printing!
Since internally, there is no AST distinction between \forall or \all (!) --- the same for the other
29 repeated tokens. 

So, I went to Unicode2Latex.xml (parser-src) to see that the method se

protected void setupMarkupTable(LatexMarkupFunction table)  (line 308)

is the place where an underlying "unicode2latexMap" is created for printing. 
So, for the Unicode2Latex, I do not add anything from "fuzz_toolkit" to the map,
whereas Unicode2OldLatex does (?). This kind of make both Z/Eves and Fuzz 
into so-called "Old latex", which seems the most appropriate solution I could
come up with for now, and it works for what I intended. I also tested the explicit
"print old latex" to see, and it does use the fuzz_toolkit names accordingly.
Perhaps more tests are needed with Old LaTeX to see weather or not there are any unpredicted side-effect. :-(

Finally, there is one more issue: in Fuzz, there are a lot of common markup for
different LaTeXx commands. That means, the problem is still there, if one wants
to be "selective" (or indeed faithful to the original Old Tex file). That is, only the
last one entered will be the one printed, even in Old LaTex...

By the way, why there is an extra mapping there for \\num to ARITHMOS? Why isn't
this in fuzz_toolkit itself? Or is it because this is one where the difference is in the UNICODE
rather than in the LaTeX? In any case the underlying "unicode2latexMap" for this instance
has <String, LatexCommand> rather than <String, MarkupDirective>. 

I will commit these changes soon after doing some more tests.

Best,
Leo

On 17 Feb 2011, at 22:07, Petra Malik wrote:

> Hi Leo,
> 
>> In particular, the problem occurs / manifest itself here
>> 
>> net.sourceforge.czt.parser.util.LatexMarkupFunction.add(Directive)
>> and sometimes
>> net.sourceforge.czt.parser.util.LatexMarkupFunction.add(LatexMarkupFunction)
>> 
>> because the underlying maps already have a "key" for the given command being
>> overridden (e.g., the two maps  .put methods return non-null). 
>> 
>> Any suggestions on how to overcome this properly?
> 
> I think you've pinpointed the problem.  The LatexMarkupFunction class
> contains a map from a Unicode string to its LaTeX command and is created
> when a LaTeX specification is parsed.  If a specification defines
> several LaTeX commands for the same Unicode string (like \forall and
> \all) the one parsed later will just overwrite the one that has been put
> into the map earlier.
> 
> Are you looking for a nice, extensible solution or a quick fix?  My
> first quick idea is to change the behaviour of the LatexMarkupFunction
> class to not overwrite existing entries.
> 
> Any thoughts?
> Petra
> 
> ------------------------------------------------------------------------------
> The ultimate all-in-one performance toolkit: Intel(R) Parallel Studio XE:
> Pinpoint memory and threading errors before they happen.
> Find and fix more than 250 security defects in the development cycle.
> Locate bottlenecks in serial and parallel code that limit performance.
> http://p.sf.net/sfu/intel-dev2devfeb
> _______________________________________________
> CZT-Devel mailing list
> CZT...@li...
> https://lists.sourceforge.net/lists/listinfo/czt-devel

Re: [CZT-Devel] Old LaTeX printing problem

[Petra M. <Pet...@ec...>]

Hi Leo,

> In particular, the problem occurs / manifest itself here
> 
> net.sourceforge.czt.parser.util.LatexMarkupFunction.add(Directive)
> and sometimes
> net.sourceforge.czt.parser.util.LatexMarkupFunction.add(LatexMarkupFunction)
> 
> because the underlying maps already have a "key" for the given command being
> overridden (e.g., the two maps  .put methods return non-null). 
> 
> Any suggestions on how to overcome this properly?

I think you've pinpointed the problem.  The LatexMarkupFunction class
contains a map from a Unicode string to its LaTeX command and is created
when a LaTeX specification is parsed.  If a specification defines
several LaTeX commands for the same Unicode string (like \forall and
\all) the one parsed later will just overwrite the one that has been put
into the map earlier.

Are you looking for a nice, extensible solution or a quick fix?  My
first quick idea is to change the behaviour of the LatexMarkupFunction
class to not overwrite existing entries.

Any thoughts?
Petra

[CZT-Devel] Fwd: Old LaTeX printing problem

[Leo F. <leo...@gm...>]

Begin forwarded message:

> From: Leo Freitas <leo...@ne...>
> Date: 17 February 2011 15:47:09 GMT
> To: czt-devel <czt...@li...>
> Subject: Old LaTeX printing problem
> 
> Hi guys,
> 
> I am having the following problem:
> 
> a) a section FOO with fuzz_toolkit as a parent (e.g., the user spec)
> b) mixed old and new latex within - all parse/typecheck
> c) a section BAR with FOO as a parent (e.g., the VCs of FOO)
> 
> Now, trouble is I want BAR *NOT* to print \all or \exi for \forall,
> but unfortunately it does print OLD latex. And even if I ask a
> LatexCommand (rather than OldLatexCommand) directly, OLD
> LaTeX is still print :-(
> 
> If one removes fuzz_toolkit, then all goes to "normal". So, whenever
> any (transitive) parent does have fuzz_toolkit, the underlying markup 
> directives get overridden.
> 
> In particular, the problem occurs / manifest itself here
> 
> net.sourceforge.czt.parser.util.LatexMarkupFunction.add(Directive)
> and sometimes
> net.sourceforge.czt.parser.util.LatexMarkupFunction.add(LatexMarkupFunction)
> 
> because the underlying maps already have a "key" for the given command being
> overridden (e.g., the two maps  .put methods return non-null). 
> 
> Any suggestions on how to overcome this properly?
> 
> Best,
> Leo

[CZT-Devel] Old LaTeX printing problem

[Leo F. <leo...@gm...>]

Hi guys,

I am having the following problem:

a) a section FOO with fuzz_toolkit as a parent (e.g., the user spec)
b) mixed old and new latex within - all parse/typecheck
c) a section BAR with FOO as a parent (e.g., the VCs of FOO)

Now, trouble is I want BAR *NOT* to print \all or \exi for \forall,
but unfortunately it does print OLD latex. And even if I ask a
LatexCommand (rather than OldLatexCommand) directly, OLD
LaTeX is still print :-(

If one removes fuzz_toolkit, then all goes to "normal". So, whenever
any (transitive) parent does have fuzz_toolkit, the underlying markup 
directives get overridden.

In particular, the problem occurs / manifest itself here

net.sourceforge.czt.parser.util.LatexMarkupFunction.add(Directive)
and sometimes
net.sourceforge.czt.parser.util.LatexMarkupFunction.add(LatexMarkupFunction)

because the underlying maps already have a "key" for the given command being
overridden (e.g., the two maps  .put methods return non-null). 

Any suggestions on how to overcome this properly?

Best,
Leo