Wow, a whole week since my last post. I'll have to try not to repeat that again. However, there were extenuating circumstances: I felt really crumby for the past week. I came down with a nasty cold on Friday and couldn't really concentrate on anything up until this morning. As a result of this, I only read two and a half chapters of Using Z this week, and I'm not at all confident that I understood them. I'll probably have to go back over them later (but I was most likely going to do that anyway).
Chapter eleven was on schemas. As I understand it, schemas are basically Z's equivalent of abstract data types. They consist of a declaration section and a predicate section. The declaration just introduces the variables used in the schema, while the predicate section is a set of predicates involving these variables that every object in the schema must, by definition, satisfy.
Just to complicate things, schemas can also be used as types, declarations, and predicates. The type part seems obvious enough. For declarations, using a schema introduces the variables in the declaration and puts them under the appropriate constraint. As predicates, a schema defines constraints on the variables, provided they have already been introduced.
One note of interest is schema normalization. Basically, this just means putting all the constraint information in the schema in the predicate part. For example, if two schemas are the same, except that one declares a variable as being in the natural nubmers, while the other declares it as being in the integers, we would change the first schema to have that variable in Z and add a constraint to the predicate section that it is an element of N. The same sort of thing can happen with functions and relations.
Last, but not least, it is possible to have generic schemas that are parameterized by a type. However, that's about all I know about them at this point.
Chapter 12 was on schema operators: conjunction, disjunction, negation, composition, as well as sections on quantification and decorators. It introduced the notation for schema states and state changes (using the familiar ΔState), plus the conventional ? and ! decorators for input and result variables.
Chapter 13 is on promotion. I'm only part way through that one, and I didn't really grok it while I was reading it, so I'll leave that to tomorrow. Right now, it's late and I'm tired, so it's bed time.
You can reply to this entry by leaving a comment below. You can send TrackBack pings to this URL. This entry accepts Pingbacks from other blogs. You can follow comments on this entry by subscribing to the RSS feed.