Specification-based testing of Ada units with low encapsulation

Describes a system that improves testing quality by supporting automatic test data selection, execution and result verification. The system tests poorly-encapsulated Ada units against formal specifications. This task is difficult partly because the unit´s interface is not explicit, but rather is buried in the body/implementation code. We attack this problem by making the unit´s interface explicit and complete. This is accomplished via automatic and manual analysis of the body. The complete interface is represented using an extended algebraic signature notation. Once the signature has been discovered, it can be reformulated so that a collection of well-defined, static mappings are established between it and the signature of the unit´s formal specification. These mappings guide the development of test artifact transformers and oracles, which support automatic test data selection, execution and result verification. This paper discusses problems that arise as a result of testing under low encapsulation, discusses our solution using an ongoing example, and compares our solution to earlier solutions