检索结果-内蒙古大学图书馆

丛书名： Workshops in computing

1000年

作者： J. P. Bowen J. E. Nicholls

ISBN: (数字)9781447135562

ISBN: (纸本)9783540198185

The Z notation has been developed at the programming {1. group at the oxford university computing laboratory and elsewhere for over a decade. It is now used by industry as part of the software (and hardware) development process in both Europe and the USA. It is currently undergoing BSI standardisation in the UK, and has been proposed for ISO standardisation internationally. In recent years {1.ers have begun to focus increasingly on the development of techniques and tools to encourage the wider application of Z and other formal methods and notations. This volume contains papers from the Seventh Annual Z User Meeting, held in London in December 1.92. In contrast to previous years the meeting concentrated specifically on industrial applications of Z, and a high proportion of the participants came from an industrial background. The theme is well represented by the four invited papers. Three of these discuss ways in which formal methods are being introduced, and the fourth presents an international survey of industrial applications. It also provides a reminder of the improvements which are needed to make these methods an accepted part of software development. In addition the volume contains several submitted papers on the industrial use of Z, two of which discuss the key area of safety-critical applications. There are also a number of papers related to the recently-completed ZIP project. The papers cover all the main areas of the project including methods, tools, and the development of a Z Standard, the first publicly-available version of which was made available at the meeting. Finally the volume contains a select Z bibliography, and section on how to access information on Z through ***.z, the international, computer-based USENET newsgroup.;provides an important overview of current {1. into industrial applications of Z, and will provide invaluable reading for {1.ers, postgraduate students andalso potential industrial users of Z.

关键词： Software Engineering Mathematical Logic and Formal Languages Logics and Meanings of Programs programming Techniques

来源：评论

学校读者我要写书评

暂无评论

From programs to object code and back again using logic programming: Compilation and decompilation

引用

Journal of Software Maintenance: research and Practice 1993年第4期5卷 205-234页

作者： Bowen, Jonathan Oxford University Computing Laboratory Programming Research Group Oxford OX1 3QD 11 Keble Road United Kingdom

A compiler may be specified by a description of how each construct of the source language is translated into a sequence of object code instructions. It is possible to produce a compiler prototype almost directly from this specification in the form of a logic program. This defines a relation between allowed high‐level and low‐level program constructs. Normally a high‐level program is supplied as input to a compiler and object code is returned. Because of the declarative nature of a logic program, it is possible for the object code to be supplied and the allowed high‐level programs returned, resulting in a decompiler, provided enough information is available in the object code. This paper discusses the problems of adopting such an approach in practice. A simple compiler and decompiler are presented in full as an example in the logic programming language Prolog, together with some sample output. The possible benefits of using constraint logic programming are also considered. Potential applications include reverse‐engineering in the software maintenance process, verification of safety‐critical object code, quality assessment of code and program debugging tools. Copyright © 1.93 John Wiley & Sons, Ltd

关键词： Compiler Constraint logic programming Decompilation Logic programming Prolog prototyping Reverse‐engineering

来源：评论

学校读者我要写书评

暂无评论

Categories, Relations and Dynamic programming

引用

Mathematical Structures in Computer Science 1994年第1期4卷 33-69页

作者： De Moor, Oege Programming Research Group Oxford University Computing Laboratory Oxford OX1 3QD 11 Keble Road United Kingdom

Dynamic programming is a strategy for solving optimisation problems. In this paper, we show how many problems that may be solved by dynamic programming are instances of the same abstract specification. This specification is phrased using the calculus of relations offered by topos theory. The main theorem underlying dynamic programming can then be proved by straightforward equational reasoning.

关键词：

来源：评论

学校读者我要写书评

暂无评论

Denotational semantics as a specification of code generators 82

Denotational semantics as a specification of code generators

引用

1.82 SIGPLAN Symposium on Compiler Construction, SIGPLAN 1.82

作者： Raskovsky, Martin R. Essex University Department Of Computing Science Oxford University Computing Laboratory Programming Research Group United Kingdom

We describe the automatic generation - from the formal denotational semantic specification - of an efficient compiler's code generation phase, producing efficient code for real machines. The method has been succes... 详细信息

ISBN: (纸本)0897910745

关键词： Specifications

来源：评论

学校读者我要写书评

暂无评论

Event refinement in state-based concurrent systems

引用

Formal Aspects of computing 1995年第3期7.0卷 266-288页

作者： Sinclair, Jane Woodcock, Jim Programming Research Group Oxford University Computing Laboratory Oxford OX1 3QD 7-11 Keble Road United Kingdom

Operations on action systems may be defined corresponding to CSP hiding and renaming. These are of particular use in describing the refinement between action systems in which the granularity of actions is altered. We derive a simplified expression for hiding sets of actions and present sufficient conditions for forwards simulation in which the concrete system uses hiding and renaming. Both of these reduce the complexity of proofs of refinement. We present a case study in specification and refinement using action systems which makes use of the operations and refinement rules previously defined. © 1.95 BCS.

关键词： Action systems Concurrency Refinement State-based specification

来源：评论

学校读者我要写书评

暂无评论

A formal model of explanation

引用

Formal Aspects of computing 1995年第2期7卷 207-225页

作者： Todd, Bryan S. Stamper, Richard The Programming Research Group Oxford University Computing Laboratory Oxford OX1 3QD Wolfson Building Parks Road United Kingdom

As information systems become more complex, formal methods offer a solution to the increasing problem of ensuring correctness of design and implementation. This paper illustrates the use of mathematical specification to formalise the notion of 'explanation'. This is relevant to any information system which engages in inference. An information system is regarded as a homogeneous function on states of information. An explanation for a conclusion is regarded as a weakening of the theory relating input to output, such that the same conclusion is reached. As an example, the specification is implemented for a simple statistical classifier to assist medical diagnosis. © 1.95 BCS.

关键词： Computer-aided diagnosis Explanation Formal specification

来源：评论

学校读者我要写书评

暂无评论

Exits in the refinement calculus

引用

Formal Aspects of computing 1995年第1期7.0卷 54-76页

作者： King, Steve Morgan, Carroll Programming Research Group Oxford University Computing Laboratory Oxford OX1 3QD Wolfson Building Parks Rd United Kingdom

Although many programming languages contain exception handling mechanisms, their formal treatment - necessary for rigorous development - can be complex. Nevertheless, this paper presents a simple incorporation of exit commands and exception blocks into a rigorous program development method. The refinement calculus, chosen for the exercise, is a method of developing imperative programs. It is based on weakest preconditions, although they are not used explicitly during program construction;they merely justify the general method. In the style of the refinement calculus, program development laws are given that introduce and allow the manipulation of exits. The soundness of the new laws is shown using weakest preconditions (as for the existing refinement calculus laws). The extension of weakest preconditions needed to handle exits is a variation on earlier work of Cristian;the variation is necessary to handle nondeterminism. © 1.95 BCS.

关键词： Exception handling Exceptions Refinement calculus Weakest preconditions

来源：评论

学校读者我要写书评

暂无评论

Specification, Verification and Prototyping of an Optimized Compiler

引用

Formal Aspects of computing 1994年第6期6卷 643-658页

作者： Jifeng, He Bowen, Jonathan Oxford University Computing Laboratory Programming Research Group Oxford OX1 3QD Wolfson Building Parks Road United Kingdom

This paper generalizes an algebraic method for the design of a correct compiler to tackle specification and verification of an optimized compiler. The main optimization issues of concern here include the use of existing contents of registers where possible and the identification of common expressions. A register table is introduced in the compiling specification predicates to map each register to an expression whose value is held by it. We define different kinds of predicates to specify compilation of programs, expressions and Boolean tests. A set of theorems relating to these predicates, acting as a correct compiling specification, are presented and an example proof within the refinement algebra of the programming language is given. Based on these theorems, a prototype compiler in Prolog is produced. © 1.94 BCS.

关键词： Code optimization Formal verification Logic programming Program compilation Refinement algebra

来源：评论

学校读者我要写书评

暂无评论

Process simulation and refinement

引用

Formal Aspects of computing 1989年第1期1卷 229-241页

作者： Jifeng, He Oxford University Computing Laboratory Programming Research Group Oxford OX1 3QD 8-11 Keble Road United Kingdom

In this paper we deal with the problem of (nondeterministic and parallel) process refinement. The basic notion of refinement is defined via the improved failure semantics of CSP [BHR84, BrR85, Hoa85, Ros88]. The concept of simulation of Communicating Systems introduced in [Mil80, Par81. is generalised and proved to be sound for the correctness of refinement. A Galois connection is presented to show that up-simulation and down-simulation together provide a complete proof method. The paper also suggests that simulation can be employed to derive an implementation from a specification. © 1.89 BCS.

关键词： Refinement Simulation

来源：评论

学校读者我要写书评

暂无评论

Unification: A case-study in data refinement

引用

Formal Aspects of computing 1995年第2期7卷 150-168页

作者： Spivey, J.M. Programming Research Group Oxford University Computing Laboratory Oxford OX1 3QD Wolfson Building Parks Road United Kingdom

In this paper, the Z notation is used to develop a small theory of terms and substitutions within which a simple unification algorithm can be specified and proved correct. Particular emphasis is placed on the use of Z's mathematical data types to simplify the development and structure of this theory. The correctness of an abstract version of the algorithm is proved first;this version operates on substitutions by composition. Then data refinement is used to show that the substitutions can be represented by 'binding functions' that make composition a particularly efficient operation. The approach taken in this paper is compared with the approaches of three previous papers based on VDM. The contribution of this paper is to show how data refinement can be used to explain the design decisions behind a non-trivial program, and to provide a point of comparison between Z and VDM approaches to the same problem. © 1.95 BCS.

关键词： Data refinement Formal specification Unification

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：