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

International Symposium on Advanced research in Asynchronous Circuits and Systems

作者： G. Brown W. Luk J. O'Leary School of Electrical Engineering Cornell University Ithaca NY USA Programming Research Group Computing Laboratory Oxford University Oxford UK

We show how to retarget the correctness proof of a hardware compiler generating two-phase delay-insensitive circuits to a compiler generating four-phase speed-independent circuits. We use protocol converters to convert the specifications of our compiler's two-phase circuit elements into equivalent specifications for four-phase elements. The processes of converting the specifications and verifying their implementations are automated.

关键词： Hardware Protocols Delay Asynchronous circuits Production Program processors Laboratories Buildings Europe System recovery

来源：评论

学校读者我要写书评

暂无评论

An enhanced algorithm for the minimization of exclusive-OR sum-of-products for incompletely specified functions

An enhanced algorithm for the minimization of exclusive-OR s...

引用

IEEE International Conference on Computer Design: VLSI in Computers and Processors, (ICCD)

作者： T. Kozlowski E.L. Dagless J.M. Saul Electrical and Electronic Engineering Department University of Bristol Bristol UK Programming Research Group Oxford University Computing Laboratory Oxford UK

Most of the current exclusive-OR sum-of-products minimization algorithms use rule-based heuristics to transform an initial circuit description into a possibly compact form. This paper presents an enhanced minimization algorithm, MINT, introducing new transformations including rules operating on three product terms at a time. These multiple-product-term transformations prove to be an efficient extension of previously defined two-product-term operating rules. Additionally, new efficient procedures for the optimization based on the use of don't cares are introduced. The algorithm can simplify multiple-valued input two-valued multiple-output incompletely specified functions.

关键词： Minimization methods Programmable logic arrays Heuristic algorithms Circuits Laboratories Functional programming Input variables

来源：评论

学校读者我要写书评

暂无评论

The industrial take-up of formal methods in safety-critical and other areas: A perspective 1st

The industrial take-up of formal methods in safety-critical ...

引用

1st International Symposium of Formal Methods Europe, FME 1993

作者： Bowen, Jonathan Stavridou, Victoria Oxford University Computing Laboratory Programming Research Group 11 Keble Road OxfordOX1 3QD United Kingdom Department of Computer Science Royal ttolloway University of London Egham SurreyTW20 0EX United Kingdom

ISBN: (纸本)9783540566625

Formal methods may be at the crossroads of acceptance by a wider industrial community. In order for the techniques to become widely used, the gap between theorists and practitioners must be bridged effectively. In particular, safety-critical systems offer an application area where formal methods may be engaged usefully to the benefit of all. This paper discusses some of the issues concerned with the general acceptance of formal methods and concludes with a summary of the current position and how the formal methods community could proceed to improve matters in the future. © 1993, Springer Verlag. All rights reserved.

关键词： Formal methods

来源：评论

学校读者我要写书评

暂无评论

Unifying theories of healthiness condition

Unifying theories of healthiness condition

引用

Asia-Pacific Conference on Software Engineering

作者： He Jifeng C.A.R. Hoare International Institute for Software Technology United Nations University Macau Macao China Computing Laboratory Programming Research Group Oxford University Oxford UK

A theory of programming starts with a complete Boolean algebra of specifications, and defines healthiness conditions which exclude infeasibility of implementation. These are expressed as algebraic laws useful for transformation and optimisation of designs. programming notations and languages must be restricted to those preserving all the healthiness conditions. We have explored a wide range of programming paradigms, including nondeterministic, sequential, parallel, logical and probabilistic. In all cases, we have found a single healthiness condition, formalised by constructions due to Karoubi and to Kleisli. The uniformity maintains for all paradigms a single notion of correctness throughout the chain that leads from specification through designs to programs that are proved to meet the original specification.

关键词： Design optimization Laboratories Boolean algebra Logic programming Parallel programming Maintenance Specification languages

来源：评论

学校读者我要写书评

暂无评论

Dynamics of Control

Dynamics of Control

引用

Theoretical Aspects of Software Engineering (TASE)

作者： J W Sanders Matteo Turilli International Institute for Software Technology United Nations University Macau Macao China Programming Research Group Oxford University Computing Laboratory Oxford UK

This paper proposes a , the "ambit' of an action, that allows the degree of distribution of an action in a multiagent system to be quantified without regard to its functionality. It demonstrates the use of that notion in the design, analysis and implementation of dynamically-reconfigurable multi-agent systems. It distinguishes between the extensional (or system) view and intensional (or agent-based) view of such a system and shows how, using the notion of ambit, the step-wise derivation paradigm of formal methods can be used to derive the latter from the former. In closing it addresses the manner in which these ideas inform studies in the ethics of systems of artificial agents.

关键词： Multiagent systems Dynamic programming Ethics Personal digital assistants Control systems Functional programming Distributed computing Laboratories Buildings Information technology

来源：评论

学校读者我要写书评

暂无评论

Billiards and related systems on the bulk-synchronous parallel model 97

Billiards and related systems on the bulk-synchronous parall...

引用

Proceedings of the eleventh workshop on Parallel and distributed simulation

作者： Mauricio Marín Programming Research Group Computing Laboratory University of Oxford Wolson Building Parks Road Oxford OX1 3QD England UK

ISBN: (纸本)9780818679650

With two examples we show the suitability of the bulk-synchronous parallel (BSP) model for discrete-event simulation of homogeneous large-scale systems. This model provides a unifying approach for general purpose parallel computing which in addition to efficient and scalable computation, ensures portability across different parallel architectures. A valuable feature of this approach is a simple cost model that enables precise performance prediction of BSP algorithms. We show both theoretically and empirically that systems with uniform event occurrence among their components, such as colliding hard-spheres and ising-spin models, can be efficiently simulated in practice on current parallel computers supporting the BSP model.

关键词： ising-spin models bulk-synchronous parallel model discrete event simulation general purpose parallel computing billiards homogeneous large-scale systems colliding hard-spheres scalable computation discrete-event simulation

来源：评论

学校读者我要写书评

暂无评论

Using VDM with rely and guarantee-conditions: Experiences from a real project 2nd

Using VDM with rely and guarantee-conditions: Experiences fr...

引用

2nd VDM-Europe Symposium : The Way Ahead, 1988

作者： Woodcock, J.C.P. Dickinson, B. Oxford University Computing Laboratory Programming Research Group 8-11 Keble Road OxfordOX1 3QD United Kingdom GEC Telecommunications Ltd Telephone Works P.O.Box No.53 CoventryCV3 1HJ United Kingdom

ISBN: (纸本)9783540502142

In his extension of VDM, Jones added a rely and a guarantee-condition to the usual pre and post-condition pair. This extension to the technique permits the specification and development of concurrent, shared-variable systems. We describe the technique in detail by giving an example of a simple, but formal, development. A description of part of a substantial system development that has been carried out on a real project is given in the full version of this paper [Woodcock & Dickinson, 1988]. Conclusions are drawn, both about the rules for concurrent data reification, and about the efficacy of the technique and of the industrial use of formal methods in general. © 1988, Springer-Verlag.

关键词： Formal methods

来源：评论

学校读者我要写书评

暂无评论

Seven more myths of formal methods: Dispelling industrial prejudices 2nd

引用

2nd International Symposium of Formal Methods Europe, FME 1994

作者： Bowen, Jonathan P. Hinchey, Michael G. Oxford University Computing Laboratory Programming Research Group Wolfson Building Parks Road OxfordOX1 3QD United Kingdom University of Cambridge Computer Laboratory New Museums Site Pembroke Street CambridgeCB2 3QG United Kingdom Department of Computer and Information Science New Jersey Institute of Technology United States

ISBN: (纸本)9783540585558

For whatever reason, formal methods remain one of the more contentious techniques in industrial software engineering. Despite some improvement in the uptake of formal methods, it is still the case that the vast majority of potential users of formal methods fail to become actual users. A paper by Hall in 1990 [31] exaznined a number of ‘myths’ concerning formal methods, assumed by some to be valid. This paper considers a few more beliefs held by many and presents some counter examples. © 1994, Springer Verlag. All rights reserved.

关键词： Formal methods

来源：评论

学校读者我要写书评

暂无评论

BULK-SYNCHRONOUS PARALLEL ALGORITHMS FOR QR AND QZ MATRIX FACTORISATION

引用

Parallel Algorithms and Applications. 1997年第1-2期11卷 97-112页

作者： RADU CALINESCU DAVID J. EVANS [a] Programming Research Group Oxford University Computing Laboratory Oxford 0X1 3QD UK [b] Parallel Algorithms Research Centre Loughborough University of Technology Loughborough Leicestershire LE11 3TU UK

This paper presents bulk-synchronous parallel (BSP) algorithms for linear system solving through QR and QZ factorisation. The two new algorithms are analysed in terms of the BSP cost model, and portable implementations of the QR and QZ decomposition methods are devised using the Oxford BSP Library. The experimental results obtained on a shared-memory multiprocessor accurately match the theoretical predictions, permitting a thorough comparison of the two algorithms.

关键词： linear system solving QR factorisation QZ factorisation bulk-synchronous parallel model

来源：评论

学校读者我要写书评

暂无评论

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 © 1993 John Wiley & Sons, Ltd

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

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：