Current Research

Theory and Technology for Developing High Quality Software

High quality software should behave correctly and have efficient execution time and memory use. From the viewpoint of software engineering high quality software must also be well-structured, reusable, and well-documented. By focusing on the correctness of software we are studying how to prove that a given program behaves as desired and how to construct a program that satisfies a given specification.
We are studying the following three research subjects:

1. Proving a program satisfies a specification

A program specification is a description of the expected behavior of the program. Specifications are described in natural language, in formal or logical language, or as another program whose behavior is clear, etc. For specifications written as logical formulas, the problem we are studying can be treated as a problem of theorem proving or model checking. In this study, we adopt a framework in which specifications are written as equations and programs are written as term rewriting systems, which are a model of functional programming languages. In this framework the problem is reduced to proving inductive theorems. We are mainly studying implicit induction methods for proving inductive theorems.

2. Constructing programs from specifications

Programs are usually developed stepwisely. In other words, they are constructed by extending existing programs. The purpose of this study is to automate such a program construction method. More precisely, existing programs are assumed to be term rewriting systems, specifications are equations with quantifiers ∀ and ∃, and the program to be constructed is in the form of term rewriting systems. We are currently devising a transformational method consisting of transformation rules that transform pairs of a specification and a program into another. Starting from a pair of a specification and an existing program, the method repeats the transformation to get the desired program. For example, let us consider the following specification S₀ and program P₀:

 

P₀ is a program of function h that halves natural numbers, and S₀ is a specification of function d that doubles natural numbers. By repeatedly applying transformation rules to (S₀/; P₀) we eventually obtain the following S_n:



Program S_n is guaranteed to satisfy specification S₀

3. Proving the basic properties of programs

There are several common basic program properties:
・A program eventually terminates (termination)
・The computed value is unique (uniqueness of values)
・A program never stops unexpectedly (deadlock freeness)
・No information is leaked (secrecy)
・No data is falsified (integrity)
For each property so far, many works have been done for devising a method that checks whether the program has the properties. We are studying methods for efficiently checking the termination of term rewriting systems. We also approach the secrecy and integrity of programs by using typing techniques for programs.