Which logic to use for program specifications?
by
Enn Tyugu
Royal Institute of Technology

As the program synthesis from specifications is gaining popularity, more results in logic find application in practice. The answer to the question in the title depends not on the expressibility and derivability in principle, but on the efficiency and ease of usage. There are two contradictory requirements on the language of specifications for program synthesis: its expressiveness and ease of proof search in the logic with the given language. From the other side, one has some freedom to draw a border between what should be expressed in the logic and what is preprogrammed in the functional constants -- preprogrammed building blocks of a synthesized program. (We assume that the set of constants is extendible like, for instance, in any practical implementation of Prolog.) The usage of intuitionistic propositional logic for specifying purely functional programs has been justified by program synthesis practice under the condition that, for the user´s convenience, the user language is a syntactic (macro) extension of the propositional language. However, in such a case, 1) we need a sufficiently rich set of functional constants, including functions of second order, 2) we are unable to express the exact relation between an input and the output of a function, and have to rely completely on the correctness of the preprogrammed constants and specifications. Lets note that the second order functions encode control of computations (various ways of composition of functional arguments). This allows us even to synthesize recursive programs from propositional specifications. If we use first order Horn clauses as in Prolog, then the set of preprogrammed constants need not be rich, but we must specify more control explicitly. Intuitionistic propositional temporal logic suits well for synthesis of processes specified by state transition relations. Here we must again completely rely on correctness of preprogrammed functions, because we are unable to reason about the exact properties of functions. If one still wishes to reason about functions in detail, we suggest the usage of annotations written in another and more expressive language. Then one can use a simple logic for fast synthesis of a structure of a program, and a more powerful logic for verifying the correctness of results of the synthesis, e.g. correctness of synthesized recursion. The languages above are more or less suited for completely automatic synthesis, which is of our primary concern. If one decides to perform synthesis interactively, i.e. not completely automatically, then one gets considerable freedom in choice of the form of specifications. The Kestrel Institute group believes in the usefulness of the category theory in program synthesis and combines it with algebraic specifications. Constructive type theory is used traditionally by the Cornell University group, and by Gothenburg group. In order to write exact and complete specifications for synthesis of recursive (and co-recursive) programs, one can choose a language including mu and nu operators for specification of recursion (co-recursion). Last but not least, program synthesis pursued by the Stanford group started in the classical first order language of specifications, (which should be done carefully, in order to be able to extract a program from a proof), but their interest has shifted to the synthesis of reactive programs in temporal logic.

http://www.it.kth.se/~tyugu

Date received: March 11, 1999