Abstract
This paper provides a review of Raymond Turner’s book Computational Artefacts. Towards a Philosophy of Computer Science. Focus is made on the definition of program correctness as the twofold problem of evaluating whether both the symbolic program and the physical implementation satisfy a set of specifications. The review stresses how these are not two separate problems. First, it is highlighted how formal proofs of correctness need to rely on the analysis of physical computational processes. Secondly, it is underlined how software testing requires considering the formal relations holding between the specifications and the symbolic program. Such a mutual dependency between formal and empirical program verification methods is finally shown to influence the debate on the epistemological status of computer science.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
Ammann, P., & Offutt, J. (2016). Introduction to software testing. New York: Cambridge University Press.
Baier, C., & Katoen, J. P. (2008). Principles of model checking. Cambridge, MA: MIT press.
Callahan, J., Schneider, F., & Easterbrook, F. (1996). Automated software testing using model checking. In: J. C. Gregoire, G. J. Holzmann and D. Peled, (Eds) Proceedings 1996 Spin Workshop (vol 353), pp. 118–127. Rutgers, NY.
Clarke, E. M., Grumberg, O., & Peled, D. A. (1999). Model Checking. Cambridge: The MIT Press.
Hoare, C. A. R. (1969). An axiomatic basis for computer programming. Communications of the ACM, 12(10), 576–580.
Kroes, P., & Meijers, A. (2002). The dual nature of technical artifacts: presentation of a new research programme. Techné: Res Philos Technol, 6(2), 4–8.
Magnani, L., Nersessian, N., & Thagard, P. (Eds.). (1999). Model-based reasoning in scientific discovery. New York: Springer Science & Business Media.
Schiaffonati, V. (2015). Stretching the traditional notion of experiment in computing: explorative experiments. Sci Eng Ethics, 22(3), 1–19.
Symons, J., & Horner, J. (2014). Software intensive science. Philosophy and Technology, 27(3), 461–477.
Turner, R. (2018). Computational artifacts: towards a philosophy of computer science. Berlin: Springer-Verlag.
Van Leeuwen, J. (1990). Handbook of theoretical computer science. Volume B: Formal models and semantics. Cambridge, MA: MIT Press.
Wang, C., Hachtel, G. D., & Somenzi, F. (2006). Abstraction refinement for large scale model checking. New York: Springer Science & Business Media.
Author information
Authors and Affiliations
Corresponding author
Additional information
Publisher’s Note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
Rights and permissions
About this article
Cite this article
Angius, N. On the Mutual Dependence Between Formal Methods and Empirical Testing in Program Verification. Philos. Technol. 33, 349–355 (2020). https://doi.org/10.1007/s13347-019-00364-9
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s13347-019-00364-9