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. (1994) Proektirovanie korrektnyh strukturirovannyh programm. Moskva
Basili, V.R., Selby, R.W. (1993) Comparing the effectiveness of software testing strategies, components. IEEE computer society
Berković, I. (1997) The deductive bases for development of the descriptive language for the logical programming. University of Novi Sad, Ph.D.Thesis
Čubrilo, M. (1989) Mathematical logic for expert's systems
Dahl, O.J., Dijkstra, E.W., Hoare, C.A.R. (1972) Structured programming. New York-San Diego, itd: Academic Press
Dijkstra, E.W. (1993) A discipline of programming. Englewood Cliffs, NJ, itd: Prentice Hall
Glesner, S. (2003) Using program checking to ensure the correctness of compiler implementation. Journal of University Comp. Sciences, 9(3) 191-222
Hoare, C.A. (1969) An axiomatic basis for computer programming. Communications of the ACM, 12(10): 576
Hoare, C.A., Wirth, N. (1973) An axiomatic definition of the programming language PASCAL. Acta Informatica, 2(4): 335
Hotomski, P., Berković, I. (2002) Symbolical execution of Pascal programs in theorem prover of Baselog system, Tara
Jazayeri, M., Looos, R.G.K., Musser, D.R. (2000) Generic programming LNCS 1766. Springer
Klein, G., Nipkow, T. (2003) Verified bytecode verifiers. u: Theoretical Computer Sciences
Krishnamurthi, S., Fisler, H., Greenberg, M. (2004) Verifying aspect advice modularly. Foundations of Software Engineering
Manna, Z. (1969) The correctness of programs. Journal of Computer and System Sciences, 3 (2)
Manna, Z. (1974) Mathematical theory of computation. McGraw-Hill
Markoski, B. (2000) Program testing and deductive checking of their validaty. Novi Sad: Faculty of Technical Sciences, MS Thesis
Mills, H., Linger, R. (2002) Cleanroom software engineering encyclopedia of software engineering. New York: John Wiley & Sons
Nipkow, T., Paulson, L.C., Wenzel, M. (2002) A proof assistant for higher-order logic. Lecture Notes in Computer Science, vol. 2283
Pascual, J.I. (2002) On the correctness of the factoring transformation. u: FLOPS
Radulović, B., Hotomski, P. (2000) Projecting deductive databases with CWA management in Baselog-systems. Journal of Mathematics, Novi Sad, vol. 30, br. 2, str. 133-140
Sihman, M., Katz, S. (2003) Model Cbeching application of aspect and superimposition. u: Leavents G.T., C.Clicton [ur.] FOAL
Downloads
Published
Issue
Section
License
Copyright (c) YUJOR
This work is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.
