The logic of propagation in the inscape environment

ABSTRACT

The Inscape Environment research project addresses issues in supporting the development of large systems by large numbers of programmers. One aspect of this research is the “constructive use” of formal module interface specifications - that is, given that you have formal specifications, what can you do with them. In Inscape, the specifications form the basis for providing an environment that is knowledgeable about the process of developing and evolving software systems, an environment that works in symbiosis with the programmer to develop and evolve a software system. In this discussion, I present how Inscape uses operation specifications (based on Hoare's input/output predicate approach) as the basis for synthesizing the interfaces for such complex languages statements as sequence, selection and iteration. In each of these statements, the synthesized interface is a function of the component interfaces. I first present the basic rules for interface specification use and the logical framework for interface propagation and error detection. I then define the rules for propagating the interfaces for sequence, selection, iteration and operation. Finally, I define notions of “implementation completeness and correctness”.

REFERENCES

• 1: Dewayne E. Perry, The inscape environment, Proceedings of the 11th international conference on Software engineering, p.2-11, May 1989, Pittsburgh, Pennsylvania, United States [doi>10.1145/74587.74588]
• 2: D. E. Perry , G. E. Kaiser, Models of software development environments, Proceedings of the 10th international conference on Software engineering, p.60-68, April 11-15, 1988, Singapore
• 3: Dewayne E. Perry. "Industrial Strength Software Development Environments", Proceedings of the IFIPS '89 World Computer Conference San Francisco CA, August, 1989.
• 4: Frederick P. Brooks, Jr., No silver bullet: essence and accidents of software engineering, Computer, v.20 n.4, p.10-19, April 1987 [doi>10.1109/MC.1987.1663532]
• 5: D. E. Perry, Software interconnection models, Proceedings of the 9th international conference on Software Engineering, p.61-69, March 1987, Monterey, California, United States
• 6: C. A. R. Hoare, An axiomatic basis for computer programming, Communications of the ACM, v.12 n.10, p.576-580, Oct. 1969 [doi>10.1145/363235.363259]
• 7: C. A. R. Hoare, Programs are predicates, Proc. of a discussion meeting of the Royal Society of London on Mathematical logic and programming languages, p.141-155, June 1985, London, United Kingdom
• 8: John B. Goodenough, Exception handling: issues and a proposed notation, Communications of the ACM, v.18 n.12, p.683-696, Dec. 1975 [doi>10.1145/361227.361230]
• 9: David Luckham and Friedrich W. von Henke. "An Overview of Anna. A Specification Language for Ada." IEEE Software, 2:2 (March 1985). pp 24-33.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.2 Design Tools and Techniques
          Subjects: Modules and interfaces

  K. Computing Milieux
  K.6 MANAGEMENT OF COMPUTING AND INFORMATION SYSTEMS
      K.6.3 Software Management
          Subjects: Software development

General Terms:
Management, Verification