[CZT-Devel] Additional Object-Z.xsd changes

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

Hi again,

Sorry to bother everyone with a second email, but I have made addition 
changes to the Object XML schema. The new changes are made to the 
operation expression hierarchy:

- Remove OperationBoxExpr. This seems unnecessary. It is used only as an 
abstract superclass of OperationBox and OperationExpr, which are unrelated.
- Renamed OperationBox to OpText. OpText has been changed to be more 
like a schema text (i.e. the text of an operation). So it is now made up 
of a delta list and a schema text.
- Removed MainOpExpr, and modified DistOpExpr to have SchText and Expr 
to be consistent with quantifier expressions in the Z XML schema.
- Renamed Operation* to Op* for internal consistency.
- BasicOpExpr is renamed to AnonOpExpr and now has an OpText, instead of 
a MainOpExpr.
- Replaced all List Pred with just Pred to be consistent with the Z XML 
schema.

These changes do have a small effect on the TCOZ schema, which I will 
also update, but they do not change the hierarchy at all.

Comments welcome. If nobody objects then I will commit these changes.

Cheers,
Tim

Tim Miller wrote:

 > Hi everyone,
 >
 > In fixing up the CZT Object-Z parser, I have noticed several items 
that needed addressing in Object-Z XML schema. Attached is a new version 
of the schema. There are several major changes, and any feedback would 
be welcome. The changes are:
 >
 > - Added a ClassUnionExpr for class unions.
 > - Added a ClassType.
 > - Removed PromotedAttrExpr. This is not needed/possible because it 
represents a dereference a.b, which cannot be distinguished from a 
schema binding selection in the parser, so we can treat them both a 
selection expressions.
 > - Removed SelfExpr. This is not really necessary - we can just treat 
a reference expr to the implicit state variable "self". This will 
simplify any tools that use these classes.
 > - Removed PromotedInitPred. As with self, we can treat "a.Init" as a 
selection expr.
 >
 > Then, I've also changed the following to be consistent with similar 
constructs in Z.xsd:
 > In InheritedClass
 > - Replaced ActualParameters with List Expr.
 > - Replaced RenameList with List NameNamePair.
 >
 > In ClassPara
 > - Replaced SecondaryAttributes with List Decl
 > - Replaced FormalParameters with List DeclName
 > - Replaced LocalDef with List Para
 > - Replaced RefNameList with List RefName
 >
 > Any comments/objections?
 >
 > Cheers,
 > Tim