×

zbMATH — the first resource for mathematics

A formalization of programs in first-order logic with a discrete linear order. (English) Zbl 1352.68065
Summary: We consider the problem of representing and reasoning about computer programs, and propose a translation from a core procedural iterative programming language to first-order logic with quantification over the domain of natural numbers that includes the usual successor function and the “less than” linear order, essentially a first-order logic with a discrete linear order. Unlike Hoare’s logic, our approach does not rely on loop invariants. Unlike the typical temporal logic specification of a program, our translation does not require a transition system model of the program, and is compositional on the structures of the program. Some non-trivial examples are given to show the effectiveness of our translation for proving properties of programs.
MSC:
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
03B70 Logic in computer science
Software:
Daikon; GOLOG
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Dijkstra, E., A discipline of programming, (1976), Prentice Hall Englewood Cliffs, N.J. · Zbl 0368.68005
[2] Dijkstra, E. W.; Scholten, C. S., Predicate calculus and program semantics, (1990), Springer-Verlag New York · Zbl 0698.68011
[3] Hoare, C., An axiomatic basis for computer programming, Commun. ACM, 576-580, (1969) · Zbl 0179.23105
[4] Harel, D., First-order dynamic logic, Lecture Notes in Computer Science, vol. 68, (1979), Springer-Verlag New York · Zbl 0403.03024
[5] Reynolds, J. C., Separation logic: a logic for shared mutable data structures, (Proceedings of 17th Annual IEEE Symposium on Logic in Computer Science, (2002), IEEE), 55-74
[6] Pnueli, A., The temporal semantics of concurrent programs, Theor. Comput. Sci., 13, 45-60, (1981) · Zbl 0441.68010
[7] Wegbreit, B., The synthesis of loop predicates, Commun. ACM, 17, 2, 102-113, (1974) · Zbl 0273.68014
[8] Bjørner, N.; Browne, A.; Manna, Z., Automatic generation of invariants and intermediate assertions, Theor. Comput. Sci., 173, 1, 49-87, (1997) · Zbl 0902.68120
[9] Ernst, M. D.; Cockrell, J.; Griswold, W. G.; Notkin, D., Dynamically discovering likely program invariants to support program evolution, IEEE Trans. Softw. Eng., 27, 2, 99-123, (2001)
[10] Ernst, M. D.; Perkins, J. H.; Guo, P. J.; McCamant, S.; Pacheco, C.; Tschantz, M. S.; Xiao, C., The daikon system for dynamic detection of likely invariants, Sci. Comput. Program., 69, 1, 35-45, (2007) · Zbl 1161.68390
[11] Nguyen, T.; Kapur, D.; Weimer, W.; Forrest, S., Using dynamic analysis to discover polynomial and array invariants, (Proceedings of 34th International Conference on Software Engineering, ICSE 2012, (2012), IEEE), 683-693
[12] Kozen, D.; Tiuryn, J., Logics of programs, (Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics (B), (1990), Elsevier), 789-840 · Zbl 0900.68306
[13] Emerson, E. A., Temporal and modal logic, (Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics (B), (1990), Elsevier), 995-1072 · Zbl 0900.03030
[14] Barringer, H.; Kuiper, R.; Pnueli, A., Now you may compose temporal logic specifications, (STOC, (1984)), 51-63
[15] Libkin, L., Elements of finite model theory, (2004), Springer · Zbl 1060.03002
[16] Charguéraud, A., Program verification through characteristic formulae, ACM SIGPLAN Not., 45, 9, 321-332, (2010) · Zbl 1323.68202
[17] Charguéraud, A., Characteristic formulae for the verification of imperative programs, ACM SIGPLAN Not., 46, 9, 418-430, (2011) · Zbl 1323.68366
[18] Wallace, M. G., Tight, consistent, and computable completions for unrestricted logic programs, J. Log. Program., 15, 243-273, (1993) · Zbl 0787.68021
[19] Levesque, H.; Reiter, R.; Lespérance, Y.; Lin, F.; Scherl, R., GOLOG: a logic programming language for dynamic domains, J. Logic Program., 31, 59-84, (1997), special issue on Reasoning about Action and Change · Zbl 0880.68008
[20] Lin, F., A first-order semantics for golog and congolog under a second-order induction axiom for situations, (Proceedings of KR 2014, (2014))
[21] Cohen, E., Programming in the 1990s: an introduction to the calculation of programs, (1990), Springer-Verlag · Zbl 0825.68262
[22] F. Lin, B. Yang, Reasoning about mutable data structures in first-order logic with arithmetic: lists and binary trees, Technical report, Department of Computer Science, Hong Kong University of Science and Technology, http://www.cs.ust.hk/faculty/flin/papers/dsw2015.pdf.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.