Converting Specifications in a Subset of Object-Z to Skeletal Spec# Code for both Static and Dynamic Analysis
By: Xiufeng Ni, Cui Zhang
Abstract
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#.
Cite as:
Xiufeng Ni, Cui Zhang, “Converting Specifications in a Subset of Object-Z to Skeletal Spec# Code for both Static and Dynamic Analysis”, Journal of Object Technology, Volume 7, no. 8 (November 2008), pp. 165-185, doi:10.5381/jot.2008.7.8.a6.
PDF | HTML | DOI | BiBTeX | Tweet this | Post to CiteULike | Share on LinkedIn