Chiang Mai, Thailand
Dec. 10, 2003 to Dec. 12, 2003
Jason McDonald , The University of Queensland, Australia
Paul Strooper , The University of Queensland, Australia
Dan Hoffman , University of Victoria, Canada
A test oracel provides a means for determining whether an implementation behaves according to its specification. A passive test oracle checks that the correct behaviour has been implemented, but does not implement the behaviour itself. In previous work, we have presented a method that allows us to derive passive C++ test oracles from formal specifications written in Object-Z. In this paper, we describe the "Warlock" prototype tool that supports the method. Warlock is built on top on an existing Object-Z type checker and generates oracle code for a substantial subset of the Object-Z language. We describe the architecture of Warlock and its application to a number of Object-Z specifications. We also discuss its current limitations.
Jason McDonald, Paul Strooper, Dan Hoffman, "Tool Support for Generating Passive C++ Test Oracles from Object-Z Specifications", APSEC, 2003, 2013 20th Asia-Pacific Software Engineering Conference (APSEC), 2013 20th Asia-Pacific Software Engineering Conference (APSEC) 2003, pp. 322, doi:10.1109/APSEC.2003.1254386