29 results for Reeves, Steve, Working or discussion paper

  • Guarded operations, refinement and simulation

    Reeves, Steve; Streader, David (2009-06-10)

    Working or discussion paper
    University of Waikato

    Simulation rules have long been used as an effective computational means to decide refinement relations in state-based formalisms. Here we investigate how they might be amended so as to decide the event-based notion of singleton failures refinement of abstract data types or processes that have operations with a "guarded" interpretation. As the results presented here and found elsewhere in the literature are so sensitive to the details of the definitions used, we have machine-checked our results.

    View record details
  • Stepwise refinement of processes

    Reeves, Steve; Streader, David (2005-01-01)

    Working or discussion paper
    University of Waikato

    Industry is looking to create a market in reliable "plug-and-play" components. To model components in a modular style it would be useful to combine event-based and state-based reasoning. One of the first steps in building an event-based model is to decide upon a set of atomic actions. This choice will depend on the formalism used, and may restrict in quite unexpected ways what we are able to formalise. In this paper we illustrate some limits to developing real world processes using existing formalisms, and we define a new notion of refinement, vertical refinement, which addresses some of these limitations. We show that using vertical refinement we can rewrite specification into a different formalism, allowing us to move between handshake processes, broadcast processes and abstract data types.

    View record details
  • Atomic components

    Reeves, Steve; Streader, David (2004-02)

    Working or discussion paper
    University of Waikato

    There has been much interest in components that combine the best of state-based and event-based approaches. The interface of a component can be thought of as its specification and substituting components with the same interface cannot be observed by any user of the components. Here we will define the semantics of atomic components where both states and event can be part of the interface. The resulting semantics is very similar to that of (event only) processes. But it has two main novelties: one, it does not need recursion or unique fixed points to model nontermination; and two, the behaviour of divergence is modelled by abstraction, i.e. the construction of the observational semantics.

    View record details
  • Comparison of data and process refinement

    Reeves, Steve; Streader, David (2003-05)

    Working or discussion paper
    University of Waikato

    When is it reasonable, or possible, to refine a one place buffer into a two place buffer? In order to answer this question we characterise refinement based on substitution in restricted contexts. We see that data refinement (specifically in Z) and process refinement give differing answers to the original question, and we compare the precise circumstances which give rise to this difference by translating programs and processes into labelled transition systems, so providing a common basis upon which to make the comparison. We also look at the closely related area of subtyping of objects. Along the way we see how all these sorts of computational construct are related as far as refinement is concerned, discover and characterise some (as far as we can tell) new sorts of refinement and, finally, point up some research avenues for the future.

    View record details
  • µ-Charts and Z: hows, whys and wherefores

    Reeve, Greg; Reeves, Steve (2000-03)

    Working or discussion paper
    University of Waikato

    In this paper we show, by a series of examples, how the µ-chart formalism can be translated into Z. We give reasons for why this is an interesting and sensible thing to do and what it might be used for.

    View record details
  • A logic for the schema calculus

    Henson, Martin C.; Reeves, Steve (1998-03)

    Working or discussion paper
    University of Waikato

    In this paper we introduce and investigate a logic for the schema calculus of Z. The schema calculus is arguably the reason for Z’s popularity but so far no true calculus (a sound system of rules for reasoning about schema expressions) has been given. Presentations thus far have either failed to provide a calculus (e.g. the draft standard [3]) or have fallen back on informal descriptions at a syntactic level (most text books e.g. [7]). Once the calculus is established we introduce a derived equational logic which enables us to formalise properly the informal notations of schema expression equality to be found in the literature.

    View record details
  • New foundations for Z

    Henson, Martin C.; Reeves, Steve (1998-03)

    Working or discussion paper
    University of Waikato

    We provide a constructive and intensional interpretation for the specification language Z in a theory of operations and kinds T. The motivation is to facilitate the development of an integrated approach to program construction. We illustrate the new foundations for Z with examples.

    View record details
  • A teaching and support tool for building formal models of graphical user-interfaces

    Reeves, Steve (1995-08)

    Working or discussion paper
    University of Waikato

    In this paper we propose the design of a tool that will allow the construction of a formal, textual description of a software system even if it has a graphical user-interface as a component. An important aspect of this design is that it can be used for two purposes—the teaching of predicate calculus and the formal specification of graphical user-interfaces. The design has been suggested by considering a system that has already been very successful for teaching predicate logic, namely Tarski's World.

    View record details
  • Towards an integrated refinement environment for formal program development

    Reeves, Steve; Grundy, John C. (1995-08)

    Working or discussion paper
    University of Waikato

    One of the main hurdles to the general adoption of formal program development techniques is a lack of tools to support their use in combination with more traditional development techniques. This paper describes an integrated environment for software development which embodies the aim of formal program development. Multiple levels of refinement of each specification are supported, with associated proof obligations, each of which can be viewed at various levels of detail throughout the development process. All of these formal views are kept consistent with each other and with more traditional design and implementation views. This allows software developers to specify, design, refine, prove, implement and document their software within a single integrated environment.

    View record details
  • A logic for specifying and reasoning about cooperative environments

    Reeves, Steve (1995-08)

    Working or discussion paper
    University of Waikato

    In this paper we describe the current progress of an attempt to develop a logic which will allow us to specify required properties of systems which typically consist of a single interactive program being used, probably simultaneously, by several agents, usually people. The logic is a development of ideas from modal logic and their more recent developments to describe computation. Since modal logic (and its extensions) are still relatively new to most people we give introductions to these logics in this paper, assuming only a familiarity with classical first-order logic and some proof theory. We also give an account of some of the sorts of situations that we want to specify. Finally, we consider what work will be needed in the future, building on what we present here, in order to achieve our goal of providing a language in which to specify and reason about systems intended to support co-operative working.

    View record details
  • MiraCalc: the Miranda Calculator, the Unix version

    Goldson, Doug; Hopkins, Mike; Reeves, Steve (1994-04)

    Working or discussion paper
    University of Waikato

    Those of you who already have some experience of programming, or experience of simply using a computer, will know that computers can be very unforgiving. They are fussy, and unless you get things exactly right they will complain. The program described in this document has grown out of an attempt to help you to understand what is going on when the computer complains. It is designed to help you with the Miranda scripts that you will be writing as part of the process of learning Miranda (or indeed any other similar functional programming language like Gofer or Haskell).

    View record details
  • A calculator for supporting derivation in constructive type-theory: PICTCalc

    Reeves, Steve (1994-06)

    Working or discussion paper
    University of Waikato

    PICTCalc is an interactive program written in LPA Prolog which has encoded within it the rules of Martin-Löf's constructive type theory (CTT), a formal system based on the constructive or intuitionistic mathematics of Brouwer, Heyting and others. It allows us to specify and express any total, computable function, so from a computer science point of view we can write both specifications and programs, along with the derivations which lead from one to the other, in a single language. PICTCalc is a more recent version of MacPICT which is itself a reconstruction of PICT [Ham92] and is intended as a test-bed for providing formal support for work within CTT. Many of the developments and improvements were suggested by students since they used the system to work on substantial courseworks. As we shall see, PICTCalc can be used to assist in the development of derivations in CTT and so it is called a derivation assistant (DA). In this paper I show how PICTCalc can be used for supporting derivations in CTT and consider what current experience suggests for future improvement. The examples in this paper will not require any knowledge of CTT since the meaning will either be clear to anyone with experience of logic and programming notations in general or will be explained as necessary.

    View record details
  • Proceedings of the First New Zealand Formal Program Development Colloquium

    Reeves, Steve (1994-11)

    Working or discussion paper
    University of Waikato

    This volume gathers together papers presented at the first in what is planned to be a series of annual meetings which aim to bring together people within New Zealand who have an interest in the use of formal ideas to enhance program development. Throughout the World work is going on under the headings of "formal methods", "programming foundations", "formal software engineering". All these names are meant to suggest the use of soundly-based, broadly mathematical ideas for improving the current methods used to develop software. There is every reason for New Zealand to be engaged in this sort of research and, of growing importance, its application. Formal methods have had a large, and growing, influence on the software industry in Europe, and lately in the U.S.A. it is being seen as important. An article in September's "Scientific American" (leading with the Denver Airport debacle) gives an excellent overview of the way in which these ideas are seen as necessary for the future of the industry. Nearer to home and more immediate are current speculations about problems with the software running New Zealand's telephone system. The papers in this collection give some idea of the sorts of areas which people are working on in the expectation that other people will be encouraged to start work or continue current work in this area. We also want the fact that this works is going on to be made known to the New Zealand computer science community at large.

    View record details
  • Notes: an experiment in CSCW

    Apperley, Mark; Gianoutsos, Simon; Grundy, John C.; Paynter, Gordon W.; Reeves, Steve; Venable, John R. (1996-04)

    Working or discussion paper
    University of Waikato

    Computer Supported Co-operative Work (CSCW) systems are complex, yet no computer-based tools of any sophistication exist to support their development. Since several people often need to work together on the same project simultaneously, the computer system often proves to be a bottleneck. CSCW tools are a means of allowing several users to work towards their goal. Systems development is essentially a team process, yet support for CSCW on these systems is in its infancy.

    View record details
  • CSCW in New Zealand: a snapshot

    Blackett, Colin; Reeves, Steve (1996-07)

    Working or discussion paper
    University of Waikato

    This report has been produced as one of the outputs of the FORST funded project "Improved Computer Supported Collaborative Work Systems" which is currently running in the Department of Computer Science at the University of Waikato. Its aim is to give a snapshot of the uses of and possibilities for Computer Supported Collaborative (also Co-operative) Work (also Working) (CSCW) within New Zealand.

    View record details
  • LSB - Live and Safe B: Alternative semantics for Event B

    Reeves, Steve; Streader, David (2006-07-01)

    Working or discussion paper
    University of Waikato

    We define two lifted, total relation semantics for Event B machines: Safe B for safety-only properties and Live B for liveness properties. The usual Event B proof obligations, Safe, are sufficient to establish Safe B refinement. Satisfying Safe plus a simple additional proof obligation ACT REF is sufficient to establish Live B refinement. The use of lifted, total relations both prevents the ambiguity of the unlifted relational semantics and prevents operations being clairvoyant.

    View record details
  • Revising Z: semantics and logic

    Henson, Martin C.; Reeves, Steve (1998-03)

    Working or discussion paper
    University of Waikato

    We introduce a simple specification logic Zc comprising a logic and semantics (in ZF set theory). We then provide an interpretation for (a rational reconstruction of) the specification language Z within Zc. As a result we obtain a sound logic for Z, including the schema calculus. A consequence of our formalisation is a critique of a number of concepts used in Z. We demonstrate that the complications and confusions which these concepts introduce can be avoided without compromising expressibility.

    View record details
  • The syntax and semantics of μ-Charts

    Reeve, Greg; Reeves, Steve (2004-02)

    Working or discussion paper
    University of Waikato

    μ-Charts is a language for specifying the behaviour of reactive systems. The language is a simplified variant of the well-known language Statecharts that was introduced by Harel. Development of the μ-Charts language is ongoing research undertaken under the auspices of the Formal Methods Laboratory of the Computer Science Department, University of Waikato. This paper gives a comprehensive treatment of the syntax and semantic for μ-Charts.

    View record details
  • A robust semantics hides fewer errors

    Reeves, Steve; Streader, David (2009-06-10)

    Working or discussion paper
    University of Waikato

    In this paper we explore how formal models are interpreted and to what degree meaning is captured in the formal semantics and to what degree it remains in the informal interpretation of the semantics. By applying a robust approach to the definition of refinement and semantics, favoured by the event-based community, to state-based theory we are able to move some aspects from the informal interpretation into the formal semantics.

    View record details
  • Experiences using Z animation tools.

    Reeve, Greg; Reeves, Steve (2001-05-01)

    Working or discussion paper
    University of Waikato

    In this paper we describe our experience of using three different animation systems. We searched for and decided to use these tools in the context of a project which involved developing formal versions (in Z) of informal requirements documents, and then showing the formal versions to people in industry who were not Z users (or users of any formal techniques). So, an animator seemed a good way of showing the behaviour of a system described formally without the audience having to learn Z. A requirement, however, that the tools used have to satisfy is that they correctly animated Z (whatever that may mean) and they behave adequately in terms of speed and presentation. We have to report that none of the tools we looked at satisfy these requirements--though to be fair all of them are still under development.

    View record details