Today was chapter 15 of Using Z. This one was an extended example/case study involving the basic programming interface for a filesystem.
The example involved two basic object types (files and file systems) each with four operations defined on them. The global filesystem object was defined in terms of a promotion of the local file object.
To me, the most interesting part of this chapter was to see how the schemas were factored out. For instance, in addition to the expected operation schemas describing creating and deleting files, there were also schemas for error states, such as when the file does not exist. These described constratins and also generated output parameters. The final Create, Destroy, etc. schemas were defined using these extra output schema to make them total operations.
Other than that, I guess there's not a lot to say here. This chapter didn't introduce any new material, but it did give a nice example of putting this stuff into practice.
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.