From logical theories to PO-specifications

<_author_search_(theodosis dimitrakos)>Theodosis Dimitrakos
Department of Computing
Imperial College of Science,Technology and Medicine
e-mail: td@doc.ic.ac.uk

Abstract

The logical approach to specification has been successfully used to exploit the foundations of software development in terms of theory manipulations, employing the formalism of many-sorted first order logic. When dealing with pragmatic applications though, and especially when mechanical support for refinement is considered, it seems necessary to augment this approach with features that ease the specification, reasoning and manipulation of complex entities. We demonstrate an incremental augmentation of logical specifications in the following steps:

First we establish an explicit, syntactic representation of the truth values and achieve unifying format for all signature symbols. The processes of Skolemization and Unskolemization (reverse-Skolemization) are extended to deal with all signature symbols. A clearer categoric representation of theory manipulations is gained and support for a top-down analysis of global polarity values is initiated. This approach to polarity analysis exploits the extensibility of theories in a dual manner to the classical (Lyndon's approach). A unifying assignment of polarity values over all signature symbols is achieved and various inference rules are instantaneously derived. These rules code -in a deductive fashion- how a syntactic change on the terms of a logical expression affects its meaning.

The concept of a PO-specification is finally introduced as a formalism which succeeds to capture the former. PO-specifications provide a formal basis for a mechanizable model of formal software development based on theory manipulations. The underlying logic is not affected by this augmentation and similar augmentations may be applicable to specifications in other logics (e.g. temporal or multi-valued logics).

Keywords: Many-sorted logic, complete theories, boolean algebras, Lindenbaum algebra, conservative extensions, extensive theories, partial orders with equality, analysis & assignment of polarity values.

1 Introduction

The process of software development consists of theory manipulations. This assertion is able to provide an overview of software development (describing what does happen) while establishing a viewpoint (explaining what should happen). Convincing arguments on the truthfulness of the resulting overview and the usefulness of the particular viewpoint have been given, years ago, in [Vel85, VMS85] and [TM87]. In