Null pointer exceptions are subtle errors that have a negative effect on pro- grams, such as causing the program to terminate or crash. These errors are nor- mally detected through running and testing the actual program, which is inef- ficient and not 100% effective. Another approach is to use static checking tools that can automatically analyze program code and look for errors. However such tools are unable to detect null pointer exceptions. This project focuses on developing, implementing, and evaluating a static error checking tool that will detect null pointer exceptions within Java code.

In this paper an outline is given of an approach to formally reasoning about importation , parameterisation and instantiation of speciications written in a modular extension of the Z language (called Sum). Interpretation and instantiation of theories in rst order logic are well understood. We illustrate how to use these results directly to provide a framework within which we can soundly and eeciently reason about modular speciications. A reasoning environment within the Ergo 4:1 theorem prover has been constructed that provides the theory management, construction and extension facilities needed to support such a reasoning process. Sum speciications are mapped to the appropriate Ergo structures by a straightforward translation process. A simple example in Sum is presented to demonstrate the use of these theory extension mechanisms. As far as the authors are aware, no other system ooers interpreted automated support for reasoning about parameterisation and instantiation of modular model-oriented speciications.

The Cogito system provides comprehensive support for the development of specifications written in the Sum language (a modular extension of Z). The tool-set provides technology to aid in the construction, analysis and development of Sum specifications. Ada code is the final result of a development in Cogito.

In this paper we demonstrate a refinement calculus for logic programs, which is a framework for developing logic programs from specifications. The paper is written in a tutorial-style, using a running example to illustrate how the refinement calculus is used to develop logic programs. The paper also presents an overview of some of the advanced features of the calculus, including the introduction of higher-order procedures and the refinement of abstract data types.

Existing refinement calculi provide frameworks for the stepwise development of imperative programs from specifications. This paper presents a refinement calculus for deriving logic programs. The calculus contains a wide-spectrum logic programming language, including executable constructs such as sequential conjunction, disjunction, and existential quantification, as well as specification constructs such as general predicates, assumptions and universal quantification. A declarative semantics is defined for this wide-spectrum language based on executions. Executions are partial functions from states to states, where a state is represented as a set of bindings. The semantics is used to define the meaning of programs and specifications, including parameters and recursion. To complete the calculus, a notion of correctness-preserving refinement over programs in the wide-spectrum language is defined and refinement laws for developing programs are introduced. The refinement calculus is illustrated using example derivations and prototype tool support is discussed.

To support formal reasoning in mathematical and software engineering applications, it is desirable to have a generic prover that can be instantiated with a range of logics. This allows the prover to be applied to a wider variety of reasoning tasks than a fixed-logic prover. This paper describes the design principles and the architecture of the latest version of the Ergo proof engine, Ergo 6. Ergo 6 is a generic interactive theorem prover, similar to Isabelle, but with better support for proving schematic theorems with user-defined constraints, and with a different approach to handling variable scoping. A major theme of the paper is that Prolog implementation technology can be generalized to obtain efficient implementations of generic proof engines. This is demonstrated via a Qu-Prolog implementation of Ergo 6.

The refinement calculus provides a framework for the stepwise development of imperative programs from specifications. This paper presents a semantics for a refinement calculus for deriving logic programs. The calculus contains a wide-spectrum logic programming language, including executable constructs such as sequential conjunction, disjunction, and existential quantification, as well as specifications constructs (general predicates and assumptions) and universal quantification. A semantics is defined for this wide-spectrum language based on {\em executions}, which are partial functions from states to states, where a state is represented as a set of bindings. This execution semantics is used to define the meaning of programs and specifications, including parameters and recursion. To complete the calculus, a notion of correctness-preserving refinement over programs in the wide-spectrum language is defined and a refinement law for introducing recursive procedures is presented.

We report on the software development techniques used in the New Zealand software industry, paying particular attention to requirements gathering. We surveyed a selection of software companies with a general questionnaire and then conducted in-depth interviews with four companies. Our results show a wide variety in the kinds of companies undertaking software development, employing a wide range of software development techniques. Although our data are not sufficiently detailed to draw statistically significant conclusions, it appears that larger software development groups typically have more well-defined software development processes, spend proportionally more time on requirements gathering, and follow more rigorous testing regimes.

. We report on the software development techniques used in the New Zealand softwareindustry, paying particular attention to requirements gathering. We surveyed a selection of softwarecompanies with a general questionnaire and then conducted in-depth interviews with fourcompanies. Our results show a wide variety in the kinds of companies undertaking software development,employing a wide range of software development techniques. Although our data arenot sufficiently detailed to draw...

We report on the software development techniques used in the New Zealand software industry, paying particular attention to requirements gathering. We surveyed a selection of software companies with a general questionnaire and then conducted in-depth interviews with four companies. Our results show a wide variety in the kinds of companies undertaking software development, employing a wide range of software development techniques. Although our data are not sufficiently detailed to draw statistically significant conclusions, it appears that larger software development groups typically have more well-defined software development processes, spend proportionally more time on requirements gathering, and follow more rigorous testing regimes.

The refinement calculus for the development of programs from specifications is well suited to mechanised support. We review the requirements for tool support of refinement as gleaned from our experience with existing refinement tools, and report on the design and implementation of a new tool to support refinement based on these requirements. The main features of the new tool are close integration of refinement and proof in a single tool (the same mechanism is used for both), good management of the refinement context, an extensible theory base that allows the tool to be adapted to new application domains, and a flexible user interface.

A program can be refined either by transforming the whole program or by refining one of its components. The refinement of a component is, for the main part, independent of the remainder of the program. However, refinement of a component can depend on the context of the component for information about the variables that are in scope and what their types are. The refinement can also take advantage of additional information, such as any precondition the component can assume.The aim of this paper is to introduce a technique, which we call program window inference, to handle such contextual information during derivations in the refinement calculus. The idea is borrowed from a technique, called window inference, for handling context in theorem proving. Window inference is the primary proof paradigm of the Ergo proof editor. This tool has been extended to mechanize refinement using program window inference. (C) 1997 Elsevier Science B.V.

We describe some features of the tactic language implemented in the theorem proverErgo 5. This is a variant of the generic tactic language Angel. We have adapted the languageby changing the semantics of its parallel composition operator, the operator by whichdifferent tactics are applied to different branches in a proof tree. The paper includes adenotational semantics for this operator, and a collection of derived tactics which use it,together with a collection of algebraic laws which ...

The refinement calculus provides a method for transforming specifications to executable code, maintaining the correctness of the code with respect to its specification. In the original refinement calculus, the target language is an imperative programming language, but more recently a refinement calculus for deriving logic programs has been proposed. Due to the amount of detail involved, the manual refinement of programs is a tedious and time-consuming task, and is therefore an obvious candidate for tool support. Several tools exist for the imperative refinement calculus, and in this paper we describe a prototype tool to support the recently developed refinement calculus for logic programs. The tool was developed using Ergo, an interactive theorem prover. To provide tool support for the calculus, its underlying semantic model was defined within Ergo, and the laws of the calculus were proven in that framework. We illustrate the tool using a simple example refinement.

This paper addresses the practical aspects of supporting data refinement in the refinement calculus. We analyse the difficulties associated with defining and applying data refinement rules with a computer-based tool. Our analysis is illustrated by discussion of choices made when extending an existing refinement tool to support data refinement.

A new version of the Ergo theorem prover is under development. It uses a single tactic language, based on Angel, for tactic programming, user interface, and proof representation. This paper describes the language as it is used in each of these cases, and explains the details of its implementation in Qu-Prolog. An example from classical propositional calculus is included.

Note: Most SVRC technical reports are available via anonymous ftp, from svrc.it.uq.edu.au in the directory /pub/techreports. Individual abstracts and compressed postscript les are available from Abstract The reenement calculus provides a method for transforming speciications to executable code, maintaining the correctness of the code with respect to its speciication. In the original reene-ment calculus, the target language is an imperative programming language, but more recently a reenement calculus for deriving logic programs has been proposed. Due to the amount of detail involved, the manual reenement of programs is a tedious and time-consuming task, and is therefore an obvious candidate for tool support. Several tools exist for the imperative reenement calculus, and in this paper we describe a prototype tool to support the recently developed reenement calculus for logic programs. The tool was developed using Ergo, an interactive theorem prover. To provide tool support for the calculus, its underlying semantic model was deened within Ergo, and the laws of the calculus were proven in that framework. We illustrate the tool using a simple example reenement.

Reenement is a transformational method for developing programs from speciications. It generates a hierarchical structure representing design decisions. Proofs may also be viewed as hierarchical structures. The window inference proof paradigm explicitly takes advantage of hierarchical structure in proofs, and is well suited to program reenement. Both program reenements and proofs structures are complex, and powerful tools are needed to manage and present them. We discuss several approaches to the presentation of such structures, and tools to support these approaches. We also discuss how reenement and proof can be integrated, either using a multilingual document or by using a version of window inference that directly supports the reenement relation. The integration of reenement and proof has the beneet that tools supporting these activities can present a single consistent user interface. We describe prototype tools for reenement and proof, based on a window inference theorem prover with an Emacs interface , and using a sophisticated multilingual document editor.

A program can be reened either by transforming the whole program or by reening one of its components. The reenement of a component is, for the main part, independent of the remainder of the program. However, reenement of a component can depend on the context of the component for information about the variables that are in scope and what their types are. The reenement can also take advantage of additional information, such as any precondition the component can assume. The aim of this paper is to introduce a technique, which we call program window inference, to handle such contextual informationduring derivations in the reenement calculus. The idea is borrowed from a technique, called window inference, for handling context in theorem proving. Window inference is the primary proof paradigm of the Ergo proof editor. This tool has been extended to mechanize reenement using program window inference.