29 results for Reeves, Steve, Working or discussion paper

  • 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
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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
  • µ-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 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
  • 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
  • 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
  • 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
  • Eliciting usage contexts of safety-critical medical devices

    Bowen, Judy; Cunningham, Sally Jo; Hinze, Annika; Jung, Doris; Reeves, Steve (2014)

    Working or discussion paper
    University of Waikato

    This position paper outlines our approach to improve the usage choice of suitable devices in different health care environments (contexts). Safety-critical medical devices are presumed to have undergone a thorough (user-centred) design process to optimize the device for the intended purpose, user group and environment. However, in real-life health care scenarios, actual usage may not reflect the original design parameters. We suggest the identification of further usage contexts for safety-critical medical devices through ethnographic and other studies, to assist better modelling of the challenges of different usage environments. In combination with system and interaction models, these context models can then be used for decision-support in choosing medical devices that are suitable for the intended environment.

    View record details
  • A survey of software requirements specification practices in the New Zealand software industry

    Groves, Lindsay; Nickson, Ray; Reeve, Greg; Reeves, Steve; Utting, Mark (1999-06)

    Working or discussion paper
    University of Waikato

    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.

    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
  • µ-Charts and Z: Extending the translation

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

    Working or discussion paper
    University of Waikato

    This paper describes extensions and modifications to the µ-charts as given in earlier papers of Philipps and Scholz. The charts are extended to include a command language, integer-valued signals and local integer variables. The command language is based on the syntax presented in Scholz’ thesis and the integer-valued signals and local variables are based loosely on Scholz’ earlier work. After presenting the new semantics we turn to extending the µ-charts-to-Z translation that we developed in previous work. The extensions to the translation process describe both the changes due to the extensions to the µ-charts and a modification to the translation method to more fully capture the beneficial modularisation encouraged by the µ-charts formalism. We finish by giving three complete translation examples. The paper should be read as a record of our gradual development of a Z semantics for µ-charts–hence its sometimes exploratory character or laborious explanations as we come to terms (thinking out loud) with the (sometimes very subtle) meaning of µ-charts, especially with regard to pathological and unusual examples of their use.

    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