This paper describes a design framework for developing application-specific serial array circuits. Starting from a description of the state-transition logic or a fully-parallel architecture, correctness-preserving tra...
详细信息
This paper describes a design framework for developing application-specific serial array circuits. Starting from a description of the state-transition logic or a fully-parallel architecture, correctness-preserving transformations are employed to derive a wide range of implementations with different space-time trade-offs. The approach has been used in synthesising designs based on field-programmable gate arrays, and is illustrated by the development of a number of circuits including sorters and convolvers.< >
This paper considers a range of theoretical approaches to the understanding of organisations and the implications these views have for the design of computer supported cooperative work systems. Organisations have ofte...
详细信息
The safety of software is becoming increasingly important as computers pervade control systems on which human life depends. Whilst hardware has become significantly more reliable over the years, the same cannot be sai...
详细信息
The safety of software is becoming increasingly important as computers pervade control systems on which human life depends. Whilst hardware has become significantly more reliable over the years, the same cannot be said of software. This has become more complex and methods to ensure its correctness have been slow in development. One approach is to mathematically verify software in such systems. This paper investigates the industrial use of these techniques, their advantages and disadvantages, and the introduction of standards and their recommendations concerning formal methods in this area. The cost of safety is also considered.
The mathematical treatment of the concepts of vagueness and approximation is of increasing importance in artificial intelligence and related research. The theory of fuzzy sets was created by Zadeh [Z] to allow represe...
详细信息
The mathematical treatment of the concepts of vagueness and approximation is of increasing importance in artificial intelligence and related research. The theory of fuzzy sets was created by Zadeh [Z] to allow representation and mathematical manipulation of situations of partial truth, and proceeding from this a large amount of theoretical and applied development of this concept has occurred. The aim of this paper is to develop a natural logic and set theory that is a candidate for the formalisation of the theory of fuzzy sets. In these theories the underlying logic of properties and sets is intuitionistic, but there is a subset of formulae that are ‘crisp’, classical and two-valued, which represent the certain information. Quantum logic or logics weaker than intuitionistic can also be adopted as the basis, as described in [L]. The relationship of this theory to the intensional set theory MZF of [Gd] and the global intuitionistic set theory GIZF of Takeuti and Titani [TT] is also treated.
作者：
HOARE, CAROxford University
Computing Laboratory Programming Research Group 8-11 Keble Road Oxford OX1 3QD UK
This paper shows how propositional logic may be used to reason about synchronous combinational switching circuits implemented in C-mos. It develops a simple formalism and theory for describing and predicting their beh...
详细信息
This paper shows how propositional logic may be used to reason about synchronous combinational switching circuits implemented in C-mos. It develops a simple formalism and theory for describing and predicting their behaviour. On this it builds a calculus of design which is driven by proof obligations. The design philosophy for software introduced in [1] is thereby extended to a certain kind of hardware design. No prior knowledge of hardware is assumed of the reader;but useful background, motivation, examples and pictures may be found in [2]. Many of the problems described in that paper have been solved in this one.
The sliding-window protocol is specified using the notation of Communicating Sequential Processes and its partial correctness is proved using the trace semantics. First the stop-and-wait protocol is defined;its correc...
详细信息
The sliding-window protocol is specified using the notation of Communicating Sequential Processes and its partial correctness is proved using the trace semantics. First the stop-and-wait protocol is defined;its correctness, that it forms a 1-place buffer, is almost evident. Next the alternating-bit protocol is defined and described in terms of the stop-and-wait protocol, and its correctness deduced from that of the stop-and-wait protocol. Finally the sliding-window protocol is described in terms of the alternating-bit protocol and its correctness deduced accordingly. The paper has two thrusts: that modularity of a specification helps to structure proofs about it (in this case, proofs that the protocols implement buffers);and that refinement in CSP leads to structured, correct implementation in occam. In support of the latter point the appendix contains a refinement and implementation of the protocols in occam 2.
It is known that functional refinement does not preserve the security properties of a system. The authors propose a trace-based method for specifying the security properties of a system and a method which ensures that...
We give here a general definition of term rewriting in the simply typed λ-calculus, and use it to define higher-order forms of term rewriting systems, and equational unification and their properties. This provides a ...
详细信息
This paper describes a scheme for representing heterogeneous array circuits, in particular those which have been optimised by pipelining or by transposition. Equations for correctness-preserving transformations of the...
详细信息
It is known that functional refinement does not preserve the security properties of a system. The authors propose a trace-based method for specifying the security properties of a system and a method which ensures that...
详细信息
It is known that functional refinement does not preserve the security properties of a system. The authors propose a trace-based method for specifying the security properties of a system and a method which ensures that this security is preserved under refinement. They include an example to illustrate the use of the definitions and make use of non-interference (as defined in their notation).< >
暂无评论