czt-devel — For programmers using the CZT code

[CZT-Devel] New CZT font for JEdit

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

Petra and Tim and others,

I've just completed a draft version of an open-source font for CZT,
to use within our Jedit CZT plugin, which will be released shortly.
It looks quite nice in JEdit at 14 points, and is just readable at 10 
points.
It is a scalable Truetype font, so looks even better at huge sizes, and 
it should print well!

I enclose a screenshot of Jedit, showing the plugin at the top using 
CZTSans14pt
and a nonsense Z spec at the bottom using CZTSans12pt.   The only nasty
thing is that the ENDZED character seems to be classified as a whitespace
character, so I cannot get Jedit to display the shape that I've designed.
But I've turned the "Show Other Whitespace" option of the "Whitespace"
plugin on, and at least that shows a little red diamond for the ENDZED chars
-- without the whitespace plugin, those chars are completely invisible!
I am pretty annoyed at the people who chose ZEDCHAR="Paragraph Separator"!

The font is derived from the open-source BitStream Vera Sans font, which
is a nice looking, professionally-hinted font, available from the Gnome
project with a licence that allows us to add characters and redistribute
the font under the original copyright, provided that we rename the
font (I've called it "CZT Sans").

I have added all the special characters in the Z standard, plus a few
extra variants of some of them (reverse arrows, implications etc.),
except for the two "extended" characters:  (Arithmos U001 D538
and the FiniteSet constructor U001 D546). 

I used the open-source 'fontforge' editor from fontforge.sourceforge.net,
which is pretty good, though quite easy to crash.  I cannot figure out how
to add these extended unicode characters in fontforge yet -- if I do,
I will add the above missing characters.

I have also added a few characters for Object-Z, and 1 for TCOZ:
(I just worked from what was used in parser/lib/oz_toolkit.tex and 
tcoz_toolkit.tex)

U+2225 is a parallel operator (two vertical bars)
U+22C0 is a large conjunction
U+22C1 is a large disjunction (Tim, you were using 2AFF for this.  Why?)
U+2193 is a downarrow, for precondition
U+2AFE is the Dijkstra non-det choice operator  (like [])
U+2AFF is a huge version of the non-det choice operator.
U+2AF4 is an operator with THREE vertical bars
    (Object-Z calls this "PostChar", while TCOZ uses it for "Interleave"
     -- can someone please sort this out and advise me if they should
         be the same or different, and what they should be?)
U+0392 is a funny looking B, for boolean.
     (TODO: we should use U+0001 U+D539 instead, it is exactly the B we 
want)
U+039F is a funny looking O, for ObjectIds.
     (TODO: we should use U+0001 U+D546 instead, it is exactly the O we 
want)

Comments and advice gratefully received!
Mark

Re: [CZT-Devel] Binary Releases

[Tim M. <T.M...@cs...>]

Hi all,

Just following up to Petra's message: there have been many changes 
and bugfixes made to the parser/typechecker since the November 10 
version, so if you find problems, it would probably be best to 
wait until the next binary version is released (or check out the 
CVS version and compile it if you are brave), and if that problem 
is still occurring, submit a bug report to us :-)

Thanks,
Tim

Petra Malik wrote:
> Hi all,
> 
> I just noticed that I forgot to announce that here:
> On my web-site
> http://www.cs.waikato.ac.nz/~petra/
> are CZT binary releases available.
> The first one is from November, 10, and we are planning
> to provide a new one very soon (hopefully next week).
> 
> We cannot distribute full binary releases on sourceforge
> since JAXB does not have an open source license and only
> open source software is allowed to be distributed via
> sourceforge (if I understand correctly).
> 
> Petra
> 
> 
> -------------------------------------------------------
> SF email is sponsored by - The IT Product Guide
> Read honest & candid reviews on hundreds of IT Products from real users.
> Discover which products truly live up to the hype. Start reading now. 
> http://productguide.itmanagersjournal.com/
> _______________________________________________
> CZT-Devel mailing list
> CZT...@li...
> https://lists.sourceforge.net/lists/listinfo/czt-devel

[CZT-Devel] Binary Releases

[Petra M. <pe...@cs...>]

Hi all,

I just noticed that I forgot to announce that here:
On my web-site
http://www.cs.waikato.ac.nz/~petra/
are CZT binary releases available.
The first one is from November, 10, and we are planning
to provide a new one very soon (hopefully next week).

We cannot distribute full binary releases on sourceforge
since JAXB does not have an open source license and only
open source software is allowed to be distributed via
sourceforge (if I understand correctly).

Petra

[CZT-Devel] CZT 0.2 (containing corejava 1.3.0) released

[Petra M. <pe...@cs...>]

Hi all,

CZT 0.2 has been released. Included is ZML 1.3, corejava 1.3.0,
and parser 0.2.  See the CZT web-site for more information.
Note that corejava 1.3.0 can now be downloaded within
the new czt release.

Cheers,
Petra

Re: [CZT-Devel] Re: Object Z questions

[Timothy M. <ti...@cs...>]

Hi Petra,

> Hmm, then the oz_toolkit should not use the Z toolkit at all.
> For instance, we cannot use \fun but this shouldn't be a problem.
>
This is no problem... we can remove this. Although, I do seem to 
remember polymorphism and containment being added to the XML schema as 
("primitive") expressions, so no definition will be necessary in the oz 
toolkit. I don't seem to have included these in the scanner and parser 
yet though. It shouldn't be too difficult.

> Are you proposing to remove the given paragraph introducing \bool in the 
> Object-Z toolkit as well?
> This means we just do not support Object-Z specifications using \bool. 
> What is so complex about \bool?
> 
Yes, we should either remove it, or declare it something like:
   TRUE == [| true]
   FALSE == [| false]
   \bool == \{ TRUE , FALSE \}

The literals 'true' and 'false' are predicates and not expressions. 
Using these as expressions more or less makes Object-Z higher-order, and 
introduces many complexities. Even in the corejava class, for example, 
we would need TrueExpr and FalseExpr. For now it is fine to use the 
above definition, but I believe the reason languages such as Z and B do 
not have a boolean type is also that there is a philosophy that they do 
not provide anything useful. In the case where one might use a boolean 
type, a free type with the members 'PASS' and 'FAIL', or 'VALID' and 
'INVALID' make the specification more self-documenting. So maybe having 
a boolean type is not useful at all?

Cheers,
Tim

[CZT-Devel] Re: Object Z questions

[Petra M. <pe...@cs...>]

Hi Tim,

thanks for your answer.

Tim Miller wrote:

> Due to there being no standard for Object-Z, we can be quite flexible.
>
> I think that the oz_toolkit should have only the prelude as a parent 
> (I know that the oz_toolkit I wrote for the parser included the 
> mathmatical  toolkit as a parent, but I hadn't given it much thought 
> until now), and that this oz_toolkit should be implicitly included in 
> all Object-Z specifications, like the prelude. Then, an anonymous spec 
> includes the mathematical toolkit as a parent, like a standard Z 
> specification.

Hmm, then the oz_toolkit should not use the Z toolkit at all.
For instance, we cannot use \fun but this shouldn't be a problem.

>> Then I noticed that the OZ toolkit in parser/lib/oz_toolkit.tex
>> doesn't contain any markup directives. I guess we need to add:
>>
>> %%Zchar \oid U+039F
>> %%Zchar \bool U+0392
>> %%Zprechar \poly U+2193
>> %%Zpostchar \copyright U+24B8
>>
>> Is that correct?
>> I am not sure which char (pre, post, etc.) to choose.
>>
> Yep, that's correct, except I suggest not to add \bool after all. This 
> way, Object-Z is simply standard Z with the extra type of paragraph (a 
> class). Having a boolean set/type adds a whole level of complexity.

Are you proposing to remove the given paragraph introducing \bool in the 
Object-Z toolkit as well?
This means we just do not support Object-Z specifications using \bool. 
What is so complex about \bool?

Regards,
Petra

[CZT-Devel] Object Z questions

[Petra M. <pe...@cs...>]

Hi Object Z guys,

I wonder how the Object Z parser is supposed to work.

Which parents does an anonymous Object Z specification have?
In Standard Z, an anonymous specifcation is semantically
equivalent to the specification with the mathmatical toolkit as
its parent. Is it the same for Object Z or is oz_toolkit its parent?

Then I noticed that the OZ toolkit in parser/lib/oz_toolkit.tex
doesn't contain any markup directives. I guess we need to add:

%%Zchar \oid U+039F
%%Zchar \bool U+0392
%%Zprechar \poly U+2193
%%Zpostchar \copyright U+24B8

Is that correct?
I am not sure which char (pre, post, etc.) to choose.

Thanks,
Petra

[CZT-Devel] Z standard now available

[Petra M. <pe...@cs...>]

Hi,

I just wanted to let you know that the ISO international standards for Z 
(ISO/IEC 13568:2002)
can now be downloaded at no cost:

http://isotc.iso.ch/livelink/livelink/fetch/2000/2489/Ittf_Home/PubliclyAvailableStandards.htm

Petra

[CZT-Devel] Scripts under Windows not working

[Petra M. <pe...@cs...>]

Hi all,

I just got a bug report that the scripts in bin are not working properly 
on Windows.
For instance, when 'ozed2zml -in birthdaybook.tex -out birthdaybook.xml' 
is called,
one gets:

Usage: java [-options] class [args...]
           (to execute a class)
   or  java [-options] -jar jarfile [args...]
           (to execute a jar file)

where options include:
    -client       to select the "client" VM
    -server       to select the "server" VM
    -hotspot      is a synonym for the "client" VM  [deprecated]
                  The default VM is client.

    -cp <class search path of directories and zip/jar files>
    -classpath <class search path of directories and zip/jar files>
                  A ; separated list of directories, JAR archives,
                  and ZIP archives to search for class files.
    -D<name>=<value>
                  set a system property
    -verbose[:class|gc|jni]
...



I tried it on a Windows XP and it was working fine, so I cannot reproduce
the problem. I guess it is a problem with the batch scripts under older 
windows versions.
I am not familiar with batch scripting at all ... can somebody help, 
i.e. reproduce the problem
or even fix it?

Thanks,
Petra

[CZT-Devel] Re: Request for some updates to the TCZO Schema

[Petra M. <pe...@cs...>]

Hi Chenchun,

thanks for your suggestions.

I have incorporated your additions into the TCOZ Schema
and also regenerated the classes in corejava.
You can find the new classes that reflect your changes
in the CVS repository in
corejava/src/net/sourceforge/czt/tcoz/{ast,impl,visitor}

Petra

[CZT-Devel] Request for some updates to the TCZO Schema

[<che...@co...>]

Dear all,

Currently I am trying to write a parser to analyze TCOZ specification from
Latex format to XML. I found that there are a few things that I"d like to
change to the XML schema (tcoz.xsd):

* Addition: a new operation expression InChoiceProExpr, substituting
OZ:OperationExpr
<xs:element name="InChoiceProExpr" type="OZ:TwoOpExpr"
substitutionGroup="OZ:OperationExpr">
   <xs:annotation>
        <xs:documentation>
         It appears in "Timed Communicating Object Z" by Brendan Mahony
and Jin Song Dong.
         It describes variation in behavior determined by the internal
state of the process.
         Syntax: OpExp \intchoice OpExp
        </xs:documentation>
   </xs:annotation>
</xs:element>

* Addition: a new operation expressioin DistInChoiceProExpr, substituting
OZ:OperationExpr
<xs:element name="DistInChoiceProExpr" type="OZ:DistOpExpr"
substitutionGroup="OZ:OperationExpr">
     <xs:annotation>
          <xs:documentation>
          It appears in "Timed Communicating Object Z" by Brendan Mahony
and Jin Song Dong.
          It is the intentional form of InChoiceProExpr when the range of
choice is large (possibly infinite)
          Syntax: \Intchoice SchemaText @ OpExp
          </xs:documentation>
      </xs:annotation>
</xs:element>

* Addition: a new operation expression DistInterleaveProExpr, substituting
OZ:OperationExpr
<xs:element name="DistInterleaveProExpr" type="OZ:DistOpExpr"
substitutionGroup="OZ:OperationExpr">
     <xs:annotation>
         <xs:documentation>
         It appears in "Timed Communicating Object Z" by Brendan Mahony
and Jin Song Dong.
         It is the intentional form of InterleaveProExpr  when the number
of asynchronous parallel components is large
        Syntax: ||| Schematext @ OpExp
        </xs:documentation>
    </xs:annotation>
</xs:element>

Please review these requests and any suggestions, comments are welcome!

Best regards
Chun Qing

[CZT-Devel] [Announce] Corejava API change List --> ListTerm

[Petra M. <pe...@cs...>]

Hi all,

since nobody did object, I am going to commit those changes
to the CVS repository now.

Petra


Petra Malik wrote:

> Hi all,
>
> Currently, some of the AST (getter) methods return a List.
> For instance, method getSect() in class Spec returns a list (of Sect).
> This makes it quite difficult to write generic visitors since the
> children of a term must be distinguished into Term and List.
> In case of a Term, the accept method of Term can be used;
> whereas for a list one has to iterate over all its elements
> (and visit them).
> In short, this design brakes the Composite Design Pattern.
>
> I am planning to introduce a new AST interface/class ListTerm,
> which is both a list and a term and can be used instead of List to
> fix this:
> interface ListTerm
>  extends net.sourceforge.czt.base.ast.Term, java.util.List
> {
> }
> All AST interfaces/classes containing a getter that returns List
> will be changed to return ListTerm instead. That is, method
> getSect() in class Spec will then return ListTerm.
> With this approach, all non-leaf AST classes will be terms and
> can be handled equally.
>
> Consequences:
> This will not affect code that simply uses the getter methods, since the
> return value is still a list, but visitors that visit an AST may break.
> For instance, if a visitor looks like this:
> class MyVisitor
>  implements TermVisitor
> {
>  public Object visitTerm(Term term)
>  {
>    Object[] childs = term.getChildren();
>    for (int i = 0; i < childs.length; i++) {
>      if (childs[i] instanceof Term) {
>        // do something
>      }
>      else if (childs[i] instanceof List) {
>        // do something else
>      }
>    }
>  }
> }
> it will break since the else-if-case will not be reached any more (the 
> list
> children are now terms as well).
>
> I think it is worth changing corejava as described above and correct
> the broken visitors (better now where there are not so many visitors than
> later when corejava is more widely used).
>
> Objections, better ideas, comments, etc?
>
> Petra

[CZT-Devel] [Proposal] Corejava API change List --> ListTerm

[Petra M. <pe...@cs...>]

Hi all,

Currently, some of the AST (getter) methods return a List.
For instance, method getSect() in class Spec returns a list (of Sect).
This makes it quite difficult to write generic visitors since the
children of a term must be distinguished into Term and List.
In case of a Term, the accept method of Term can be used;
whereas for a list one has to iterate over all its elements
(and visit them).
In short, this design brakes the Composite Design Pattern.

I am planning to introduce a new AST interface/class ListTerm,
which is both a list and a term and can be used instead of List to
fix this:
interface ListTerm
  extends net.sourceforge.czt.base.ast.Term, java.util.List
{
}
All AST interfaces/classes containing a getter that returns List
will be changed to return ListTerm instead. That is, method
getSect() in class Spec will then return ListTerm.
With this approach, all non-leaf AST classes will be terms and
can be handled equally.

Consequences:
This will not affect code that simply uses the getter methods, since the
return value is still a list, but visitors that visit an AST may break.
For instance, if a visitor looks like this:
class MyVisitor
  implements TermVisitor
{
  public Object visitTerm(Term term)
  {
    Object[] childs = term.getChildren();
    for (int i = 0; i < childs.length; i++) {
      if (childs[i] instanceof Term) {
        // do something
      }
      else if (childs[i] instanceof List) {
        // do something else
      }
    }
  }
}
it will break since the else-if-case will not be reached any more (the list
children are now terms as well).

I think it is worth changing corejava as described above and correct
the broken visitors (better now where there are not so many visitors than
later when corejava is more widely used).

Objections, better ideas, comments, etc?

Petra

[CZT-Devel] FASD project: Online survey launched

[<ben...@id...>]

Dear Open Source developer

I am doing a research project on "Fun and Software Development" in which I kindly invite you to participate.
You will find the online survey under http://fasd.ethz.ch/qsf/. The questionnaire consists of 53 questions and you will need about 15 minutes to complete it.

With the FASD project (Fun and Software Development) we want to define the motivational significance of fun when software developers decide to engage in Open Source projects. What is special about our research project is that a similar survey is planned with software developers in commercial firms. This procedure allows the immediate comparison between the involved individuals and the conditions of production of these two development models. Thus we hope to obtain substantial new insights to the phenomenon of Open Source Development.


With many thanks for your participation,
Benno Luthiger


PS:
The results of the survey will be published under http://www.isu.unizh.ch/fuehrung/blprojects/FASD/.
We have set up the mailing list fa...@we... for this study. Please see http://fasd.ethz.ch/qsf/mailinglist_en.html for registration to this mailing list.

_______________________________________________________________________

Benno Luthiger
Swiss Federal Institute of Technology Zurich
8092 Zurich

Mail: benno.luthiger(at)id.ethz.ch
_______________________________________________________________________

[CZT-Devel] Corejava and CZT release

[Petra M. <pe...@cs...>]

Hi all,

I am planning to do a new corejava (version 1.2.0) and the first czt 
release (containing corejava and the parser).
I suggest to give the czt release the version number 0.1.  Feel free to 
suggest a better number.

I provided first versions of these releases.  They are downloadable from
http://www.cs.waikato.ac.nz/~petra/czt_0_1_src.tar.gz
http://www.cs.waikato.ac.nz/~petra/corejava_1_2_0_src.tar.gz

It would be nice if some of you could check it and report problems, 
suggestions for improvements, etc.
If nobody objects and no major problems are reported  I am going to make 
the release tomorrow.

Petra

Re: [CZT-Devel] Re: [Fwd: Re: Bug in parser?]

[Tim M. <tim...@it...>]

Hi,

Yes, I think Petra is right - mixfix can be used to remove this ambiguity.

As Mark says, it would be a bit messy for visitors to figure this out, 
but perhaps for the simplicity of the mixfix approach, it is best to 
leave it as is? I'll update the parser to use mixfix, unless anyone has 
something else to add?

Regards,
Tim

Petra Malik wrote:
> Hi,
> 
> isn't is sufficient to use the Mixfix attribute for this as well?
> e1 = e2 ->  <MemPred Mixfix="true">...</MemPred>
> e1 \in {e2} -> <MemPred Mixfix="false">...</MemPred>
> 
> A MemPred is an equality iff Mixfix=="true" and the second (right) 
> expression is a SetExpr
> (usually the second argument is a relational operator).
> 
> Do I miss something? (perhaps it is too early to think about this ;-)
> 
> Petra
> 
> Mark wrote:
> 
>> Tim wrote:
>>
>>>> I think the way that the parser does it is correct. If you look at 
>>>> rule 12.2.10.3, it suggests that e1 = e2 is transformed to e1 \in 
>>>> {e2}, because they are equivalent predicates. Also, I've just 
>>>> realised that this could cause some problems when "unparsing" a 
>>>> tree... how do we know whether the original expression is e1 = e2 or 
>>>> e1 \in {e2}?? Maybe I should add an annotation to the any MemPreds 
>>>> that record it if it is an equals sign?
>>>>     
>>
>>
>> I think Tim is right.   (looking at 12.2.10.3)
>>
>> But he is also right that it is impossible to know how to
>> 'unparse' this back to an equality.
>>
>> Also, it seems a bit messy for visitors to figure out that
>> they are looking at an equality when they see  E1 \in {E2}
>>
>>
>> This makes me think that, instead of Mixfix (boolean), MemPred should 
>> have an attribute something like:
>>
>>    Kind = Infix | Member | Equals
>>
>> We need to think about this a bit more before doing anything...
>>  
>>
> 
> 
> 
> 
> -------------------------------------------------------
> This SF.Net email is sponsored by: IBM Linux Tutorials
> Free Linux tutorial presented by Daniel Robbins, President and CEO of
> GenToo technologies. Learn everything from fundamentals to system
> administration.http://ads.osdn.com/?ad_id=1470&alloc_id=3638&op=click
> _______________________________________________
> CZT-Devel mailing list
> CZT...@li...
> https://lists.sourceforge.net/lists/listinfo/czt-devel

[CZT-Devel] Re: [Fwd: Re: Bug in parser?]

[Petra M. <pe...@cs...>]

Hi,

isn't is sufficient to use the Mixfix attribute for this as well?
e1 = e2 ->  <MemPred Mixfix="true">...</MemPred>
e1 \in {e2} -> <MemPred Mixfix="false">...</MemPred>

A MemPred is an equality iff Mixfix=="true" and the second (right) 
expression is a SetExpr
(usually the second argument is a relational operator).

Do I miss something? (perhaps it is too early to think about this ;-)

Petra

Mark wrote:

> Tim wrote:
>
>>>I think the way that the parser does it is correct. If you look at rule 
>>>12.2.10.3, it suggests that e1 = e2 is transformed to e1 \in {e2}, 
>>>because they are equivalent predicates. Also, I've just realised that 
>>>this could cause some problems when "unparsing" a tree... how do we know 
>>>whether the original expression is e1 = e2 or e1 \in {e2}?? Maybe I 
>>>should add an annotation to the any MemPreds that record it if it is an 
>>>equals sign?
>>>      
>>>
>
>I think Tim is right.   (looking at 12.2.10.3)
>
>But he is also right that it is impossible to know how to
>'unparse' this back to an equality.
>
>Also, it seems a bit messy for visitors to figure out that
>they are looking at an equality when they see  E1 \in {E2}
>
>
>This makes me think that, instead of Mixfix (boolean), MemPred should 
>have an attribute something like:
>
>    Kind = Infix | Member | Equals
>
>We need to think about this a bit more before doing anything...
>  
>

[CZT-Devel] Re: [Fwd: Re: Bug in parser?]

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

Petra,

You wrote:
> I noticed that the parser transforms
> the line
>  known=\dom birthday
> to
>                           <MemPred Mixfix="true">
>                                <RefExpr Mixfix="false">
>                                    <RefName>
>                                        <Word>known</Word>
>                                    </RefName>
>                                </RefExpr>
>                                <SetExpr>
>                                    <ApplExpr Mixfix="false">
>                                        <RefExpr Mixfix="false">
>                                            <RefName>
>                                                <Word>dom</Word>
>                                            </RefName>
>                                        </RefExpr>
>                                        <RefExpr Mixfix="false">
>                                            <RefName>
>                                                <Word>birthday</Word>
>                                            </RefName>
>                                        </RefExpr>
>                                    </ApplExpr>
>                                </SetExpr>
>                            </MemPred>
> 
> I expect to see something like
>                           <MemPred Mixfix="true">
>                                <RefExpr Mixfix="false">
>                                    <RefName>
>                                        <Word>=</Word>
>                                    </RefName>
>                                </RefExpr>
>                                <TupleExpr> ... </TupleExpr>
>                            </MemPred>
> 
> I asked Tim whether this is a bug. His answer is attached.
> Who is right and why?

Tim replied:
>> I think the way that the parser does it is correct. If you look at rule 
>> 12.2.10.3, it suggests that e1 = e2 is transformed to e1 \in {e2}, 
>> because they are equivalent predicates. Also, I've just realised that 
>> this could cause some problems when "unparsing" a tree... how do we know 
>> whether the original expression is e1 = e2 or e1 \in {e2}?? Maybe I 
>> should add an annotation to the any MemPreds that record it if it is an 
>> equals sign?

I think Tim is right.   (looking at 12.2.10.3)

But he is also right that it is impossible to know how to
'unparse' this back to an equality.

Also, it seems a bit messy for visitors to figure out that
they are looking at an equality when they see  E1 \in {E2}


This makes me think that, instead of Mixfix (boolean), MemPred should 
have an attribute something like:

    Kind = Infix | Member | Equals

We need to think about this a bit more before doing anything...

Mark.

[CZT-Devel] [Announce] Changes to zml/Objeczt-Z.xsd

[Petra M. <pe...@cs...>]

I applied the changes proposed by Yuanfang
and commited them to the CVS repository.

Petra

Li Yuan Fang wrote:

>Dear all,
>
>Currently I'm trying to write some Object-Z examples based on the XML
>Schema. I found that there're a few things that I'd like to change:
>
>*. Addition: a new predicate PromotedInitPred, substituting Z:Pred:
>
><xs:element name="PromotedInitPred" type="OZ:PromotedInitPred"
>substitutionGroup="Z:Pred">
>    <xs:annotation>
>	<xs:documentation>This corresponds to 3.8.2 of "The
>Object-Z Specificaition Language" by Graeme Smith. It denotes that the
>predicates inside the Init state of a class is being promoted. Syntax:
>a.Init, where a is an expression evaluating to the identity of an
>object.</xs:documentation>
>    </xs:annotation>
></xs:element>
>
><xs:complexType name="PromotedInitPred">
>    <xs:complexContent>
>	<xs:extension base="Z:Pred">
> 	    <xs:sequence>
>		<xs:element ref="Z:Expr"/>
>	    </xs:sequence>
>	</xs:extension>
>    </xs:complexContent>
></xs:complexType>
>
>
>*. Addition: a new expression PromotedAttrExpr, substituting Z:Expr:
>
><xs:element name="PromotedAttrExpr" type="OZ:PromotedAttrExpr"
>substitutionGroup="Z:Expr">
>    <xs:annotation>
>	<xs:documentation>This corresponds to 3.9.5 of "The
>Object-Z Specificaition Language" by Graeme Smith. It denotes that an
>attribute in the visibility list of a class is being promoted. Syntax:
>Expression ::= Expression.Identifier</xs:documentation>
>    </xs:annotation>
></xs:element>
>
><xs:complexType name="PromotedAttrExpr">
>    <xs:complexContent>
>	<xs:extension base="Z:Expr1">
>  	    <xs:sequence>
>		<xs:element ref="Z:RefName"/>
>	    </xs:sequence>
>	</xs:extension>
>    </xs:complexContent>
></xs:complexType>
>
>
>*. Addition: a new expression SelfExpr, substituting Z:Expr,
>which is used in Object-Z to denote the object itself:
>
><xs:element name="SelfExpr" type="Z:Expr" substitutionGroup="Z:Expr"/>
>
>
>*. Addition: a new expression PolyExpr, substituting Z:Expr,
>which is used to denote the concept of polymorphism in Object-Z:
>
><xs:element name="PolyExpr" type="Z:Expr1" substitutionGroup="Z:Expr"/>
>
>
>*. Addition: a new expression ContainmentExpr, substituting Z:Expr,
>which is used to denote the concept of object containment:
>
><xs:element name="ContainmentExpr" type="Z:Expr1" substitutionGroup="Z:Expr"/>
>
>
>*. Modification: for the complexType State, I want to change
>
><xs:element ref="Z:Decl" maxOccurs="unbounded"/>
>to
><xs:element ref="Z:Decl" minOccurs="0" maxOccurs="unbounded"/>
>
>
>*. Modification: for the complex type InheritedClass
>
><xs:complexType name="InheritedClass">
>    <xs:complexContent>
>        <xs:extension base="Z:TermA">
>            <xs:sequence>
>                <xs:element name="Name" type="Z:RefName"/>
>                <xs:element ref="OZ:ActualParameters" minOccurs="0"/>
>                <xs:element ref="OZ:RenameList" minOccurs="0"/>
>            </xs:sequence>
>        </xs:extension>
>    </xs:complexContent>
></xs:complexType>
>
>The third element in the sequence was originally "<xs:element
>ref="Z:RenameExpr" minOccurs="0"/>", but I then found there's a
>syntactical mismatch: in OZ, renaming doesn't need an expression in the
>beginning. So now the OZ:RenameList just contains a list of
>Z:NameNamePair. The definitions are as follows.
>
>
>*. Addition: a new element RenameList:
>
><xs:element name="RenameList" type="OZ:RenameList"/>
>
><xs:complexType name="RenameList">
>    <xs:complexContent>
>        <xs:extension base="Z:TermA">
>            <xs:sequence>
>                <xs:element ref="Z:NameNamePair" maxOccurs="unbounded"/>
>            </xs:sequence>
>        </xs:extension>
>    </xs:complexContent>
></xs:complexType>
>
>
>Please review these requests and any suggestions, comments are welcome!
>
>Best regards
>Yuan Fang
>
>
>-------------------------------------------------------
>This SF.Net email is sponsored by: IBM Linux Tutorials
>Free Linux tutorial presented by Daniel Robbins, President and CEO of
>GenToo technologies. Learn everything from fundamentals to system
>administration.http://ads.osdn.com/?ad_id=1470&alloc_id=3638&op=click
>_______________________________________________
>CZT-Devel mailing list
>CZT...@li...
>https://lists.sourceforge.net/lists/listinfo/czt-devel
>  
>

Re: [CZT-Devel] Request for some updates to the Object-Z Schema

[Timothy M. <tim...@it...>]

Hi Yuan Fang (and other CZT'ers),

I think that the changes look great. Except, I wonder about these two:

> 
> *. Addition: a new expression PolyExpr, substituting Z:Expr,
> which is used to denote the concept of polymorphism in Object-Z:
> 
> <xs:element name="PolyExpr" type="Z:Expr1" substitutionGroup="Z:Expr"/>
> 
> 
> *. Addition: a new expression ContainmentExpr, substituting Z:Expr,
> which is used to denote the concept of object containment:
> 
> <xs:element name="ContainmentExpr" type="Z:Expr1" substitutionGroup="Z:Expr"/>
> 
> 

At the moment, the Object-Z parser that I have been working on with 
Petra parses an Object-Z toolkit that defines the polymorphic and 
containment symbols using prefix and postfix templates respectively. 
However, at the moment, the axiomatic definition of these types defines 
only their types. So, I am wondering whether these can be defined 
locally using an axiomatic definition (i.e. as opposed properties of the 
entire system).

Roger Duke and Gordon Rose's textbook (Section 10.3) discusses each 
object having an implicit secondary variable called 'contained', which 
is a set containing all objects that are contained by that object. This 
would imply that containment could be defined as a local property on an 
expression. The set of all object identities ("\oid" in latex), would be 
changed from a given set (as it is in my object-z toolkit), to a class 
definition with the secondary variable 'contained'. This would still 
have no semantics because the state invariant of each new class would 
have to identify which objects are contained in an instance of that 
class (I think!), but I believe it could be defined using a syntactic 
transformation rule. I hope that I'm making sense here! :)

As for the polymorphism operator, I have no ideas on how this could be 
specified. My understanding is if we define class A, and class B 
inherits A, then the object b : B, is not a member of A. It seems that 
any axiomatic definition would need to know all inheritance heirarchies 
within a system.

Does anyone else have ideas about how these could be defined if they 
were user-defined operators? If not, then I guess we should go with 
these new type of expressions as defined by Yuan Fang.

Tim

[CZT-Devel] Request for some updates to the Object-Z Schema

[Li Y. F. <li...@co...>]

Dear all,

Currently I'm trying to write some Object-Z examples based on the XML
Schema. I found that there're a few things that I'd like to change:

*. Addition: a new predicate PromotedInitPred, substituting Z:Pred:

<xs:element name="PromotedInitPred" type="OZ:PromotedInitPred"
substitutionGroup="Z:Pred">
    <xs:annotation>
	<xs:documentation>This corresponds to 3.8.2 of "The
Object-Z Specificaition Language" by Graeme Smith. It denotes that the
predicates inside the Init state of a class is being promoted. Syntax:
a.Init, where a is an expression evaluating to the identity of an
object.</xs:documentation>
    </xs:annotation>
</xs:element>

<xs:complexType name="PromotedInitPred">
    <xs:complexContent>
	<xs:extension base="Z:Pred">
 	    <xs:sequence>
		<xs:element ref="Z:Expr"/>
	    </xs:sequence>
	</xs:extension>
    </xs:complexContent>
</xs:complexType>


*. Addition: a new expression PromotedAttrExpr, substituting Z:Expr:

<xs:element name="PromotedAttrExpr" type="OZ:PromotedAttrExpr"
substitutionGroup="Z:Expr">
    <xs:annotation>
	<xs:documentation>This corresponds to 3.9.5 of "The
Object-Z Specificaition Language" by Graeme Smith. It denotes that an
attribute in the visibility list of a class is being promoted. Syntax:
Expression ::= Expression.Identifier</xs:documentation>
    </xs:annotation>
</xs:element>

<xs:complexType name="PromotedAttrExpr">
    <xs:complexContent>
	<xs:extension base="Z:Expr1">
  	    <xs:sequence>
		<xs:element ref="Z:RefName"/>
	    </xs:sequence>
	</xs:extension>
    </xs:complexContent>
</xs:complexType>


*. Addition: a new expression SelfExpr, substituting Z:Expr,
which is used in Object-Z to denote the object itself:

<xs:element name="SelfExpr" type="Z:Expr" substitutionGroup="Z:Expr"/>


*. Addition: a new expression PolyExpr, substituting Z:Expr,
which is used to denote the concept of polymorphism in Object-Z:

<xs:element name="PolyExpr" type="Z:Expr1" substitutionGroup="Z:Expr"/>


*. Addition: a new expression ContainmentExpr, substituting Z:Expr,
which is used to denote the concept of object containment:

<xs:element name="ContainmentExpr" type="Z:Expr1" substitutionGroup="Z:Expr"/>


*. Modification: for the complexType State, I want to change

<xs:element ref="Z:Decl" maxOccurs="unbounded"/>
to
<xs:element ref="Z:Decl" minOccurs="0" maxOccurs="unbounded"/>


*. Modification: for the complex type InheritedClass

<xs:complexType name="InheritedClass">
    <xs:complexContent>
        <xs:extension base="Z:TermA">
            <xs:sequence>
                <xs:element name="Name" type="Z:RefName"/>
                <xs:element ref="OZ:ActualParameters" minOccurs="0"/>
                <xs:element ref="OZ:RenameList" minOccurs="0"/>
            </xs:sequence>
        </xs:extension>
    </xs:complexContent>
</xs:complexType>

The third element in the sequence was originally "<xs:element
ref="Z:RenameExpr" minOccurs="0"/>", but I then found there's a
syntactical mismatch: in OZ, renaming doesn't need an expression in the
beginning. So now the OZ:RenameList just contains a list of
Z:NameNamePair. The definitions are as follows.


*. Addition: a new element RenameList:

<xs:element name="RenameList" type="OZ:RenameList"/>

<xs:complexType name="RenameList">
    <xs:complexContent>
        <xs:extension base="Z:TermA">
            <xs:sequence>
                <xs:element ref="Z:NameNamePair" maxOccurs="unbounded"/>
            </xs:sequence>
        </xs:extension>
    </xs:complexContent>
</xs:complexType>


Please review these requests and any suggestions, comments are welcome!

Best regards
Yuan Fang

[CZT-Devel] [Announce] Package change for ZChar and ZString

[Petra M. <pe...@cs...>]

Hi,

Petra Malik wrote:

> Hi all,
>
> I wonder whether the corejava classes
> net.sourceforge.czt.util.ZChar and
> net.sourcefofge.czt.util.ZString
> are in a good place.
>
> I think it would be better to put them in package
> net.sourceforge.czt.z.util (note the z between czt and util :-)
> This way, extensions like oz can put their unicode
> character extensions into
> net.sourceforge.czt.<extension name>.util
> and it is consistent with the classes for standard Z.

Since nobody did object I changed it.
ZChar and ZString are now in package net.sourceforge.czt.z.util
(in CVS).

Petra

Re: [CZT-Devel] [PROPOSAL] More modifications to zml/Objeczt-Z.xsd

[Petra M. <pe...@cs...>]

Hi,

here is another suggested change (from Yuanfang) for the Object Z Schema.

Add

<xs:element name="RenameList" type="OZ:RenameList"/>
<xs:complexType name="RenameList">
    <xs:complexContent>
	<xs:extension base="Z:TermA">
   	    <xs:sequence>
		<xs:element ref="Z:NameNamePair" maxOccurs="unbounded"/>
	    </xs:sequence>
	</xs:extension>
    </xs:complexContent>
</xs:complexType>

and modify InheritedClass to use this instead of RenameExpr:

<xs:complexType name="InheritedClass">
    <xs:complexContent>
	<xs:extension base="Z:TermA">
  	    <xs:sequence>
		<xs:element name="Name" type="Z:RefName"/>
		<xs:element ref="OZ:ActualParameters" minOccurs="0"/>
		<xs:element ref="OZ:RenameList" minOccurs="0"/>
	    </xs:sequence>
	</xs:extension>
    </xs:complexContent>
</xs:complexType>

since renaming doesn't need an expression.

Since I am not familiar with Object Z, can somebody who is familiar please
check whether this is a good thing to do. I am happy to apply this change
if nobody objects.

Petra

[CZT-Devel] [PROPOSAL] Modifications to zml/Objeczt-Z.xsd

[Petra M. <pe...@cs...>]

Hi all,

here is a proposal from Li Yuan Fang to extend the Object Z Schema.
He suggests to:
- add a new predicate PromotedInitPred
- add a new expression PromotedAttrExpr
- modify complexType State to contain _zero_ up to infinity Decl
   (instead of _one_ up to infinity).

Attached are the new Objeczt-Z Schema and the diff.

Petra

[CZT-Devel] [PROPOSAL] Package change for ZChar and ZString

[Petra M. <pe...@cs...>]

Hi all,

I wonder whether the corejava classes
net.sourceforge.czt.util.ZChar and
net.sourcefofge.czt.util.ZString
are in a good place.

I think it would be better to put them in package
net.sourceforge.czt.z.util (note the z between czt and util :-)
This way, extensions like oz can put their unicode
character extensions into
net.sourceforge.czt.<extension name>.util
and it is consistent with the classes for standard Z.

What do you think?

Petra