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...
详细信息
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 existi...
详细信息
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 conce...
详细信息
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...
详细信息
This volume contains papers from the Eighth Z User Meeting, to be held at the university of Cambridge from 29 - 30 June 1994. The papers cover a wide range of issues associated with Z and formal methods, with particul...
详细信息
ISBN:
(数字)9781447134527
ISBN:
(纸本)9783540198840
This volume contains papers from the Eighth Z User Meeting, to be held at the university of Cambridge from 29 - 30 June 1994. The papers cover a wide range of issues associated with Z and formal methods, with particular reference to practical application. These issues include education, standards, tool support, and interaction with other design paradigms such as consideration of real-time and object-oriented approaches to development. Among the actual topics covered are: the formal specification in Z of Defence Standard 00-56; formal specification of telephone features; specifying and interpreting class hierarchies in Z; and software quality assurance using the SAZ method.;provides an important overview of current research into industrial applications of Z, and will provide invaluable reading for researchers, postgraduate students and also potential industrial users of Z.
作者：
Hóre, C.A.R.Oxford University
Computing Laboratory Programming Research Group Oxford OX1 3QD 8‐11 Keble Road United Kingdom
The article discusses novelties in propositional calculus. It mentions the convenience of involving a dyadic operator as a curried monadic operator towards alleviation of its algebraic properties. It offers examples b...
详细信息
The article discusses novelties in propositional calculus. It mentions the convenience of involving a dyadic operator as a curried monadic operator towards alleviation of its algebraic properties. It offers examples based on a logical foundation study of computer programming along with conditional operators and negmajority. It also notes the notation of the operators as binary written in infix form as well as the tautological detection of propositional functions.
A scheme is presented which transforms systolic programs with a two-dimensional structure to one dimension. The elementary steps of the transformation are justified by theorems in the theory of communicating sequentia...
详细信息
Machines have proved very successful in the implementation of very high level logic and functional programming languages;in particular, we have the G-machine for functional programming languages and the WAM for Prolog...
详细信息
The authors describe a method for speeding up divide-and-conquer algorithms with a hardware coprocessor, using sorting as an example. The method employs a conventional processor for the 'divide' and 'merge...
详细信息
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 origin...
详细信息
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.
暂无评论