A JML Compiler Based on AspectJ