Logic and Computer Programming
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:
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:
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.
Back to the 6th Universal Logic School !