VDMUnit for VDM-SL

[lausdahl]

Library for testing sl models using VDMUnit for sl

Library:

module TestRunner
exports all
definitions

operations

run : ()==>()
run()== is not yet specified;

markFail : () ==> ()
markFail () == is not yet specified;

setMsg : seq of char ==> ()
setMsg (msg) == is not yet specified;

end TestRunner


module Assert

imports from TestRunner all
exports all
definitions
operations
assertTrue: bool ==> ()
assertTrue (pbool) ==
  if not pbool then
    TestRunner`markFail();

assertTrueMsg: seq of char * bool ==> ()
assertTrueMsg (pmessage, pbool) ==
  if not pbool then
  (
    TestRunner`setMsg(pmessage);
    TestRunner`markFail();
  );

assertFalse: bool ==> ()
assertFalse (pbool) ==
  if pbool then
    TestRunner`markFail();

assertFalseMsg: seq of char * bool ==> ()
assertFalseMsg (pmessage, pbool) ==
   if pbool then
  (
    TestRunner`setMsg(pmessage);
    TestRunner`markFail();
  );

fail: () ==> ()
fail () == is not yet specified;

failMsg: seq of char ==> ()
failMsg (pmessage) == is not yet specified;

end Assert

test example:

module MyTest
imports from IO all
exports all definitions
operations
testError: ()==>()
testError()==(IO`println("Running MyTest`testError."); exit; IO`println("Continuing."));

test1Success: ()==>()
test1Success()==(IO`println("Running MyTest`test1Success."); skip; IO`println("Continuing."));

test2Error: ()==>()
test2Error()==(IO`println("Running MyTest`test1Success."); exit; IO`println("Continuing."));
end MyTest


module My2Test
imports from IO all,
       from Assert all
exports all
definitions
operations

setUp : () ==> ()
setUp () == IO`println("In setUp");

tearDown : () ==> ()
tearDown () == IO`println("In tearDown");

testSuccess: ()==>()
testSuccess()==(IO`println("Running My2Test`test."); skip; IO`println("Continuing."));

test1Success: ()==>()
test1Success()==(IO`println("Running My2Test`test1."); skip; IO`println("Continuing."));

test2Error: ()==>()
test2Error()==(IO`println("Running My2Test`test2."); exit; IO`println("Continuing."));

test3Success: ()==>()
test3Success()==(IO`println("Running My2Test`test3.."); skip; IO`println("Continuing."));

test4Fail: ()==>()
test4Fail()==(IO`println("Running My2Test`test4.."); Assert`assertTrueMsg("Expected failure", false); IO`println("Continuing."));

test5Success: ()==>()
test5Success()==(IO`println("Running My2Test`test5.."); Assert`assertTrueMsg("Not expecting failure", true); IO`println("Continuing."));

end My2Test

if execute with -Dvdm.unit.report then junit reports for CI is also generated, example:

<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<testsuite xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" errors="0" failures="0" name="Mqttest" skipped="0" tests="1" time="14.856560025" xsi:schemaLocation="https://maven.apache.org/surefire/maven-surefire-plugin/xsd/surefire-test-report.xsd">
  <testcase classname="MqttRouteTest" name="test" time="14.856560025"/>
</testsuite>

<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<testsuite xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" error="1" errors="0" failures="0" name="BeeTest" skipped="0" tests="3" time="0.04333706700000001" xsi:schemaLocation="https://maven.apache.org/surefire/maven-surefire-plugin/xsd/surefire-test-report.xsd">
  <testcase classname="BTest" name="test_abc" time="0.016850875">
    <error message="Error 4129: Exit &quot;... file.vdmsl) at line 90:17" type="ERROR">	harvMin = 36000
stack trace vdm
</error>
  </testcase>
 </testsuite>

[lausdahl]

Here another test:

module MyTest
imports from Assert all,
       from IO all
exports all definitions
operations

testFailure: ()==>()
testFailure()==
(
 IO`println("Before");
 Assert`assertTrueMsg("Fail deliberately", false);
 IO`println("After");
);

end MyTest

Output

Parsed 4 modules in 0.121 secs. No syntax errors
Type checked 4 modules in 0.082 secs. No type errors
Initialized 4 modules in 0.047 secs. 
Executing test: MyTest`testFailure()
Before
	FAIL: Fail deliberately
Executing test: MyTest`testOk()
Before
After
	OK
----------------------------------------
|    TEST RESULTS                      |
|--------------------------------------|
| Executed: 2                          |
| Failures: 1                          |
| Errors  : 0                          |
|______________________________________|
|              FAILURE                 |
|______________________________________|

()
Bye