Maximality Properties

Traditionally, a program specification is given by safety and progress properties, as explained in chapters 5 and 6. A safety property —e.g., no two neighbors eat simultaneously in a dining philosophers solution— is used to exclude certain undesirable execution sequences. A specification with safety properties alone can be implemented by a program that does nothing; that is, the safety constraints are implemented by excluding all nontrivial executions. Therefore, it is necessary to specify progress properties —e.g., some hungry philosopher eats eventually— which guarantee that some execution sequence will be included. Safety and progress requirements are sufficient for specifying nontrivial sequential programming tasks, but they are not sufficient for concurrent program design because, for instance, the dining philosophers solution may allow only one philosopher to eat at a time, thus eliminating all concurrency. We propose a new class of properties, called maximality, to permit inclusion of all executions that satisfy a specification. Thus, the sequential solution to the dining philosophers problem can be excluded by requiring that the solution be maximal for the appropriate specification.