In this paper, we present an idea about verifying OCL pre/post condition. This idea works by mapping pre/post conditions to a graph specification that can be verified by a tool called Cyclone. The purpose of this paper is to show a developing idea rather than presenting a more complete approach. We illustrate this idea by using an example, discuss our work-in-progress and outline challenges to be tackled in the future.