Recent work in sequential program semantics has produced both an operational (He et al., Sci. Comput. programming 28(2, 3) (1997) 171-192) and an axiomatic (Morgan et al., ACM Trans. programming Languages Systems 18(3...
详细信息
Recent work in sequential program semantics has produced both an operational (He et al., Sci. Comput. programming 28(2, 3) (1997) 171-192) and an axiomatic (Morgan et al., ACM Trans. programming Languages Systems 18(3) (1996) 325-353;Seidel et al., Tech Report PRG-TR-6-96, programming Research group, February 1996) treatment of total correctness for probabilistic demonic programs, extending Kozen's original work (J. Comput. System Sci. 22 (1981) 328-350;Kozen, Proc. 15th ACM Symp. on Theory of Computing, ACM, New York, 1983) by adding demonic nondeterminism. For practical applications (e.g. combining loop invariants with termination constraints) it is important to retain the traditional distinction between partial and total correctness. Jones (Monograph ECS-LFCS-90-105, Ph.D. Thesis, Edinburgh University, Edinburgh, UK, 1990) defines probabilistic partial correctness for probabilistic, but again not demonic programs. In this paper we combine all the above, giving an operational and axiomatic framework for both partial and total correctness of probabilistic and demonic sequential programs;among other things, that provides the theory to support our earlier - and practical - publication on probabilistic demonic loops (Morgan, in: Jifeng et al. (Eds.), Proc. BCS-FACS Seventh Refinement Workshop, Workshops in Computing, Springer, Berlin, 1996). (C) 2001 Elsevier Science B.V. All rights reserved.
A formal refinement calculus targeted at system-level descriptions in the IEEE standard hardware description language VHDL is described here. Refinement can be used to develop hardware description code that is '&#...
详细信息
A formal refinement calculus targeted at system-level descriptions in the IEEE standard hardware description language VHDL is described here. Refinement can be used to develop hardware description code that is ''correct by construction.'' The calculus is closely related to a Hoare-style programming logic for VHDL and real-time systems in general. That logic and a semantics for a core subset of VHDL are described. The programming logic and the associated refinement calculus are shown to be complete. This means that if there is a code that can be shown to implement a. given specification, then it will be derivable from the specification via the calculus.
A denotational semantics and a Hoare programming logic for a subset of the standard hardware description language VHDL are set out here. Both define the behaviour of synchronously clocked VHDL simulators in declarativ...
详细信息
A denotational semantics and a Hoare programming logic for a subset of the standard hardware description language VHDL are set out here. Both define the behaviour of synchronously clocked VHDL simulators in declarative and compositional style. The logic is proved complete with respect to the denotational semantics and a natural implementation of the logic in PROLOG as a validation condition generator for VHDL is also described. The subset of the language referred to above essentially consists of elaborated VHDL excluding only delta-delayed signal assignments and zero waits. However, for brevity, only one of the two forms of VHDL Signal assignment is treated here. Moreover, for simplicity, signal resolution functions and local state are assumed to have been encoded away via expressions and signals.
In the paper we suggest an approach to proving global properties of structured states by using languages with special modal operators reflecting an internal structure of these states.
In the paper we suggest an approach to proving global properties of structured states by using languages with special modal operators reflecting an internal structure of these states.
暂无评论