Shape and Content

摘要: The verification community has studied dynamic data structures primarily in a bottom-up way by analyzing pointers and the shapes induced them. Recent work fields such as separation logic made significant progress extracting from program source code. Many real world programs however manipulate complex whose structure content is most naturally described formalisms object oriented programming databases. In this paper, we look at of with perspective representation. Our approach based on description logic, widely used knowledge representation paradigm which gives logical underpinning for diverse modeling frameworks UML ER. Technically, assume that have shape invariants obtained analysis tool, requirements terms logic. We show two-variable fragment first order counting trees can be joint framework to embed suitable fragments