FM Thesis

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.