epicardium
发表于 2025-3-26 21:52:13
http://reply.papertrans.cn/83/8247/824680/824680_31.png
HERTZ
发表于 2025-3-27 03:56:58
Weak Refinementternal operations. In this, we also consider the possibility of “livelock”, where internal operations are continuously enabled, its impact on refinement conditions, and the related notion of divergence.
汇总
发表于 2025-3-27 06:44:31
http://reply.papertrans.cn/83/8247/824680/824680_33.png
陶瓷
发表于 2025-3-27 11:37:50
Simple Refinementformal motivation of the simplest refinement relation of all, namely operation refinement. Operation refinement can be applied to individual operations without reference to the other operations present in the abstract data type (ADT). The other simple refinement rules presented in this chapter, esta
Gerontology
发表于 2025-3-27 16:00:01
Data Refinement and Simulationslying these definitions to abstract data types with partial relations are then considered. The central part of this chapter is the standard definition of data refinement for relational data types, the definitions of upward and downward simulations, and the statement of their soundness and joint comp
逢迎白雪
发表于 2025-3-27 20:21:02
Refinement in Zlar attention is given to the role of inputs and outputs in Z..In this chapter, we formulate the theory of data refinement for Z. This is done systematically: a relational interpretation will be given for the standard Z ADT as defined in Chap. .. We apply the simulation based refinement rules from C
Adenoma
发表于 2025-3-27 21:56:47
http://reply.papertrans.cn/83/8247/824680/824680_37.png
chastise
发表于 2025-3-28 02:11:55
Promotionomposing specifications in order to build multiple indexed instances of a single component. To do so the component is described as a local state together with operations acting on that state, a global state is then defined which consists of multiple instances of this local state together with global
Incorporate
发表于 2025-3-28 09:07:32
http://reply.papertrans.cn/83/8247/824680/824680_39.png
metropolitan
发表于 2025-3-28 11:33:53
A Single Simulation Rulean be proved using a combination of upward and downward simulation steps. This chapter presents an alternative in the form of powersimulations which provide for a single complete refinement rule for Z. This requires a change in the underlying framework, moving from relations to possibility mappings.