The bidirectional transformation has played beneficial roles in broad areas, database management, programming languages and model-driven development after Foster et al. revisited view updating problems introduced by Bancilhon and Spyratos. They introduced the concept of the (asymmetric) lens as a pair of a forward get and a backward put functions to synchronize source data and its view consistently. The consistency of the get and put functions is specified by several lens laws such as the (StrongGetPut), (GetPut), (PutGet) and (PutPut) laws. By combining some of these lens laws, we can represent how consistent a lens is. This chapter introduces 15 lens laws proposed in the literature, with their definitions, motivations and examples. In addition, their precise relationship will be given, such as the fact that one law implies another and that combining two laws is equivalent to combining three others. All implication relations are shown by a diagram, which is complete: every implication among lens laws is derivable by taking their transitive closure; the others have a counterexample. The results can be used to verify the law of desirable lenses quickly.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Lens Laws Zoo

  • Keisuke Nakano

摘要

The bidirectional transformation has played beneficial roles in broad areas, database management, programming languages and model-driven development after Foster et al. revisited view updating problems introduced by Bancilhon and Spyratos. They introduced the concept of the (asymmetric) lens as a pair of a forward get and a backward put functions to synchronize source data and its view consistently. The consistency of the get and put functions is specified by several lens laws such as the (StrongGetPut), (GetPut), (PutGet) and (PutPut) laws. By combining some of these lens laws, we can represent how consistent a lens is. This chapter introduces 15 lens laws proposed in the literature, with their definitions, motivations and examples. In addition, their precise relationship will be given, such as the fact that one law implies another and that combining two laws is equivalent to combining three others. All implication relations are shown by a diagram, which is complete: every implication among lens laws is derivable by taking their transitive closure; the others have a counterexample. The results can be used to verify the law of desirable lenses quickly.