1. The design rule is easier to verify (manually or automatically) than the interesting property.
2. The fact that the desing-rule property holds boosts the developer's confidence that the interesting property holds.
3. Adherence to the design rule makes the code easier to read and understand (because it makes the interesting property more obvious and easier to verify).

• All files that are opened are eventually closed.

The behavioral property itself is potentially very hard to verify. This is because there all kinds of ways in which files can be opened and eventually closed. Without knowing the intended design structure a developer has in mind to ensure that a particular file is effectively guaranteed to be closed, it is unclear how to limit the scope of an analysis to verify the property.

However, the property becomes easier to verify if the following design rule is followed:

• All files that are opened are always eventually closed.

• Files that are opened by a method should be closed before exiting the method.

Design Rules

What are Design Rules

Note: This is an attempt to provide a definition / vision on what we mean by "design rule". This is not the be all and end all.

A Design Rule is a (relatively) easily verifiable rule that constrains how code is to be structured. By adhering to a design rule developers trade away some flexibility on how they write and structure code in order to make it easier to manually or automatically verify important properties of their software.

A design rule is not the same as the actual property one is seaking to guarantee (let's call this the interesting property) but can actually be a weaker or stronger property than the interesting property. The property specified by the design rule is a structural property of their code which developer chose to adopt because it:

1. Is easier to verify (manually or automatically) than the interesting property.
2. The fact that the desing-rule property holds boosts the developer's confidence in that the interesting property holds.
3. It makes the code easier to read and understand (because it makes the interesting property more obvious and easier to verify).

For example, let's us considering the opening and closing of files. An interesting property we may wish to ensure ourselves of as developers is that

• All files are opened before they are always closed eventually.

This property is potentially very hard to verify. However, it becomes much easier to verify it if adopt the following design rule:

• Files that are opened by a method should closed within the same method.

By adopting this desing rule the developer agrees to always open and close file in manner similar to the following idiom:

     void operateOnFile(String filename) {
        ... open file ...
        ... operate on the file ...
        ... close the file ...
     }

Note that this design rule may be overly restrictive for some situations. In such cases, the desing rule may need to be extended to allow for certain exceptions. For these more complex cases may then chose to adopt a different design rule as an alternative.

Design Rule Catalog

• ExecuteAfterPut
• LazyInitialization

-- Main.kdvolder - 05 May 2005