Construction of correctness is an essential issue for the implementation of a reliable software system. Formal methods based verification techniques provide programmers various ways to reason their program correctness through mathematically supported static analysis and dynamic analysis. In this paper, we introduce a tool that converts formal specifications in a subset of Object-Z to skeletal Spec# code with assertions. This tool aims at facilitating the refinement from formal specifications to Spec# and the full usage of the static and dynamic analysis techniques in Spec#.
['Xiufeng Ni', 'Cui Zhang']
Converting Specifications in a Subset of Object-Z to Skeletal Spec# Code for both Static and Dynamic Analysis