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

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. © 1995 BCS.

关键词： Exception handling Exceptions Refinement calculus Weakest preconditions

来源：评论

学校读者我要写书评

暂无评论

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. © 1995 BCS.

关键词： Computer-aided diagnosis Explanation Formal specification

来源：评论

学校读者我要写书评

暂无评论

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. © 1995 BCS.

关键词： Data refinement Formal specification Unification

来源：评论

学校读者我要写书评

暂无评论

An object model of data, based on the ODMG industry standard for database applications

An object model of data, based on the ODMG industry standard...

引用

International Seminar on Client/Server computing. Seminar Proceedings (Digest No. 1995/184)

作者： K.R. Sujithan Programming Research Group Oxford University Computing Laboratory Oxford UK

The computational requirements of modern information systems, coupled with the inherent limitations of the relational databases, are stimulating research into post-relational database systems. The recent advances in object databases resulting from the integration of object-oriented programming capabilities with database capabilities, seem highly promising. The Object Database Management Group (ODMG) as part of the Object Management Group (OMG) has proposed a de facto standard known as ODMG-93 for object databases, which is rapidly gaining acceptance. The author introduces the relevant aspects of the object technology within the OMG framework, their Common Object Request Broker Architecture (CORBA), and discusses how this technology integrates with, and extends the client-server model. The author surveys the main elements of ODMG data model, particularly the datatypes supported, and introduces the elements of both, ODL (Object Definition Language) for defining the structure of the database, and OQL (Object Query Language) for defining queries over the database. Finally, some results are highlighted from the author's work on a calculus for the declarative representation of the OQL queries, suitable for an efficient implementation.

关键词：

来源：评论

学校读者我要写书评

暂无评论

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 RELATIVE ACCURACY OF A VARIETY OF MEDICAL DIAGNOSTIC PROGRAMS

引用

METHODS OF INFORMATION IN MEDICINE 1994年第4期33卷 402-416页

作者： TODD, BS STAMPER, R Programming Research Group Oxford University Computing Laboratory UK.

Acute abdominal pain is one of the most widely studied applications of computer-aided diagnosis. The usual approach is to apply Bayes' theorem with the assumption of conditional independence (''independence Bayes''). We compared various approaches to designing diagnostic programs for abdominal pain of suspected gynaecological origin. The methods range from statistical to knowledge-based. All programs were evaluated using a database of 1,270 cases collected retrospectively. Our results suggest that in this application no significant improvement in accuracy can be made by taking interactions into account, either by statistical or by knowledge-based means;independence Bayes is near-optimal. As far as accuracy is concerned, there appears to be little point in pursuing knowledge-based approaches. However, the ''nearest neighbours'' method using a new metric appears to be at least as accurate as independence Bayes. We argue that the nearest neighbours method is more suitable than independence Bayes for clinical use because of greater accountability.

关键词： COMPUTER-AIDED DIAGNOSIS NEAREST NEIGHBORS ABDOMINAL PAIN

来源：评论

学校读者我要写书评

暂无评论

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 *** generic specification of dynamic programming makes use of higher-order operators on relations, akin to the fold operators found in functional programming languages. In the present context, a data type is modelled as an initial F-algebra, where F is an endofunctor on the topos under consideration. The mediating arrows from this initial F-algebra to other F-algebras are instances of fold – but only for total functions. For a regular category ε, it is possible to construct a category of relations Rel(ε). When a functor between regular categories is a so-called relator, it can be extended (in some canonical way) to a functor between the corresponding categories of relations. Applied to an endofunctor on a topos, this process of extending functors preserves initial algebras, and hence fold can be generalised from functions to *** is well-known that the use of dynamic programming is governed by the principle of optimality. Roughly, the principle of optimality says that an optimal solution is composed of optimal solutions to subproblems. In a first attempt, we formalise the principle of optimality as a distributivity condition. This distributivity condition is elegant, but difficult to check in practice. The difficulty arises because we consider minimum elements with respect to a preorder, and therefore minimum elements are not unique. Assuming that we are working in a Boolean topos, it can be proved that monotonicity implies distributivity, and this monotonicity condition is easy to verify in practice.

关键词：

来源：评论

学校读者我要写书评

暂无评论

A SEMANTICS FOR LAMBDA-PROLOG

引用

THEORETICAL COMPUTER SCIENCE 1994年第1期136卷 277-289页

作者： WOLFRAM, DA Oxford University Computing Laboratory Programming Research Group Wolfson Building Parks Road Oxford OX1 3QD UK

We give a model-theoretic semantics for the logic of higher-order Horn clauses, the basis of a form of the lambdaProlog higher-order logic programming language. We define certain intensional general models and show th... 详细信息

关键词： Computer science

来源：评论

学校读者我要写书评

暂无评论

A generalized carrier-null method for conservative parallel simulation 94

A generalized carrier-null method for conservative parallel ...

引用

8th Workshop on Parallel and Distributed Simulation, PADS 1994

作者： Wood, Kenneth R. Turner, Stephen J. Programming Research Group Oxford University Computing Laboratory United Kingdom Department of Computer Science University of Exeter United Kingdom

ISBN: (纸本)1565550277

The carrier-null message approach to conservative distributed discrete-event simulation can significantly reduce the number of synchronization messages required to avoid deadlock. In thts paper we show that the original approach does not apply to simulations with arbitrary communication graphs and we propose a modified carrier-null approach whtch does. We present and discuss some preliminary results obtained using our approach to simulate digital logic circuits.

关键词： Discrete event simulation

来源：评论

学校读者我要写书评

暂无评论

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. © 1994 BCS.

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

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：