The aim of this tutorial is to acquaint attendees with the primary models of program semantics; to present logics based on formal program models; to study relationship between such logics; to discuss applicability of program logics in program analysis and verification.

Computer Programming, as well as Software Engineering in general, is a grateful area of logic application. Logics can be used at every stage of software development cycle, in particular, during requirement analysis, specification, design, verification, and testing.

To be successful, such logics should adequately represent essential features of the development stages. Among various logics, oriented on software development, the central place belongs to logics describing main properties of computer programs. Such logics should be based on formal program models.

The tutorial consists of three sessions:

1. Review of program-oriented logics. Formal models of programs.


2. Program-oriented first-order logics of predicates and functions with non-fixed arity. Their relationships with classical first-order logic. Soundness and completeness of logics.


3. Program logics of Floyd-Hoare style of partial predicates and functions over hierarchical data structures. New consequence relations, their properties. Applicability of program logics.

The main questions to be discussed during the first session are short review of program-oriented logics and main methods of description of formal semantics of programs:

• denotational semantics in style of Scott–Strachey;
• operational semantics in style of Gordon D. Plotkin;
• axiomatic semantics in style of Floyd-Hoare.

Then we describe various classes of mappings used to represent program semantics such as n-ary mappings, mappings with non-fixed arity (quasiary mappings), and mappings over hierarchical data. We demonstrate that these classes have different compositional properties that affect program construction and investigation.

During the second session, we construct various first-order logics based on the described classes of mappings. We demonstrate that each logic has specific features which are not characteristic for classical logic based on n-ary mappings. Soundness and completeness of such logics are discussed.

The last session is devoted to construction of various types of Floyd-Hoare program logics.

We investigate classical Floyd-Hoare logic, logics with partial predicates and functions, logics over hierarchical data. Such analysis demonstrates that even in a case of simple programs we have to introduce new rather complicated consequence relations and new rules of calculi.

In conclusion, we formulate the main challenging problems of program logics construction and investigation and discuss approaches to their solution.

Bibliography

1. Nielson H.R., Nielson F. Semantics with Applications: A Formal Introduction. John Wiley & Sons Inc (1992)
2. Hoare, C.A.R. An axiomatic basis for computer programming, Communications of the ACM, 12, pp. 576-583 (1969)
3. Sannella D., Tarlecki A. Foundations of Algebraic Specification and Formal Software Development, Springer (2012)
4. Nikitchenko M., Shkilniak S. Applied Logic, Publishing house of Taras Shevchenko National University of Kyiv, Kyiv, 278 p. (In Ukrainian, 2013)
5. Kryvolap A., Nikitchenko M. Schreiner W. Extending Floyd-Hoare logic for partial pre- and postconditions, CCIS 412, Springer, Heidelberg, pp. 355-378 (2013)

Back to the 6th Universal Logic School !