Right now an rcp file contains a) a ReCiPe system and b) zero or more specification, and it is "correct" iff its system satisfies all the specifications.
Sometimes it is nice to include properties that we know are not satisfied by the system. E.g., for regression testing, or to document an expected behaviour of the system. Thus, it would be nice to decorate specifications with their expected verification outcome.
My suggestion is to allow a syntax
where b ::= true|false denotes the expexted outcome of verifying the system against phi. For compatibility and to keep the specs compact, we would treat SPEC phi as synonym for SPEC{true} phi.
Then, an rcp file is correct iff all of its specifications give the expected verification verdict, be it true or false.
Right now an
rcpfile contains a) a ReCiPe system and b) zero or more specification, and it is "correct" iff its system satisfies all the specifications.Sometimes it is nice to include properties that we know are not satisfied by the system. E.g., for regression testing, or to document an expected behaviour of the system. Thus, it would be nice to decorate specifications with their expected verification outcome.
My suggestion is to allow a syntax
where
b ::= true|falsedenotes the expexted outcome of verifying the system againstphi. For compatibility and to keep the specs compact, we would treatSPEC phias synonym forSPEC{true} phi.Then, an
rcpfile is correct iff all of its specifications give the expected verification verdict, be it true or false.