FLACK
发表于 2025-3-28 15:47:37
http://reply.papertrans.cn/83/8247/824680/824680_41.png
悠然
发表于 2025-3-28 20:38:01
IO Refinementystem. Indeed, many previous textbooks on Z and refinement had included subtle manipulations of inputs and outputs in refinement steps in their examples, without considering formal justifications. This chapter describes the new notion of “IO refinement”, which provides the foundations for changing,
PHAG
发表于 2025-3-28 22:54:05
Weak Refinementit is common to also use “internal” operations which are under the control of the system rather than of the observer. From a generalisation of the definition of data refinement in Chap. ., we obtain versions of the simulation conditions which allow the refinement, introduction and removal of such in
NEXUS
发表于 2025-3-29 03:14:45
Non-atomic Refinementoperation into several concrete ones. This chapter considers the consequences of allowing operations to be decomposed in refinement, which involves further generalisation of the theory from Chap. .. This is often known as non-atomic or action refinement in the literature. The final sections discuss
两栖动物
发表于 2025-3-29 08:56:43
Further Generalisations at whether new operations can be added without relating to any previous operations, or as multiple copies of previous ones: alphabet extension, and alphabet translation. It also describes a generalisation which looks at approximate refinement between abstract and concrete systems.
DOLT
发表于 2025-3-29 14:09:00
Refinement in Object-Zequences of the different interpretation of preconditions. We also consider how weak refinement and non-atomic refinement may be applied to Object-Z. Finally, we discuss the relation between refinement, and two other important concepts in object orientation: subtyping and inheritance.
Exonerate
发表于 2025-3-29 17:16:31
Simple Refinements without reference to the other operations present in the abstract data type (ADT). The other simple refinement rules presented in this chapter, establishing and imposing invariants, only apply in the context of a full ADT, and require abstraction, in the sense of the state not being observable.
雇佣兵
发表于 2025-3-29 20:23:12
Calculating Refinements needed is the abstract specification, a description of the concrete state space and a retrieve relation which links the abstract to concrete. The result of this calculation will be the most general data refinement of the abstract specification with respect to the concrete state space and retrieve relation used.
刀锋
发表于 2025-3-30 00:27:26
http://reply.papertrans.cn/83/8247/824680/824680_49.png
爱哭
发表于 2025-3-30 04:23:00
Non-atomic Refinementrther generalisation of the theory from Chap. .. This is often known as non-atomic or action refinement in the literature. The final sections discuss applications to verifying concurrent data structures.