A relational basis for program construction by parts.
Program construction by parts consists of tackling a complex specification one component at a time, developing a partially defined solution for each component, then combining the partial solutions into a global solution for the aggregate specification. This method is desirable whenever the specifica...
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | Others |
| Published: |
University of Ottawa (Canada)
2009
|
| Subjects: | |
| Online Access: | http://hdl.handle.net/10393/9728 http://dx.doi.org/10.20381/ruor-16472 |
| Summary: | Program construction by parts consists of tackling a complex specification one component at a time, developing a partially defined solution for each component, then combining the partial solutions into a global solution for the aggregate specification. This method is desirable whenever the specification at hand is too complex to be grasped in all its detail. It is feasible whenever the specification at hand is structured as an aggregate of clearly defined subspecifications--where each subspecification represents a simple functional requirement. Our approach is based on relational specifications, whereby a specification is described by a binary relation. The set of relational specifications is naturally ordered by the refinement ordering, which provides a lattice-like structure. The join of two specifications S and $S\sp\prime$ is the specification that carries all the functional features of S and all the functional features of $S\sp\prime$. Complex specifications are naturally structured as the join of simpler subspecifications. On this basis, we have defined a language where specifications and programs can be represented. This language can represent specifications and programs can be represented. This language can represent specifications (structured as joins), programs (structured by means of traditional Pascal-like control structures) and intermediate designs (by means of a mixture of specification constructs and program constructs). Also, we have provided a set of rules for transforming a specification into a program, by changing a representation in this language from a specification structuring into a program structuring. The transformations we propose are correctness preserving in the sense that they map one representation into a more refined representation. |
|---|