Skip to main content
SpringerLink
Log in
Book cover

System Development and Ada pp 173–194Cite as

Integration of program construction and verification: the PROSPECTRA methodology

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 275))

Abstract

The PROSPECTRA project aims to provide a rigorous methodology for developing correct Ada software and a comprehensive support system. It is a cooperative project between Universität Bremen, Universität Dortmund, Universität Passau, Universität des Saarlandes (all D), University of Strathclyde (GB), SYSECA Logiciel (F), Dansk Datamatik Center (DK), and Standard Electrica S.A. (E), and is sponsored by the Commission of the European Communities under the ESPRIT Programme, ref. #390 (see [1]).

The methodology integrates program construction and verification during the development process. User and implementor start with a formal specification, the interface or "contract". This initial specification is then gradually transformed into an optimised machine-oriented executable program. The final version is obtained by stepwise application of transformation rules. These are carried out by the system, with interactive guidance by the implementor, or automatically by compact transformation tools. Transformation rules form the nucleus of an extendible knowledge base.

The strict methodology of Program Development by Transformation (based on the CIP approach, see e.g. [2, 3]) is completely supported by the system. Any kind of activity is conceptually and technically regarded as a transformation of a "program" at one of the system layers. This provides for a uniform user interface, reduces system complexity, and allows the construction of system components in a highly generative way.

A methodology for PROgram development by SPECification and TRAnsformation is described. Formal requirement specifications in Anna are the basis for constructing correct and efficient Ada programs by gradual transformation.

This is a preview of subscription content, log in via an institution.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Krieg-Brückner, B., Hoffmann, B., Ganzinger, H., Broy, M., Wilhelm, R., Möncke, U., Weisgerber, B., McGettrick, A.D., Campbell, I.G., Winterstein, G.: PROgram Development by SPECification and TRAnsformation. in: CEC, Directorate General XIII (eds.): ESPRIT '86: Results and Achievements. Elsevier Sci. Publ. (North-Holland) (1987) 301–311

    Google Scholar 

  2. Bauer, F.L.: Program Development by Stepwise Transformations — The Project CIP. in: Bauer, F. L., Broy, M. (eds.): Program Construction. LNCS 69, Springer 1979.

    Google Scholar 

  3. Bauer, F.L., Berghammer, R., Broy, M., Dosch, W., Gnatz, R., Geiselbrechtinger, F., Hangel, E., Hesse, W., Krieg.-Brückner, B., Laut, A., Matzner, T.A., Möller, B., Nickl, F., Partsch, H., Pepper, P., Samelson, K., Wirsing, M., Wössner, H.: The Munich Project CIP, Vol. 1: The Wide Spectrum Language CIP-L. LNCS 183, Springer 1985.

    Google Scholar 

  4. Partsch, H., Steinbrüggen, R.: Program Transformation Systems. ACM Computing Surveys 15 (1983) 199–236.

    Article  Google Scholar 

  5. Reference Manual for the Ada Programming Language. ANSI/MIL.STD 1815A. US Government Printing Office, 1983. Also in: Rogers, M. W. (ed.): Ada: Language, Compilers and Bibliography. Ada Companion Series, Cambridge University Press, 1984.

    Google Scholar 

  6. Luckham, D.C., von Henke, F.W., Krieg-Brückner, B., Owe, O.: Anna, a Language for Annotating Ada Programs, Preliminary Reference Manual. Technical Report No. 84–248, Computer Systems Laboratory, Stanford University, June 1984; also: LNCS, Springer (to appear).

    Google Scholar 

  7. Krieg-Brückner, B.: Informal Specification of the PROSPECTRA System. PROSPECTRA Study Note M.1.1.S1-SN-9.1, Universität Bremen, 1986.

    Google Scholar 

  8. Bertling, H., Ganzinger, H.: A Structure Editor Based on Term Rewriting. in: Proc. 2nd ESPRIT Technical Week, Brussels (1985) 455–466.

    Google Scholar 

  9. Bertling, H., Ganzinger, H.: Paraphrasing in the PROSPECTRA System. PROSPECTRA Report M.1.4-R-1.0, Universität Dortmund, 1986.

    Google Scholar 

  10. Heckmann, R.: An Efficient ELL(1) Parser Generator. Acta Informatica 23 (1986) 127–148.

    Article  MathSciNet  Google Scholar 

  11. Möncke, U., Weisgerber, B., Wilhelm, R.: Generative Support for Transformational Programming. in: Proc. 2nd ESPRIT Technical Week, Brussels (1985) 511–528.

    Google Scholar 

  12. Möncke, U., Pistorius, S., Weisgerber, B.: OPTRAN under UNIX. PROSPECTRA Report S.1.6-R-3.0, Universität des Saarlandes, 1986.

    Google Scholar 

  13. Heckmann, R.: A Proposal for the Sytactic Part of the PROSPECTRA Transformation Language. PROSPECTRA Study Note S.1.6-SN-6.0, Universität des Saarlandes, 1987.

    Google Scholar 

  14. Owe. O.: An Approach to Program Reasoning Based on a First Order Logic for Partial Functions. Research Report No. 89, Institute of Informatics, University of Oslo, 1985.

    Google Scholar 

  15. Krieg-Brückner, B.: Transformation of interface Specifications. in: Kreowski, H.-J. (ed.): Recent Trends in Data Type Specification. Informatik Fachberichte 116, Springer 1985, 156–170.

    Google Scholar 

  16. Krieg-Brückner, B.: Systematic Transformation of Interface Specifications: Applicative to Imperative Style, Exceptions. in: Partsch, P. (ed.): Program Specification and Transformation, Proc. IFIP TC2 Working Conf. (Tölz). Elsevier Sci. Publ. (North-Holland) (to appear).

    Google Scholar 

  17. Bauer, F.L., Wössner, H.: Algorithmic Language and Program Development. Springer 1982.

    Google Scholar 

  18. Pepper, P.: A Study of Transformational Semantics. in: Bauer, F.L., Broy, M (eds.): Program Construction. LNCS 69, Springer (1979) 322–405.

    Google Scholar 

  19. Treff, L.: The Static Semantic Analysis of PAnndA-S; Vol. 1: Rationale, Vol. 2: Attribute Grammar. PROSPECTRA Report S.3.1-R-4.0, Karlsruhe: SYSTEAM KG, 1986.

    Google Scholar 

  20. Broy, M., Nickl, F.: PAnndA-S Semantics. PROSPECTRA Study Note M.2.1.A1-SN-2.1, Universität Passau, 1986.

    Google Scholar 

  21. Krieg-Brückner, B.: PAnndA-S, its Canonical Syntax and Alternative Paraphrasings. PROSPECTRA Study Note M.1.1.S1-SN-7.2, Universität Bremen, 1986.

    Google Scholar 

  22. Kahrs, S.: PAnndA-S Standard Types. PROSPECTRA Study Note M.1.1.S1-SN-11.2, Universität Bremen, 1986.

    Google Scholar 

  23. Broy, M.: Program Construction by Transformations: A Family Tree of Sorting Programs. in: Biermann, A. W. et al. (eds.): Computer Program Synthesis Methodologies. Proc. NATO Advanced Study Institute, Bonas 1981. NATO Advanced Study Series 95, Dordrecht: Reidel (1983) 1–49.

    Google Scholar 

  24. Partsch, H.: An Exercise in the Transformational Derivation of an Efficient Program by Joint Development of Control and Data Structure. Science of Computer Programming 3, 1983, 1–35.

    Article  Google Scholar 

  25. Partsch, H.: Structuring Transformational Developments: a Case Study Based on Early's Recogniser. Science of Computer Programming 4 (1984) 17–44.

    Article  Google Scholar 

  26. Broy, M., Krieg-Brückner, B.: Derivation of Invariant Assertions During Program Development by Transformation. ACM TOPLAS 2:3 (1980) 321–337.

    Article  Google Scholar 

  27. Kahrs, S.: From Constructive Specifications to Algorithmic Specifications. PROSPECTRA Study Note M.3.1.S1-SN-1.2, Universität Bremen, 1986.

    Google Scholar 

  28. Ganzinger, H.: Ground Term Confluence in Parametric Conditional Equational Specifications. in: Brandenburg, F.J., Vidal-Naquet, G., Wirsing, M.(eds.): Proc. 4th Annual Symp. on Theoretical Aspects of Comp. Sci., Passau '87. LNCS 247 (1987) 286–298.

    Google Scholar 

  29. Broy, M., Möller, B., Pepper, P., Wirsing, M.: Algebraic Implementations Preserve Program Correctness. Science of Computer Programming 7 (1986) 35–53.

    Article  Google Scholar 

  30. Qian, Z.: Structured Contextual Rewriting. in: Proc. 2nd Int'l Conf. on Rewriting Techniques and Applications, Bordeaux '87. LNCS (to appear).

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Universität Bremen, Germany

    Bernd Krieg-Brückner

Authors
  1. Bernd Krieg-Brückner
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

A. Nico Habermann Ugo Montanari

Rights and permissions

Reprints and permissions

Copyright information

© 1987 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Krieg-Brückner, B. (1987). Integration of program construction and verification: the PROSPECTRA methodology. In: Habermann, A.N., Montanari, U. (eds) System Development and Ada. Lecture Notes in Computer Science, vol 275. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-18341-8_21

Download citation

  • DOI: https://doi.org/10.1007/3-540-18341-8_21

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-18341-9

  • Online ISBN: 978-3-540-47885-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation