Conferences on Intelligent Computer Mathematics - Birmingham 2008
CICM '08

Doctoral Programme

Birmingham, UK, 29-31 July 2008

Fulya Horozal: Flexible Degrees of Formality in Large Scale Mathematical Specifications

We present a PhD proposal in the field of mathematical knowledge management, where we will look at large scale mathematical specifications used in software development. The research will be concerned with the following problem. Formal software specifications are usually too complex to be worked on with a single domain-specific tool. Often, a collaboration of various such tools is needed. Moreover, methods used for formal software specifications do not integrate well with informal methods which dominate in practice due to the high cost of formalization. Our main research objective is to design a framework (1) to allow for the heterogeneity of software specifications, and (2) to take the first steps towards filling the gap between formal and informal methods. Therefore, we will firstly focus on logic translations, which are crucial in large specifications and proofs that use multiple logics. We will look at specific translations in the light of an existing framework that combines approaches from proof theory and model theory, and extend the framework to support for possibly arbitrary logics. Secondly, we will design a document framework that integrates documents, which may contain software specifications, code, documentation or proofs that are used to verify software. Our main goal in this framework is to embed the notion of flexible degrees of formality into the document structure. This means that documents may vary in their degree of formalization as their content can be formal, semi-formal and informal as well as a combination of these forms. We aim at using this notion in industry-scale projects to ease the software development processes by means of knowledge management services, such as management of change. In the case where documents contain formal proofs, the framework will adapt the notion of flexible degrees of formality to proofs, which will yield us heterogeneity in the proof structure and content. Heterogeneous proofs will contain subproofs formalized in different logics, and logic translations will be used as a transition step between two subproofs. As a second aspect of heterogeneity we will allow proofs to partially contain informal content as well. Finally, we will evaluate the proposed framework with case studies, where we will in particular investigate the applicability of management of change to small-sized specifications from industry.