Abstract
This article presents the generation and test case execution under the framework Focal. In the programming language Focal, all properties of the program are written within the source code. These properties are considered, here, as the program specification. We are interested in testing the code against these properties. Testing a property is split in two stages. First, the property is cut out in several elementary properties. An elementary property is a tuple composed of some pre-conditions and a conclusion. Lastly, each elementary property is tested separately. The pre-conditions are used to generate and select the test cases randomly. The conclusion allows us to compute the verdict. All the testing process is done automatically.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Antoy, S., Hamlet, D.: Automatically checking an implementation against its formal specification. IEEE Trans. Softw. Eng. 26(1), 55–69 (2000)
Berghofer, S., Nipkow, T.: Random testing in Isabelle/HOL. In: Cuellar, J., Liu, Z. (eds.) Software Engineering and Formal Methods (SEFM 2004), pp. 230–239. IEEE Computer Society, Los Alamitos (2004)
Bernot, G., Gaudel, M.-C., Marre, B.: Software testing based on formal specifications: a theory and a tool. Software Engineering Journal 6(6) (1991)
Bonichon, R., Delahaye, D., Doligez, D.: Zenon: An extensible automated theorem prover producing checkable proofs. In: Dershowitz, N., Voronkov, A. (eds.) LPAR 2007. LNCS (LNAI), vol. 4790, pp. 151–165. Springer, Heidelberg (2007)
Brucker, A.D., Wolff, B.: Test-Sequence Generation with HOL-TestGen – With an Application to Firewall Testing. In: Gurevich, Y., Meyer, B. (eds.) TAP 2007. LNCS, vol. 4454, Springer, Heidelberg (2007)
Chen, T.Y., Tse, T.H., Zhou, Z.: Fault-based testing without the need of oracles. Information & Software Technology 45(1), 1–9 (2003)
Cheon, Y., Leavens, G.T.: A simple and practical approach to unit testing: The jml and junit way. In: Magnusson, B. (ed.) ECOOP 2002. LNCS, vol. 2374, pp. 231–255. Springer, Heidelberg (2002)
Claessen, K., Hughes, J.: QuickCheck: a lightweight tool for random testing of Haskell programs. ACM SIGPLAN Notices 35(9), 268–279 (2000)
Dubois, C., Hardin, T., Viguié Donzeau-Gouge, V.: Building certified components within focal. In: Loidl, H.-W. (ed.) Revised Selected Papers from the Fifth Symposium on Trends in Functional Programming, TFP 2004. Trends in Functional Programming, München, Germany, vol. 5, pp. 33–48. Intellect (2006)
Dybjer, P., Haiyan, Q., Takeyama, M.: Combining testing and proving in dependent type theory. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol. 2758, pp. 188–203. Springer, Heidelberg (2003)
Flajolet, P., Sedgewick, R.: Analytic Combinatorics, ch. I-IX. In: Draft available electronically from P. Flajolet’s home page (2007)
INRIA. Coq, version 8.1 (November 2006), http://coq.inria.fr/
Koopman, P.W.M., Alimarine, A., Tretmans, J., Plasmeijer, M.J.: Gast: Generic automated software testing. In: Peña, R., Arts, T. (eds.) IFL 2002. LNCS, vol. 2670, pp. 84–100. Springer, Heidelberg (2003)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Carlier, M., Dubois, C. (2008). Functional Testing in the Focal Environment. In: Beckert, B., Hähnle, R. (eds) Tests and Proofs. TAP 2008. Lecture Notes in Computer Science, vol 4966. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-79124-9_7
Download citation
DOI: https://doi.org/10.1007/978-3-540-79124-9_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-79123-2
Online ISBN: 978-3-540-79124-9
eBook Packages: Computer ScienceComputer Science (R0)