Proving the Correctness of ATES Programs

  • Armand Puccetti
Part of the Research Reports ESPRIT book series (ESPRIT, volume 1)


In the present chapter we will describe the method and the tools used within the ATES system to prove the correctness of an ATES operator with respect to its formal specifications.


Proof System Verification Condition Interface Specification Loop Statement Weak Precondition 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    ATES: Specifications of the programming language. Report of the ESPRIT Project no. 1222(1158), CISI Ingenierie, (September 1986).Google Scholar
  2. [2]
    ATES: Proof User Manual of the ATES system. Report of the ESPRIT Project no. 1222(1158), CISI Ingenierie, (May 1989).Google Scholar
  3. [3]
    ATES: 1D-Heat Transfer Stationary Problem. Report of the ESPRIT Project no 1222(1158), CISI Ingenierie, Task AP.P1, (November 1989).Google Scholar
  4. [4]
    Bjorner, D., Jones, C.B.: Formal Specification & Software Developement. Prentice/Hall International (1982).Google Scholar
  5. [5]
    Luckham, D.C., von Henke, F.W.: An overview of Anna, a specification Language for Ada. Standford University, (March 1985).Google Scholar
  6. [6]
    Dijkstra, E.W.: A discipline of programming. Prentice Hall Series in Automatic Computation (1976).Google Scholar
  7. [7]
    Floyd, R.: Assigning meanings to programs. Mathematical Aspects of computer Science, XIX American Mathematical Society, 19-32, (1967).Google Scholar
  8. [8]
    Gallier, J.H.: Logic for Computer Science, Foundations of Automatic Theorem Proving. Harper & Row Publishers, New Yordk (1986).Google Scholar
  9. [9]
    Gerhart, S.L., Musser, D.R., Thompson, D.H., Baker, D.A., Bates, R.L., Erickson, R.W., London, R.L., Taylor, D.G., While, D.S.: An overview of AFFIRM, a specification and verification system. USC Information Sciences Institute, Proceedings IFIP 1980, 343-347 (1980).Google Scholar
  10. [10]
    Hoare, C.A.R.: An axiomatic basis for computer programming. Communications of the ACM 12 576-580, 583 (october 1969).Google Scholar
  11. [11]
    Gordon, M.J., Milner, A.J., Wadsworth, C.P.: Edinburgh LCF, A mechanised Logic of Computation. LNCS 78, Springer-Verlag Berlin Heidelberg, New York (1979).Google Scholar
  12. [12]
    Hagino, T., Honda, M., Koga, A., Kojima, K., Nakajima, R., Shibayma, E., Yuasa, T.: The IOTA Programming System, a Modular Programming Environment. LNCS 160, Springer-Verlag. Berlin Heidelberg New York Tokyo (1983).Google Scholar
  13. [13]
    Manna, Z.: Mathematical Theory of Computation. Weizmann Institute of Science, Mc GRAW-HILL Computer Science Series, (1974).Google Scholar
  14. [14]
    Naur, P.: Proofs of algorithms by general snapshots. BIT 6, 310–316 (1969).CrossRefGoogle Scholar
  15. [15]
    Vangeersdael, J.: An overview of proof systems. ESPRIT Project ATES 1158, Philips Research Laboratory, Brussels (1987).Google Scholar
  16. [16]
    Wulf, W.A., London, R.L., Shaw, M.: An introduction to the Construction and Verification of the Alphard Programs. IEEE transactions on Software Engineering, vol SE-2, no. 4, (December 1976).Google Scholar
  17. [17]
    Greenbaum, S.: Input transformations and resolution techniques for theorem proving in first-order logic. Ph. D. This is in Computer Science, University of Illinois at Urbana Chaupaigu, (1986).Google Scholar
  18. [18]
    Abrial, J.A.: Selected documents parts of the B project, Paris, (November 1986). An informal introduction to B; A logic for B; B user manual; A simple theorem in linear algebra;. A decision package for linear arithmetic.Google Scholar
  19. [19]
    Plaisted, D.A.: Theorem proving with abstraction. Artificial Intelligence 16. North Holland Publishing Company, (1981), pp. 47-108.Google Scholar
  20. [20]
    Boyer, R.S., Strother-Moore, J.: A theorem prover for recursive functions: a user’s manual. CSL-91, Computer Science Laboratory, S.R.I. International, Mehlo Park, California, (June 1979).Google Scholar
  21. [21]
    Ghezzi, C., Jazayeri, M.: Programming language concepts. Wiley, New York, (1987) (2nd edition).Google Scholar
  22. [22]
    Gries, D.: The Science of Programming, Springer-Verlag. New York (1983).Google Scholar
  23. [23]
    Jones, C.B.: Systematic software development using VDM. Prentice Hall, New York, (1990).MATHGoogle Scholar
  24. [24]
    Liskov, B., Guttag, J.: Abstraction and Specification in Program Development. The MIT Press, Cambridge, (1986).MATHGoogle Scholar
  25. [25]
    Ratcliff, B.: Software engineering: principles and methods. Blackwell, Oxford (1987).Google Scholar
  26. [26]
    Sommerville, I.: Software engineering. Addison-Wesley Publ. Co, Wokingham (1989).MATHGoogle Scholar
  27. [27]
    Manna, Z., Waldinger, R.: Logical Basis for Computer Programming. Addison-Wesley Publ. Co, Reading MA, (1985).MATHGoogle Scholar

Copyright information

© ECSC - EEC - EAEC, Brussels - Luxembourg 1991

Authors and Affiliations

  • Armand Puccetti
    • 1
  1. 1.CISI IngénierieRungis CedexFrance

Personalised recommendations