W-AVJ（Wonsec - Automatic Verifier for J）是一款基于JML形式化规约语言进行合约约束的形式化验证工具软件。它采用插件集成的方式，对JAVA源代码文件进行形式化验证。emc易倍该系统通过接收一个包含形式规约语言注释的程序，找到源代码中不符合注释描述的内容，从而确保源代码的功能正确性。该系统提供了用于描述功能的形式规约语言，基于形式规约语言注释的源代码形式化自动验证器，以及良好的验证状态、验证结果与源代码功能错误定位的界面展示。

　　W-AVJ(JAVA代码形式化验证)采用插件集成的方式，emc易倍对JAVA语言源代码文件进行形式化验证。

　　源代码编辑模块提供直接编辑源代码功能。可在W-AVJ上直接添加、修改、删除源代码，更方便于开发人员在定位到错误代码位置后修改代码。

　　源代码形式规约编辑模块根据功能规范emc易倍，直接在源代码中编辑形式化规约注释语言。

　　通过接收一个经过解析的包含形式规约语言注释的源代码，根据霍尔逻辑原理对源代码进行验证，找到其中不符合注释描述的内容，从而确保源代码的功能正确性。

　　验证报告输出模块以界面方式展示验证结果信息，包含验证代码位置、验证错误信息等，并根据验证结果提供错误代码位置定位功能。

　　明确定位代码出错位置，emc易倍方便开发人员定位错误所在行，并对代码进行修改完善，提高效率。

　　地址：浙江省绍兴市柯桥区齐贤街道柯桥经济技术开发区西环路586号科创大厦A座507-508