P Test cases

P Test cases are used to define different finite scenarios under which we would like to check the correctness of our system.

P Test Cases Grammar

testcase
| test iden [main=iden] : modExpr ;                  # TestDecl
;

modExpr represent the P module defined using the module expressions described in P Module System

Test Case Declaration

P allows programmers to write different scenarios under which we would like to check the correctness of the module (or system) under test. More concretely, the system module to be tested is unioned with different environment modules (or test harnesses/drivers) to check its correctness for different inputs scenarios generated by the environment modules. Each test case is automatically discharged by the P Checker.

Syntax:: test tName [main=mName] : module_under_test ;

tName is the name of the test case, mName is the name of the main machine where the execution of the system starts, and module_under_test is the module to be tested (manual: modules in P).

Properties checked for a Test Case

For each testcase, the P checker by default asserts that for each execution of the system (i.e., module_under_test): (1) there are no unhandled event exceptions; (2) all local assertions in the program hold; (3) there are no deadlocks; and finally (4) based on the specification monitors that are attached to the module, these safety and liveness properties asserted by the monitors always hold.