Mutation testing in UTP

This paper presents a theory of testing that integrates into Hoare and He’s Unifying Theory of Programming (UTP). We give test cases a denotational semantics by viewing them as specification predicates. This reformulation of test cases allows for relating test cases via refinement to specifications...

Full description

Saved in:
Bibliographic Details
Published in:Formal aspects of computing 2009-02, Vol.21 (1-2), p.33-64
Main Authors: Aichernig, Bernhard K., Jifeng, He
Format: Article
Language:English
Subjects:
Computer Science
Math Applications in Computer Science
Original Article
Theory of Computation
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
cited_by cdi_FETCH-LOGICAL-c424t-dbef0fe04b7e812b390628c106f4634dfc8e16db6cb0d9c458f1af17ef96ece63
cites cdi_FETCH-LOGICAL-c424t-dbef0fe04b7e812b390628c106f4634dfc8e16db6cb0d9c458f1af17ef96ece63
container_end_page 64
container_issue 1-2
container_start_page 33
container_title Formal aspects of computing
container_volume 21
creator Aichernig, Bernhard K.
Jifeng, He
description This paper presents a theory of testing that integrates into Hoare and He’s Unifying Theory of Programming (UTP). We give test cases a denotational semantics by viewing them as specification predicates. This reformulation of test cases allows for relating test cases via refinement to specifications and programs. Having such a refinement order that integrates test cases, we develop a testing theory for fault-based testing. Fault-based testing uses test data designed to demonstrate the absence of a set of pre-specified faults. A well-known fault-based technique is mutation testing. In mutation testing, first, faults are injected into a program by altering (mutating) its source code. Then, test cases that can detect these errors are designed. The assumption is that other faults will be caught, too. In this paper, we apply the mutation technique to both, specifications and programs. Using our theory of testing, two new test case generation laws for detecting injected (anticipated) faults are presented: one is based on the semantic level of UTP design predicates, the other on the algebraic properties of a small programming language.
doi_str_mv 10.1007/s00165-008-0083-6
format article
fullrecord <record><control><sourceid>proquest_hal_p</sourceid><recordid>TN_cdi_hal_primary_oai_HAL_hal_00477906v1</recordid><sourceformat>XML</sourceformat><sourcesystem>PC</sourcesystem><sourcerecordid>1638242411</sourcerecordid><originalsourceid>FETCH-LOGICAL-c424t-dbef0fe04b7e812b390628c106f4634dfc8e16db6cb0d9c458f1af17ef96ece63</originalsourceid><addsrcrecordid>eNp1kM1Lw0AQxRdRsFbP4i14EQ-rs5_JHktRK1T00IK3Jdns1pQ0qbuJ4H_vhoiC4GEYGH7vzZtB6ILADQFIbwMAkQIDZEMxLA_QhHDGMFXq9RBNQDGOBXB2jE5C2EZaKEIm6Pyp7_Kuapuks6Grmk1SNcl69XKKjlxeB3v23adofX-3mi_w8vnhcT5bYsMp73BZWAfOAi9SmxFaMAWSZoaAdFwyXjqTWSLLQpoCSmW4yBzJHUmtU9IaK9kUXY--b3mt977a5f5Tt3mlF7OlHmYAPE2j6weJ7NXI7n373se4elcFY-s6b2zbB51yLhXQlEby8g-5bXvfxEM0BSZkxoWIEBkh49sQvHU_-wno4al6fGqMkA3F9BCXjpoQ2WZj_a_x_6Iveq12lA</addsrcrecordid><sourcetype>Open Access Repository</sourcetype><iscdi>true</iscdi><recordtype>article</recordtype><pqid>203568455</pqid></control><display><type>article</type><title>Mutation testing in UTP</title><source>ACM Digital Library</source><creator>Aichernig, Bernhard K. ; Jifeng, He</creator><creatorcontrib>Aichernig, Bernhard K. ; Jifeng, He</creatorcontrib><description>This paper presents a theory of testing that integrates into Hoare and He’s Unifying Theory of Programming (UTP). We give test cases a denotational semantics by viewing them as specification predicates. This reformulation of test cases allows for relating test cases via refinement to specifications and programs. Having such a refinement order that integrates test cases, we develop a testing theory for fault-based testing. Fault-based testing uses test data designed to demonstrate the absence of a set of pre-specified faults. A well-known fault-based technique is mutation testing. In mutation testing, first, faults are injected into a program by altering (mutating) its source code. Then, test cases that can detect these errors are designed. The assumption is that other faults will be caught, too. In this paper, we apply the mutation technique to both, specifications and programs. Using our theory of testing, two new test case generation laws for detecting injected (anticipated) faults are presented: one is based on the semantic level of UTP design predicates, the other on the algebraic properties of a small programming language.</description><identifier>ISSN: 0934-5043</identifier><identifier>EISSN: 1433-299X</identifier><identifier>DOI: 10.1007/s00165-008-0083-6</identifier><identifier>CODEN: FACME5</identifier><language>eng</language><publisher>London: Springer-Verlag</publisher><subject>Computer Science ; Math Applications in Computer Science ; Original Article ; Theory of Computation</subject><ispartof>Formal aspects of computing, 2009-02, Vol.21 (1-2), p.33-64</ispartof><rights>British Computer Society 2008</rights><rights>British Computer Society 2009</rights><rights>Distributed under a Creative Commons Attribution 4.0 International License</rights><lds50>peer_reviewed</lds50><oa>free_for_read</oa><woscitedreferencessubscribed>false</woscitedreferencessubscribed><citedby>FETCH-LOGICAL-c424t-dbef0fe04b7e812b390628c106f4634dfc8e16db6cb0d9c458f1af17ef96ece63</citedby><cites>FETCH-LOGICAL-c424t-dbef0fe04b7e812b390628c106f4634dfc8e16db6cb0d9c458f1af17ef96ece63</cites></display><links><openurl>$$Topenurl_article</openurl><openurlfulltext>$$Topenurlfull_article</openurlfulltext><thumbnail>$$Tsyndetics_thumb_exl</thumbnail><link.rule.ids>230,314,780,784,885,27924,27925</link.rule.ids><backlink>$$Uhttps://hal.science/hal-00477906$$DView record in HAL$$Hfree_for_read</backlink></links><search><creatorcontrib>Aichernig, Bernhard K.</creatorcontrib><creatorcontrib>Jifeng, He</creatorcontrib><title>Mutation testing in UTP</title><title>Formal aspects of computing</title><addtitle>Form Asp Comp</addtitle><description>This paper presents a theory of testing that integrates into Hoare and He’s Unifying Theory of Programming (UTP). We give test cases a denotational semantics by viewing them as specification predicates. This reformulation of test cases allows for relating test cases via refinement to specifications and programs. Having such a refinement order that integrates test cases, we develop a testing theory for fault-based testing. Fault-based testing uses test data designed to demonstrate the absence of a set of pre-specified faults. A well-known fault-based technique is mutation testing. In mutation testing, first, faults are injected into a program by altering (mutating) its source code. Then, test cases that can detect these errors are designed. The assumption is that other faults will be caught, too. In this paper, we apply the mutation technique to both, specifications and programs. Using our theory of testing, two new test case generation laws for detecting injected (anticipated) faults are presented: one is based on the semantic level of UTP design predicates, the other on the algebraic properties of a small programming language.</description><subject>Computer Science</subject><subject>Math Applications in Computer Science</subject><subject>Original Article</subject><subject>Theory of Computation</subject><issn>0934-5043</issn><issn>1433-299X</issn><fulltext>true</fulltext><rsrctype>article</rsrctype><creationdate>2009</creationdate><recordtype>article</recordtype><recordid>eNp1kM1Lw0AQxRdRsFbP4i14EQ-rs5_JHktRK1T00IK3Jdns1pQ0qbuJ4H_vhoiC4GEYGH7vzZtB6ILADQFIbwMAkQIDZEMxLA_QhHDGMFXq9RBNQDGOBXB2jE5C2EZaKEIm6Pyp7_Kuapuks6Grmk1SNcl69XKKjlxeB3v23adofX-3mi_w8vnhcT5bYsMp73BZWAfOAi9SmxFaMAWSZoaAdFwyXjqTWSLLQpoCSmW4yBzJHUmtU9IaK9kUXY--b3mt977a5f5Tt3mlF7OlHmYAPE2j6weJ7NXI7n373se4elcFY-s6b2zbB51yLhXQlEby8g-5bXvfxEM0BSZkxoWIEBkh49sQvHU_-wno4al6fGqMkA3F9BCXjpoQ2WZj_a_x_6Iveq12lA</recordid><startdate>20090201</startdate><enddate>20090201</enddate><creator>Aichernig, Bernhard K.</creator><creator>Jifeng, He</creator><general>Springer-Verlag</general><general>Association for Computing Machinery</general><general>Springer Verlag</general><scope>AAYXX</scope><scope>CITATION</scope><scope>3V.</scope><scope>7SC</scope><scope>7XB</scope><scope>8AL</scope><scope>8AO</scope><scope>8FD</scope><scope>8FE</scope><scope>8FG</scope><scope>8FK</scope><scope>ABUWG</scope><scope>AFKRA</scope><scope>ARAPS</scope><scope>AZQEC</scope><scope>BENPR</scope><scope>BGLVJ</scope><scope>CCPQU</scope><scope>DWQXO</scope><scope>GNUQQ</scope><scope>HCIFZ</scope><scope>JQ2</scope><scope>K7-</scope><scope>L7M</scope><scope>L~C</scope><scope>L~D</scope><scope>M0N</scope><scope>P5Z</scope><scope>P62</scope><scope>PQEST</scope><scope>PQQKQ</scope><scope>PQUKI</scope><scope>PRINS</scope><scope>Q9U</scope><scope>FR3</scope><scope>P64</scope><scope>RC3</scope><scope>1XC</scope><scope>VOOES</scope></search><sort><creationdate>20090201</creationdate><title>Mutation testing in UTP</title><author>Aichernig, Bernhard K. ; Jifeng, He</author></sort><facets><frbrtype>5</frbrtype><frbrgroupid>cdi_FETCH-LOGICAL-c424t-dbef0fe04b7e812b390628c106f4634dfc8e16db6cb0d9c458f1af17ef96ece63</frbrgroupid><rsrctype>articles</rsrctype><prefilter>articles</prefilter><language>eng</language><creationdate>2009</creationdate><topic>Computer Science</topic><topic>Math Applications in Computer Science</topic><topic>Original Article</topic><topic>Theory of Computation</topic><toplevel>peer_reviewed</toplevel><toplevel>online_resources</toplevel><creatorcontrib>Aichernig, Bernhard K.</creatorcontrib><creatorcontrib>Jifeng, He</creatorcontrib><collection>CrossRef</collection><collection>ProQuest Central (Corporate)</collection><collection>Computer and Information Systems Abstracts</collection><collection>ProQuest Central (purchase pre-March 2016)</collection><collection>Computing Database (Alumni Edition)</collection><collection>ProQuest Pharma Collection</collection><collection>Technology Research Database</collection><collection>ProQuest SciTech Collection</collection><collection>ProQuest Technology Collection</collection><collection>ProQuest Central (Alumni) (purchase pre-March 2016)</collection><collection>ProQuest Central (Alumni)</collection><collection>ProQuest Central</collection><collection>Advanced Technologies &amp; Aerospace Collection</collection><collection>ProQuest Central Essentials</collection><collection>AUTh Library subscriptions: ProQuest Central</collection><collection>Technology Collection</collection><collection>ProQuest One Community College</collection><collection>ProQuest Central</collection><collection>ProQuest Central Student</collection><collection>SciTech Premium Collection</collection><collection>ProQuest Computer Science Collection</collection><collection>Computer Science Database</collection><collection>Advanced Technologies Database with Aerospace</collection><collection>Computer and Information Systems Abstracts – Academic</collection><collection>Computer and Information Systems Abstracts Professional</collection><collection>Computing Database</collection><collection>Advanced Technologies &amp; Aerospace Database</collection><collection>ProQuest Advanced Technologies &amp; Aerospace Collection</collection><collection>ProQuest One Academic Eastern Edition (DO NOT USE)</collection><collection>ProQuest One Academic</collection><collection>ProQuest One Academic UKI Edition</collection><collection>ProQuest Central China</collection><collection>ProQuest Central Basic</collection><collection>Engineering Research Database</collection><collection>Biotechnology and BioEngineering Abstracts</collection><collection>Genetics Abstracts</collection><collection>Hyper Article en Ligne (HAL)</collection><collection>Hyper Article en Ligne (HAL) (Open Access)</collection><jtitle>Formal aspects of computing</jtitle></facets><delivery><delcategory>Remote Search Resource</delcategory><fulltext>fulltext</fulltext></delivery><addata><au>Aichernig, Bernhard K.</au><au>Jifeng, He</au><format>journal</format><genre>article</genre><ristype>JOUR</ristype><atitle>Mutation testing in UTP</atitle><jtitle>Formal aspects of computing</jtitle><stitle>Form Asp Comp</stitle><date>2009-02-01</date><risdate>2009</risdate><volume>21</volume><issue>1-2</issue><spage>33</spage><epage>64</epage><pages>33-64</pages><issn>0934-5043</issn><eissn>1433-299X</eissn><coden>FACME5</coden><abstract>This paper presents a theory of testing that integrates into Hoare and He’s Unifying Theory of Programming (UTP). We give test cases a denotational semantics by viewing them as specification predicates. This reformulation of test cases allows for relating test cases via refinement to specifications and programs. Having such a refinement order that integrates test cases, we develop a testing theory for fault-based testing. Fault-based testing uses test data designed to demonstrate the absence of a set of pre-specified faults. A well-known fault-based technique is mutation testing. In mutation testing, first, faults are injected into a program by altering (mutating) its source code. Then, test cases that can detect these errors are designed. The assumption is that other faults will be caught, too. In this paper, we apply the mutation technique to both, specifications and programs. Using our theory of testing, two new test case generation laws for detecting injected (anticipated) faults are presented: one is based on the semantic level of UTP design predicates, the other on the algebraic properties of a small programming language.</abstract><cop>London</cop><pub>Springer-Verlag</pub><doi>10.1007/s00165-008-0083-6</doi><tpages>32</tpages><oa>free_for_read</oa></addata></record>
fulltext fulltext
identifier ISSN: 0934-5043
ispartof Formal aspects of computing, 2009-02, Vol.21 (1-2), p.33-64
issn 0934-5043
1433-299X
language eng
recordid cdi_hal_primary_oai_HAL_hal_00477906v1
source ACM Digital Library
subjects Computer Science
Math Applications in Computer Science
Original Article
Theory of Computation
title Mutation testing in UTP
url http://sfxeu10.hosted.exlibrisgroup.com/loughborough?ctx_ver=Z39.88-2004&ctx_enc=info:ofi/enc:UTF-8&ctx_tim=2025-01-06T05%3A38%3A51IST&url_ver=Z39.88-2004&url_ctx_fmt=infofi/fmt:kev:mtx:ctx&rfr_id=info:sid/primo.exlibrisgroup.com:primo3-Article-proquest_hal_p&rft_val_fmt=info:ofi/fmt:kev:mtx:journal&rft.genre=article&rft.atitle=Mutation%20testing%20in%20UTP&rft.jtitle=Formal%20aspects%20of%20computing&rft.au=Aichernig,%20Bernhard%20K.&rft.date=2009-02-01&rft.volume=21&rft.issue=1-2&rft.spage=33&rft.epage=64&rft.pages=33-64&rft.issn=0934-5043&rft.eissn=1433-299X&rft.coden=FACME5&rft_id=info:doi/10.1007/s00165-008-0083-6&rft_dat=%3Cproquest_hal_p%3E1638242411%3C/proquest_hal_p%3E%3Cgrp_id%3Ecdi_FETCH-LOGICAL-c424t-dbef0fe04b7e812b390628c106f4634dfc8e16db6cb0d9c458f1af17ef96ece63%3C/grp_id%3E%3Coa%3E%3C/oa%3E%3Curl%3E%3C/url%3E&rft_id=info:oai/&rft_pqid=203568455&rft_id=info:pmid/&rfr_iscdi=true