Frameworks are increasingly being recognised as very useful components in the emerging paradigm of component-based software development (CBD). They are widely accepted as better units of reuse than objects. The CBD methodology Catalysis, for instance, uses frameworks. However, at present, Catalysis frameworks are described only informally, which means we cannot reason formally about frameworks, in particular their composition, and thereby their reuse. For this, we would need to specify frameworks (and their composition) formally. In this paper, we describe our approach for doing so.

In current OO design, most of the existing (semi-formal) methods use classes or objects as the basic unit of design. However it is increasingly recognised that classes are not the best focus for design. Typical design artefacts are about groups of objects and the way they interact In the Catalysis project, we use the term frameworks for descriptions of groups of objects, their relationships, division of responsibilities, and interactions. The power of frameworks lies in the fact that interactions can also occur at the level of frameworks. In a previous paper we defined a framework formally as a (first-order) many-sorted theory with a model theoretic semantics and showed how it can be represented using a pictorial notation for practical system development. However we considered only frameworks that do not interact with one another In this paper we discuss frameworks that interact with one another and show that such frameworks are very powerful tools for formal OO design.

In OO Design, it is widely recognised that the distribution of tasks between objects and the contracts between them are key to effective design. In composing designs from reusable parts, the parts are therefore frameworks, namely descriptions of the interactive relationships between objects which participate in the interactions. Designs are then built by composing these frameworks, and any object in the final design will play (various) roles from several frameworks. Practitioners of OO Design use pictorial notations for design. However, in order to reason formally about design, we need a sound (formal) semantics for the diagrams. In this paper, we show that frameworks can be formalised as many-sorted theories, and then present a pictorial representation of such theories, developed in the Catalysis project.

It can be argued that for (semi-)automated software development, program schemas are indispensable, since they capture not only structured program design principles but also domain knowledge, both of which are of crucial importance for hierarchical program synthesis. Most researchers represent schemas purely syntactically (as higher-order expressions). This means that the knowledge captured by a schema is not formalised. We take a semantic approach and show that a schema can be formalised as an open (first-order) logical theory that contains an open logic program. By using a special kind of correctness for open programs, called steadfastness, we can define and reason about the correctness of schemas. We also show how to use correct schemas to synthesise steadfast programs.

The aim of this paper is to show the fruitfulness and fecundity of the authors' proof-theoretic analysis of logic programming (both for definite and normal programs). It is based on a simple logical framework that goes under the name of regular search spaces. The challenge faced here is to give a treatment in proof-theoretic terms of the issue of negation, which has been one of the toughest problems that has plagued logic programming from its very beginning. While negation-as-failure (NF) has been overwhelmingly the more widespread answer, its intrinsic limitations have made it a rather unsatisfactory solution. In the present paper it is first contended that the notion of regularity offers a better understanding of the traditional theory of NF, and second a firm yet very simple and natural basis for a form of constructive negation, in the sense of Chan, Stuckey and Harland. A version of constructive negation is presented, based on the notion of regular splitting, a transformation technique where the failure axiom(s) of a predicate occurring negatively in a program are split into new clauses according to a covering of the underlying signature.

This paper deals with the problem of constructing the final version Pt of a flowchart program through successive refinements P2, …, Pt−1 that preserve correctness proved on its first version P1. Correctness conditions are associated with P1 in the frame of Manna's formalism. With each refinement Pi a relational (data) structure Si is associated, and given representation functions τi relate structures Si, Si+1 of refinements Pi, Pi+1. Construction of Pi+1 from Pi proceeds as follows: (a) every block of Pi is considered as an elementary program over Si and its correctness conditions are expressed with terms of Si; (b) these correctness conditions are translated by using the representation function τi; (c) the translated correctness conditions are transformed into expansion conditions, expressed with terms of Si+1 only, for every block of Pi; (d) by means of these expansion conditions, expansions of blocks are constructed and connected to obtain Pi+1. The constructive character of the above process is emphasised with a detailed example. In the appendix a discussion relates this paper to other works connecting constructivism and program theory.