Invited talk at 8th International Conference on Applied Informatics (ICAI 2010)
Sprache des Tagungstitel:
Englisch
Original Kurzfassung:
We approach the generation of the verification conditions for the total correctness of both functional as well as imperative programs in a purely logical manner: The conditions must ensure the existance and uniqueness of the function implemented by the program. We assume that the program is based on an existing logical {\em object theory} which contains the properties of the objects used in the program (integers, rationals, tuples, etc.). When a new function is implemented, then its specification (input and output conditions) are added to the theory, together with the respective (new!) function symbol. Note that, since the program is using formulae and terms from this theory, no translation of these is necessary. {\em Functional programs} are just syntactic versions of the logical formulae which constitute the implicit (because of recursion) definition of the function implemented by the program. {\em Imperative programs} are meta-terms containing the usual imperative programming constructs. We use a natural and simple transformation of imperative programs into functional programs, thus defining their semantics. %This approach to semantics of imperative programs allows to generate the verification conditions in the same way as for functional programs. This transformation as well as the generation of the verification conditions are fully formalized in predicat logic as meta-level functions. They use {\em forward symbolic execution}: the values of the current variables are computed symbolically, and the branching statements generate various path conditions. There are three kinds of verification conditions: for {\em coherence}, for {\em functional} correctness, and for {\em termination}.
Sprache der Kurzfassung:
Englisch
Vortragstyp:
Hauptvortrag / Eingeladener Vortrag auf einer Tagung
Forschungs-