​​​​​​​​​​​​ W-AVJ 简介

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

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

JAVA代码形式化验证主要可以分为以下几个模块：

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

源代码解析模块将源代码解析为可以进行源代码自动验证的验证输入。

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

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

验证结果分析模块根据源代码验证模块返回的验证信息进行结果分析处理。

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

​​​

可直接在JAVA代码中撰写注释，验证只需点击一次按钮

​​​

​​​

​​​

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

基于霍尔逻辑的自动化验证Java文件的形式化验证工具软件。

W-AVJ能够快速检测代码对设计的一致性和异常行为。

​​​