FM Thesis

On Thursday and Friday, I read through a 1997 paper comparing Z and VDM. This is kind of an interesting thing to do because they are probably the two most widely used and recognized formal methods. I don't know much about VDM, but apparently the underlying principles of it are not all that terribly different from Z. In addition to the general discussion, the author compared tool support for the two methods (which seems somewhat limited in both cases) and tried to compare the results seen in projects using them. However, he only chose to compare CICS and CDIS, i.e. just two data points, which is not especially useful.

Yesterday and today (I didn't accomplish anything on Saturday), I just spent a little time trying to outline a concrete plan to procede from here. By now I have a pretty good idea of what material I have, so now I'm trying to figure out what I need to get in terms of research and what I can do with what I already have. In particular, I need to start picking out some case studies and analyzing the results. However, first I want to find some more commercially-oriented cases to look at. The international survey had a few, but pretty much everything else is a safety- or security-critical project.

So I'm going to spend the next couple of days trying to plan a direction for the remainder of my research and, hopefully, hunting for some sources. That should allow me to be a little more productive from here on out. It will also give me a nice break from the constant reading. I swear, I can only read so many journal articles before my brain starts to turn to mush. I've really been running out of steam on that front the past couple of weeks.

I read and took notes on two papers today. The first was Kate Finney and Norman Fenton's 1996 paper Evaluating the Effectiveness of Z: Claims Made About CICS and Where to Go From Here. It basically critiques the claims made about the benefits IBM saw from using Z in the respecificatino or parts of CICS. The more impressive claims were that the parts of the system which used Z saw 2.5 times fewer defects and that the overall project cost was reduced by 9%. Because of this, CICS is (or, at least, was) often viewed as the poster-project for formal methods success.

Basically, the paper points out that this optimism is unfounded. There is (or was - I've not seen any follow-up studies) insufficient evidence to evaluate these claims. Basically, this is because CICS was not a proper experiment. The literature is unclear on what was being compared to what and how valid those comparisons were. For example, the 9% cost saving figure seems to appear pretty much out of thin air, with no indication how it was calculated. So while CICS seems to be a success story, it should be viewed with caution.

The second paper is a 2002 article by Carol Smidts, Xin Huang, and James C. Widmaier entitled Producing Reliable Software: An Experiment. This one is interesting because it involves having two different teams independently develop the same system using different methods. There was a formal methods team that used Haskell and Specware and a conventional team the using Carnegie Melon SEI Capability Maturity Model (CMM) level 4. They were each separately contracted to build a card access system from the same specification. The contract specified reliability levels and required process documentation, design documents, and test plans. The reliability of the actual software was tested by a third party using automated test suites.

The results of both teams were pretty dismal. Neither one got close to the target 0.99 reliability for "level 1," i.e. critical, defects, with the formal team getting 0.77 and the CMM team 0.56. Furthermore, the formal methods team failed to produce much of anything in the way of documentation. A disappointing showing all around.

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.

Today was chapter 14, on preconditions. Basically, this covered methods for calculating preconditions of schemas, in order to do things lik establish basic consistency.

The first section described the initialization theorem. Basically, this just says that if you can establish that there exists a state satisfying the initialization schema, then the schema requirements must be consistent. This seems fairly obvious.

After that, it got into calculating preconditions. To be honest, this is where my eyes started to glaze over. Let's face it: the mechanics of doing logic just isn't that interesting. Even the author left out large sections of proof at various points. I pretty much just plowed through this and literally tried my best to stay awake.

So section two discussed various general concerns related to preconditions (e.g. conceptual stuff, like remembering to factor out the things in the declarations). It also introduced the pre precondition operator for schemas.

Section three got seriosly into the mechanics of calculating and simplifying preconditions. It also included a basic algorithm/method for calculating the precondition of a schema.

Section four discussed the structure of operations and the effect on preconditions. For instance, it discussed distributivity of the precondition operator (it distributes over disjunction, but not conjunction).It also including some stuff on free promotion. The punchline seems to be that the precondition of a global operation under a free promotion is equivalent to the conjunction of the preconditions of the local operation and promotion schema. Not that I fully grasp promotions yet, but I'm sure that will make sense later.

Today I finally finished reading chapter 13 of Using Z. I've been looking at this for days, and I'm still not sure I get it. I'll probably have to come back to it later.

This chapter covers schema factorization and promotion. It seems that this relates to how you can model indexed collections of things. The examples include things like arrays and the player scores in Trivial Pursuit. The basic idea seems to be that, given the right conditions, you can describe the global state in terms of local states. So, instead of having a schema to describe the global state, you can factor this out as a schema describing the local state and a promotion schema, which basically determines how changes in the local state affect the global state.

What I don't get is why you would want to define things in terms of promotion schemas and how to you would go about constructing them. Maybe I've just put up a mental block, but it kind of seems like this method is overly complicated. The concept seems reasonable enough, but the examples just seem to make things more difficult than they need to be. Perhaps promotion suffers from the same problem as teaching object-orientation - all the good examples are too comlicated for beginners and all the examples beginners can handle are incredibly stupid applications of the concept.

It doesn't help that I'm starting to drown in the notation in this chapter. I think I'm going to have to go back over the last few chapters again soon. For instance, I keep wondering where the thetas are coming from. Of course, the theta operator indicates a characteristic binding, which was never really defined with any clarity. The book pretty much just said it's a binding that characterizes a schema by binding, e.g. element a to a, b to b, and so on. What, exactly, that means and why I should care is still an open question.

That's enough for now. It's late, I'm tired, and I just don't care anymore. Plus I'm pissed off because VMware's network bridging module has been causing kernel panics every time I try to use it.

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.

Well, it's been a couple of days, but there's not an awful lot to say, so this will be short. It's also late, so I don't feel like going into great detail.

On Tuesday, I read chapter 10 of Using Z. That was the chapter on free types. Basically, it introduced how to define an arbitrary type, such as enumerated types. It also showed how to use free types to model a binary tree, which was kind of interesting.

Basically, there are a couple of ways to define a free type. One is by explicitly enumerating the possible values, like this:
Colors::= red|gree|blue
Another is with a constructor function. The general case of the constructor looks like this:
FreeType::= constant|constructor <<source>>
This is convenient for recursive definitions, as you can have a constant as your base case and reference the free type in the constructor. The simplest example was defining the natural numbers as follows:
nat::= zero | succ <<nat>>
Another interesting example was the following definition of a binary tree:
Tree::= leaf <<N>> | branch <<Tree x Tree>>
This defines a tree as either a numbered leaf node or an ordered pair of trees.

In addition to the expected sections on induction and primitive recursion that this chapter included, there was also a breif section on consistency. Free types makes it possible to introduce contradictions into our math. The example given was the definition:
T::= d <<&weierp; T>>
The problem here is that power sets are not finitary, whatever that means. The text leaves the term undefined, except to say that we basically need to stick to finite constructs to maintain consistency. Apparently the idea is that non-finitary (or is it infinitary?) constructs generate too many values, so we would end up with a set T that must be bigger than itself.

Anyway, yesterday and today I spent in reviewing the past five chapters of Using Z. Basically just looking over the key points and taking some notes. The symbols were all starting to run together, so I figured it would help make them stick in my memory if I wrote them down.

Today I read the sequences chapter of Using Z. I'd not been exposed to sequences before, so this was relatively new to me. Intuitively, a sequence is an ordered series of items that allows repetition, such as <a, b, b, c, a>. It turns out that sequences can also be viewed as functions from the natural numbers to some set of objects. Needless to say, this simplifies things from a conceptual standpoint, as it allows the reuse of a lot of mathematical language.

The chapter covered basics such as the definition of a sequence, operations such as concatenation and filtering, as well as functions for the head and tail of the sequence, reversing, etc.

This chapter also went into structural induction to prove properties of sequences. This was initially confusing to me, as they didn't give the usual symbolic statement of the proof rule for structural induction. They also define axioms for the equivalence of the predicate to be proved and construct the proof using those. It took me a couple of proofs to realize that the defined axiom was how they were getting form "P s" to some complex predicate.

Lastly, they introduced the idea of bags, which are basically sequences without order. Bags can be represented as a function from a set of objects to the natural number, where the number in the range represents the number of times the item is in the bag. This section also introduced bag-equivalents of set membership and subset, as well bag union and difference operators. The latter simply involve adding or subtracting the number of elements for each bag involved to get the resulting bag. The only odd thing I found was that the difference operator is a union cup with a minus sign in it, whereas I'd have thought an intersection cap would have been more appropriate. Oh well....

Slow weekend for research. I spent all weekend visiting my in-laws, so the only thing I managed to get done was to finish chapter 8 of Using Z. That was the one on functions.

Maybe I'm just getting rusty, but this chapter was a little confusing. It covered lambda notation (which I think I get), functions on relations (which I also think I get, though the examples were a little confusing), function overriding (which seems pretty basic), properties of functions, and finite sets. It got really confusing in the properties of functions chapter when they introduced different styles of arrows to denote different types of functions. So injective functions got one style of arrow, surjective another, and bijective yet another. Plus there was a vertical line through the arrow to denote partial functions and, later, a double line to indicate the set of all finite functions on two sets. I think I'm going to have to go back and make myself a cheat-sheet of all the symbols I've seen in the past few chapters.

So yesterday I polished off chapters 4 and 5 of Using Z and I finished chapter 6 tonight. With any luck, I'll get a good start on chapter 7 before bed. It's a much faster read than I would have expected, but that might just be because I haven't gotten into the really heavy stuff yet.

Chapter four discussed rules for equality of expressions and introduced the "one-point" rule for reasoning with existential quantifiers. It also included some interesting examples of predicates describing uniquness with quantifiers and introduced the mu notation for definite description. That was something I had not seen before. The notation is (&mu; x: a | p), which denotes the unique object x in set a which satisfies predicate p.

Chapter five was an overview of basic set theory, including things like the inference rules regarding set conprehension. It also included basics such as definitions of the union, intersection, and difference operations, and all that good stuff. It also included a brief definition of types in Z. It turns out that Z types are maximal sets, often defined in terms of power sets or Cartesian products.

Chapter six was an introduction to defining things in Z. This includes defining types, declaring objects, and introducing axioms. The basic syntax is fairly straight forward so far. The only problem I had was trying to figure out the relevance of power sets of power sets.

To take the example from page 82, the predicate "is a crowd" was formalized as:
crowds: P(P Person)
crowds = {s: P Person | #s >= 3}
This indicates that crowds is an element of the power set of the power set of all people and that crowds is the set of all members of the power set of people with three or more members. After thinking about this for a few minutes, it started to become clear what that means. The set of all crowds is a set of sets, so its elements obviously have to belong to the power set of all people. But since a type is a maximal set, what is the type of crowds? Obviously it must be P(P Person), since crowds must be an element of that. And since crowds contains elements of P Person, we end up with each element of crowds being a set of individual people.

It all makes perfect sense, really. It's just a different type and level of abstraction than I'm used to using. I just needed to stop for a few minutes and wrap my brain around.

Another slow couple of days. Yesterday and today I just spent a little time reading the next to chapters of Using Z. Nothing interesting in these; just propositional and predicate logic review. The next two chapters are also mathematical background. It looks like I'll start getting into the meat of Z around chapter six.