Resolution methods in proving the program correctness
DOI:
https://doi.org/10.2298/YJOR0702275MKeywords:
test, specification, resolution, program correctnessAbstract
Program testing determines whether its behavior matches the specification, and also how it behaves in different exploitation conditions. Proving of program correctness is reduced to finding a proof for assertion that given sequence of formulas represents derivation within a formal theory of special predicted calculus. A well-known variant of this conception is described: correctness based on programming logic rules. It is shown that programming logic rules may be used in automatic resolution procedure. Illustrative examples are given, realized in prolog-like LP-language (with no restrictions to Horn's clauses and without the final failure). Basic information on LP-language are also given. It has been shown how a Pascal-program is being executed in LP-system proffer.References
Alagić, S., Arbib, M., Proektirovanie korrektnyh strukturirovannyh programm, Moskva, 1994.
Basili, V.R., and Selby, R.W., Comparing the Effectiveness of Software Testing Strategies, Components, a publication of the IEEE computer society, 1993.
Berković, I., "The deductive bases for development of the descriptive language for the logical programming", Ph.D. Thesis, University of Novi Sad, 1997.
Čubrilo, M., Mathematical logic for expert’s systems, 1989.
Dahl, O.J., Dijkstra, E.W., and Hoare, C.A.R, Structured Programming, Academic Press, 1972, 83-174.
Dijkstra, E.W., "A Discipline of Programming", Prentice-Hall, 1993.
Glesner, S., "Using program checking to ensure the correctness of compiler implementation", Journal of University Comp. Sciences, 9(3) (2003) 191-222.
Hoare, C.A.R., "An axiomatic basis for computer programming", Communications of the ACM, 12 (1973) 576-583.
Hoare, C.A.R., and Wirth, N., "An axiomatic definition of the programming language Pascal", Acta Informatica, 2 (1973) 335-355.
Hotomski, P., and Berković, I., "Symbolical execution of Pascal programs in theorem prover of Baselog system", Tara, 2002.
Jazayeri, M., Looos, R.G.K., and Musser, D.R., "Generic Programming", LNCS 1766, Springer, 2000.
Klein, G., Nipkow, T., "Verified Bytecode Verifiers", Theoretical Computer Sciences, 2003.
Krishnamurthi, S., Fisler, H., and Greenberg, M., "Verifying aspect advice modularly", Foundations of Software Engineering, 2004.
Manna, Z., "The correctness of programs", Journal of Computer and System Sciences, 3 (2) 1969.
Manna, Z., Mathematical Theory of Computation, McGraw-Hill, 1974.
Markoski, B., "Program testing and deductive checking of their validity", MS Thesis, University of Novi Sad, Faculty of Technical Sciences, Novi Sad, 2000.
Mills, H., and Linger, R., "Cleanroom Software Engineering", Encyclopedia of Software Engineering, 2nd (J. Marciniak, ed.), New York: John Wiley & Sons, 2002.
Nipkow, T., Paulson, L.C., Wenzel, M., "A proof assistant for higher-order logic", Springer, Lecture Notes in Computer Science, Vol 2283, 2002.
Pascual, J.I., "On the Correctness of the Factoring Transformation", FLOPS, 2002.
Radulović, B., Hotomski, P., "Projecting Deductive Databases with CWA Management in Baselog system", Novi Sad J. Math, Vol. 30, No 2, 2000.
Sihman, M., and Katz, S., "Model Checking application of aspect and superimposition", In G.T. Leavents and C. Clicton (eds.), FOAL, 2003.
Downloads
Published
Issue
Section
License
Copyright (c) 2007 YUJOR
This work is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.
