Article Free Access Share on Relationships between users' and interfaces' task representations Authors: Robert B. Terwilliger Institute of Cognitive Science, University of Colorado, Boulder, CO Institute of Cognitive Science, University of Colorado, Boulder, COView Profile , Peter G. Polson Institute of Cognitive Science, University of Colorado, Boulder, CO Institute of Cognitive Science, University of Colorado, Boulder, COView Profile Authors Info & Claims CHI '97: Proceedings of the ACM SIGCHI Conference on Human factors in computing systemsMarch 1997 Pages 99–106https://doi.org/10.1145/258549.258617Published:27 March 1997Publication History 5citation440DownloadsMetricsTotal Citations5Total Downloads440Last 12 Months25Last 6 weeks7 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF

A study measured the time experienced Macintosh users took to create a graph from pre-existing daa including the assignment of vtiables to axes in a dialog box. The study revealed that the task took less time when the items in the dialog box were labeled in terms of one problem representation, even when the instructions were written in terms of another. The Kitajima and Poison model explains this as resulting from the problem representation being elaborated with task-speeific schemata during the instruction comprehension process.

Usersattempting to interaetwith an application for the fmt time are confronted with the problem of determing which commandto executein order to accomplishtheir goals. A “rational analysis”wasconductedin order to determinehow users ought to behave when faced with this decision problem. The resulting model is able to account at a qualitative level for a number of behaviors that users actually exhibit when trying to use a new application.

We are investigating software design processes using a three part approach. For a design method of interest, we first perform walkthroughs on a number of small problems. Second, we construct a simulation program which duplicates the designs produced by the walkthroughs, and third, we construct a process program that supports human application of the method. We have been pursuing this program for the formal design process developed by Dijkstra and Gries. In this paper, we describe our first step towards process programming this method: ISLET, a language-oriented program/proof editor. ISLET supports simple stepwise refinement with proof by automatically generating and mechanically certifying verification conditions. In addition, through ISLET the programmer has access to a library of pre-verified cliches that can be used to create programs more easily. We have constructed a prototype implementation in Prolog and used it to generate a number of example designs.

Software design processes are investigated using a three-part approach. For a design method of interest, walkthroughs are first performed on a number of small problems. Second, a simulation program is constructed which duplicates the design produced by the walkthroughs. Third, a process program is constructed that supports human application of the method. This program is being pursued for the formal design process developed by Dijkstra and Gries. (E.W. Dijkstra, 1975, 1976; D. Gries, 1981). This method takes as input a pre- and post-condition specification written in predicate logic and through a sequence of steps transforms it into an algorithm written using guarded commands. A simulation program is described for this process that is based on a library of cliches describing solutions to common programming problems. A prototype implementation was constructed in Prolog and used to generate a number of example designs

It has also been suggested that methods combining stepwise refinment with formal proof can help solve the verification problem. In these methods, components are first specified using using a mathematical notation. These specifications are then incrementally refined into implementations. The refinements are performed one at a time, and each is verified before another is applied; therefore, the implementations satisfy the specifications. Since each refinement step is small, design and implementation errors can be detected and corrected sooner and at lower cost.

article Free Access Share on An example of formal specification as an aid to design and development Authors: R. B. Terwilliger Department of Computer Science, University of Colorado, Boulder, CO Department of Computer Science, University of Colorado, Boulder, COView Profile , M. J. Maybee Department of Computer Science, University of Colorado, Boulder, CO Department of Computer Science, University of Colorado, Boulder, COView Profile , L. J. Osterweil Department of Computer Science, University of Colorado, Boulder, CO Department of Computer Science, University of Colorado, Boulder, COView Profile Authors Info & Claims ACM SIGSOFT Software Engineering NotesVolume 14Issue 3May 1989 pp 266–272https://doi.org/10.1145/75200.75239Online:01 April 1989Publication History 7citation457DownloadsMetricsTotal Citations7Total Downloads457Last 12 Months4Last 6 weeks2 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF

ENCOMPASS is an environment designed to support the incremental construction of Ada programs using executable specifications and formal techniques similar to the Vienna Development Method. ENCOMPASS supports the rigorous development of software: parts of a project may use completely formal methods, while other, less critical parts use less expensive techniques. ENCOMPASS provides automated support for all aspects of the development process including specification, prototyping, testing, formal verification, documentation, configuration control, and project management. In ENCOMPASS, software can be specified using PLEASE, an Ada-based executable specification language which can be automatically translated into Prolog. A prototype implementation of ENCOMPASS has been constructed. The authors give an overview of ENCOMPASS, describe the decisions made in the design of the prototype, and discuss the lessons learned in the process.< >

ENCOMPASS, a prototype software development environment, is being constructed from components built by the SAGA project. Application of SAGA to the major phases of the lifecycle will be demonstrated through ENCOMPASS. The system will include configuration management; a software design paradigm based on the Vienna Development Method; executable specifications; languages which can be used to support modular programming, like Berkeley Pascal or ADA; verification and validation tools and methods; and basic management tools. ENCOMPASS is intended to examine many of the requirements for the design of complex software development environments such as might be used to construct the space station software. It is intended to be used as a prototype for examining many of the more advanced features that will be required in future generations of software development environments which support aerospace applications. In this paper, we describe the framework adopted within ENCOMPASS to provide automated management. We exemplify the approach using an example taken from problem tracking and change control during software maintenance.

Article Free Access Share on PLEASE:Predictable Logic based ExecutAble SpeCifications Authors: Robert B. Terwilliger Department of Computer Science, University of Illinois at Urbana-Champaign, 252 Digital Computer Laboratory, 1304 West Springfield Avenue, Urbana, IL Department of Computer Science, University of Illinois at Urbana-Champaign, 252 Digital Computer Laboratory, 1304 West Springfield Avenue, Urbana, ILView Profile , Roy H. Campbell Department of Computer Science, University of Illinois at Urbana-Champaign, 252 Digital Computer Laboratory, 1304 West Springfield Avenue, Urbana, IL Department of Computer Science, University of Illinois at Urbana-Champaign, 252 Digital Computer Laboratory, 1304 West Springfield Avenue, Urbana, ILView Profile Authors Info & Claims CSC '86: Proceedings of the 1986 ACM fourteenth annual conference on Computer scienceFebruary 1986 Pages 349–358https://doi.org/10.1145/324634.325453Published:01 February 1986Publication History 12citation166DownloadsMetricsTotal Citations12Total Downloads166Last 12 Months3Last 6 weeks1 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF

ENCOMPASS is an example integrated software engineering environment being constructed by the SAGA project. ENCOMPASS supports the specification, design, construction and maintenance of efficient, validated, and verified programs in a modular programming language. The life cycle paradigm, schema of software configurations, and hierarchical library structure used by ENCOMPASS is presented. In ENCOMPASS, the software life cycle is viewed as a sequence of developments, each of which reuses components from the previous ones. Each development proceeds through the phases planning, requirements definition, validation, design, implementation, and system integration. The components in a software system are modeled as entities which have relationships between them. An entity may have different versions and different views of the same project are allowed. The simple entities supported by ENCOMPASS may be combined into modules which may be collected into projects. ENCOMPASS supports multiple programmers and projects using a hierarchical library system containing a workspace for each programmer; a project library for each project, and a global library common to all projects.

A key component of the 'SAGA' metatool system for software development support is an integrated modular environment that furnishes a uniform view of software components and can be adapted for different programming languages and development methodologies. Attention is presently given to the model/representation of the entities thus used in software development; programs are structured on the basis of modules whose relationships form layers of abstraction. Different views of the program under development are provided for different development phases. The implementation of the modular environment based on the model of a UNIX system is presented.