Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
ATES: Specifications of the programming language. Report of the ESPRIT Project no. 1222(1158), CISI Ingenierie, (September 1986).
ATES: Proof User Manual of the ATES system. Report of the ESPRIT Project no. 1222(1158), CISI Ingenierie, (May 1989).
ATES: 1D-Heat Transfer Stationary Problem. Report of the ESPRIT Project no 1222(1158), CISI Ingenierie, Task AP.P1, (November 1989).
Bjorner, D., Jones, C.B.: Formal Specification & Software Developement. Prentice/Hall International (1982).
Luckham, D.C., von Henke, F.W.: An overview of Anna, a specification Language for Ada. Standford University, (March 1985).
Dijkstra, E.W.: A discipline of programming. Prentice Hall Series in Automatic Computation (1976).
Floyd, R.: Assigning meanings to programs. Mathematical Aspects of computer Science, XIX American Mathematical Society, 19-32, (1967).
Gallier, J.H.: Logic for Computer Science, Foundations of Automatic Theorem Proving. Harper & Row Publishers, New Yordk (1986).
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).
Hoare, C.A.R.: An axiomatic basis for computer programming. Communications of the ACM 12 576-580, 583 (october 1969).
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).
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).
Manna, Z.: Mathematical Theory of Computation. Weizmann Institute of Science, Mc GRAW-HILL Computer Science Series, (1974).
Naur, P.: Proofs of algorithms by general snapshots. BIT 6, 310–316 (1969).
Vangeersdael, J.: An overview of proof systems. ESPRIT Project ATES 1158, Philips Research Laboratory, Brussels (1987).
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).
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).
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.
Plaisted, D.A.: Theorem proving with abstraction. Artificial Intelligence 16. North Holland Publishing Company, (1981), pp. 47-108.
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).
Ghezzi, C., Jazayeri, M.: Programming language concepts. Wiley, New York, (1987) (2nd edition).
Gries, D.: The Science of Programming, Springer-Verlag. New York (1983).
Jones, C.B.: Systematic software development using VDM. Prentice Hall, New York, (1990).
Liskov, B., Guttag, J.: Abstraction and Specification in Program Development. The MIT Press, Cambridge, (1986).
Ratcliff, B.: Software engineering: principles and methods. Blackwell, Oxford (1987).
Sommerville, I.: Software engineering. Addison-Wesley Publ. Co, Wokingham (1989).
Manna, Z., Waldinger, R.: Logical Basis for Computer Programming. Addison-Wesley Publ. Co, Reading MA, (1985).
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1991 ECSC - EEC - EAEC, Brussels - Luxembourg
About this chapter
Cite this chapter
Puccetti, A. (1991). Proving the Correctness of ATES Programs. In: Puccetti, A. (eds) The Programming and Proof System ATES. Research Reports ESPRIT, vol 1. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-84542-0_6
Download citation
DOI: https://doi.org/10.1007/978-3-642-84542-0_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-54188-2
Online ISBN: 978-3-642-84542-0
eBook Packages: Springer Book Archive