In the upstream of software development, the ambiguity of natural languages (say, English, Japanese) becomes a problem for designing software.
The ambiguity of natural languages makes ambiguous specification.
Ambiguous specification causes ambiguous understanding of the system to be developed.
Implementation based on ambiguos understanding causes discrepancies between specification and implementation.
Finally, bugs are included in the software.
To solve this issue,
By designing the software with formal specification language instead of natural languages,
it's available
VDM (Vienna Development Method) is one of the formal methods. And VDM-SL is formal specification language of VDM.
In this research,
we develop
BWDM analyzes boundary values of software specification written in VDM++ that is object-oriented dialect of VDM-SL,
and generates test cases.
Input and output are shown below.
The decision table is generated by the decision table generation support tool developed in this laboratory.
Input for this support tool is VDM++ specification, and its output is a decision table that format is csv (comma separated values).
And test cases generated by BWDM consist of input data and expected output data.
Parsing : By using VDMJ (https://github.com/NickBattle).
Extraction : Extract information (argument types, parameter, if-conditions) from fucntion definition for boundary value analysis.
Boundary Value Analysis : Generate boundary values based on extracted information. And generate test cases.
Now, the constraction of VDM++ that BWDM can analyze is function definition only.
Also, BWDM can not analyze pre conditions and post conditions too.
The argument types are only Integer (int ,nat, nat1).
The number of arguments of function is only two.
It has been found that there are cases where it isn't possible to cover all the paths by current analysis.
For this reasen, we implement processing based on Symbolic Execution.