This paper reports a preliminary work on using an aspect oriented attribute grammar system called UU_AG to develop computer aided verification tools, UU_AG provides an abstract and modular way to develop such a tool and later on incrementally upgrade them. This paper shows an example of a toy programming logic implemented in UU_AG. We will show the implementation of the verificationcondition generator (VCG). We extend the implementatin with a new feature such as run-time trace generator to validate the computation of the implemented inference engine