出版社：European Association of Software Science and Technology (EASST)
摘要：Our work aims to build a bridge between constructive (top-down) and analytical (bottom-up) approaches to software verification. This paper presents a tool-supported method for linking two existing verification methods: Event-B (constructive) and Dafny (analytical). This method combines Event-B abstraction and refinement with the code-level verification features of Dafny . The link transforms Event-B models to Dafny contracts by providing a framework in which Event-B models can be implemented correctly. The paper presents a method for transformation of Event-B models of abstract data types to Dafny contracts. Also a prototype tool implementing the transformation method is outlined. The paper also defines and proves a formal link between property verification in Event-B and Dafny . Our approach is illustrated with a small case study.
其他摘要：Our work aims to build a bridge between constructive (top-down) and analytical (bottom-up) approaches to software verification. This paper presents a tool-supported method for linking two existing verification methods: Event-B (constructive) and Dafny (analytical). This method combines Event-B abstraction and refinement with the code-level verification features of Dafny . The link transforms Event-B models to Dafny contracts by providing a framework in which Event-B models can be implemented correctly. The paper presents a method for transformation of Event-B models of abstract data types to Dafny contracts. Also a prototype tool implementing the transformation method is outlined. The paper also defines and proves a formal link between property verification in Event-B and Dafny . Our approach is illustrated with a small case study.
